Orthocenter

Load Eos

In[]:=
<<"EosHeader.m"

Orthocenter

The three (possibly extended) altitudes intersect in a single point H of the triangle.　The point H is called the orthocenter of the triangle.
In[]:=
EosSession["Orthocenter"];
In[]:=
NewOrigami[10]
Orthocenter: Step 1
Out[]=
In[]:=
NewPoint["E"{6,7}]
Orthocenter: Step 1
Out[]=
In[]:=
HO["AE"]!
Orthocenter: Step 3
Out[]=
In[]:=
HO["AE","B",Mark{"AE"}]!
Orthocenter: Step 5
Out[]=
In[]:=
HO["BE"]!
Orthocenter: Step 7
Out[]=
In[]:=
HO["BE","A",Mark{{"FB","H"}}]!
Orthocenter: Step 9
Out[]=
In[]:=
Goal[​​O4Q["AB","E","EH"]];
In[]:=
Prove["Orthocenter",Mapping{"A"{0,0},"B"{1,0},(*"C"{1,1},"D"{0,1},*)"E"{u,v}}]
ProofbyGB
::gbstart
:Proof by Groebner basis method started at March 22, 2021 at 10:56:17 PM JST.
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 0.027695 seconds.
Proof is successful.
Orthocenter: Step 9
Out[]=
Success,0.027695,
Orthocenter.nb

In[]:=
HO["AB","H",Mark{"AB"}]!
Orthocenter: Step 11
Out[]=
In[]:=
ShowOrigami[More{Thick,Red,Line[{"A","E","B","A"}]}]
Orthocenter: Step 11
Out[]=
In[]:=
EndSession[];