Step
*
of Lemma
cong3-in-half-plane
∀e:EuclideanPlane. ∀a,b,c,x,y,u:Point.
  (c # ab 
⇒ u # xy 
⇒ ab ≅ xy 
⇒ (∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy 
⇐⇒ z leftof xy))))
BY
{ (Auto
   THEN (InstLemma `Euclid-drop-perp-1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅
         THENA (Auto THEN InstLemma  `lsep-iff-all-sep` [⌜e⌝;⌜c⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto)
         )
   THEN D -1) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. u : Point
8. c # ab
9. u # xy
10. ab ≅ xy
11. p : Point
12. Colinear(a;b;p) ∧ ab  ⊥p pc
⊢ ∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy 
⇐⇒ z leftof xy))
Latex:
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,u:Point.
    (c  \#  ab
    {}\mRightarrow{}  u  \#  xy
    {}\mRightarrow{}  ab  \mcong{}  xy
    {}\mRightarrow{}  (\mexists{}z:Point.  (Cong3(abc,xyz)  \mwedge{}  z  \#  xy  \mwedge{}  (u  leftof  xy  \mLeftarrow{}{}\mRightarrow{}  z  leftof  xy))))
By
Latex:
(Auto
  THEN  (InstLemma  `Euclid-drop-perp-1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  InstLemma    `lsep-iff-all-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  D  -1)
Home
Index