---

Step * 1 1 1 of Lemma cong3-in-half-plane


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
13. q : Point
14. Colinear(x;y;q) ∧ Cong3(abp,xyq)
15. r : Point
16. l : Point
17. [%27] : xy  ⊥q lq ∧ xy  ⊥q rq ∧ l leftof xy ∧ r leftof yx
⊢ ∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy ⇐⇒ z leftof xy))
BY
{ (Assert xy  ⊥q lq ∧ xy  ⊥q rq ∧ l leftof xy ∧ r leftof yx BY
         (Unhide THEN Auto THEN (Unfold `geo-perp-in` 0 THEN Auto) THEN Unfold `right-angle` 0 THEN Auto)) }

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
13. q : Point
14. Colinear(x;y;q) ∧ Cong3(abp,xyq)
15. r : Point
16. l : Point
17. [%27] : xy  ⊥q lq ∧ xy  ⊥q rq ∧ l leftof xy ∧ r leftof yx
18. xy  ⊥q lq ∧ xy  ⊥q rq ∧ l leftof xy ∧ r leftof yx
⊢ ∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy ⇐⇒ z leftof xy))

---

Latex:

---

Latex:

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  \mcong{}  xy
11.  p  :  Point
12.  Colinear(a;b;p)  \mwedge{}  ab    \mbot{}p  pc
13.  q  :  Point
14.  Colinear(x;y;q)  \mwedge{}  Cong3(abp,xyq)
15.  r  :  Point
16.  l  :  Point
17.  [\%27]  :  xy    \mbot{}q  lq  \mwedge{}  xy    \mbot{}q  rq  \mwedge{}  l  leftof  xy  \mwedge{}  r  leftof  yx
\mvdash{}  \mexists{}z:Point.  (Cong3(abc,xyz)  \mwedge{}  z  \#  xy  \mwedge{}  (u  leftof  xy  \mLeftarrow{}{}\mRightarrow{}  z  leftof  xy))


By

---

Latex:
(Assert  xy    \mbot{}q  lq  \mwedge{}  xy    \mbot{}q  rq  \mwedge{}  l  leftof  xy  \mwedge{}  r  leftof  yx  BY
              (Unhide
                THEN  Auto
                THEN  (Unfold  `geo-perp-in`  0  THEN  Auto)
                THEN  Unfold  `right-angle`  0
                THEN  Auto))

---

Home Index