---

Step * 1 1 1 1 1 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)
13. ab  ⊥p pc
14. q : Point
15. Colinear(x;y;q)
16. ab ≅ xy
17. bp ≅ yq ∧ pa ≅ qx
18. r : Point
19. l : Point
20. xy  ⊥q lq
21. xy  ⊥q rq
22. l leftof xy
23. r leftof yx
24. r # l
25. r # q
26. l # q
27. z1 : Point
28. B(rqz1) ∧ qz1 ≅ pc
29. z2 : Point
30. B(lqz2) ∧ qz2 ≅ pc
31. p # c
⊢ ∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy ⇐⇒ z leftof xy))
BY
{ (Assert yz1 ≅ bc BY
         (gSeparatedCases ⌜b⌝ ⌜p⌝⋅
          THEN Auto
          THEN ((Progress(gEliminatePoints) THENA Auto)
          ORELSE (InstLemma `right-angle-SAS` [⌜e⌝;⌜y⌝;⌜q⌝;⌜z1⌝;⌜b⌝;⌜p⌝;⌜c⌝]⋅ 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)
13. ab  ⊥p pc
14. q : Point
15. Colinear(x;y;q)
16. ab ≅ xy
17. bp ≅ yq ∧ pa ≅ qx
18. r : Point
19. l : Point
20. xy  ⊥q lq
21. xy  ⊥q rq
22. l leftof xy
23. r leftof yx
24. r # l
25. r # q
26. l # q
27. z1 : Point
28. B(rqz1) ∧ qz1 ≅ pc
29. z2 : Point
30. B(lqz2) ∧ qz2 ≅ pc
31. p # c
32. yz1 ≅ bc
⊢ ∃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)
13.  ab    \mbot{}p  pc
14.  q  :  Point
15.  Colinear(x;y;q)
16.  ab  \mcong{}  xy
17.  bp  \mcong{}  yq  \mwedge{}  pa  \mcong{}  qx
18.  r  :  Point
19.  l  :  Point
20.  xy    \mbot{}q  lq
21.  xy    \mbot{}q  rq
22.  l  leftof  xy
23.  r  leftof  yx
24.  r  \#  l
25.  r  \#  q
26.  l  \#  q
27.  z1  :  Point
28.  B(rqz1)  \mwedge{}  qz1  \mcong{}  pc
29.  z2  :  Point
30.  B(lqz2)  \mwedge{}  qz2  \mcong{}  pc
31.  p  \#  c
\mvdash{}  \mexists{}z:Point.  (Cong3(abc,xyz)  \mwedge{}  z  \#  xy  \mwedge{}  (u  leftof  xy  \mLeftarrow{}{}\mRightarrow{}  z  leftof  xy))


By

---

Latex:
(Assert  yz1  \mcong{}  bc  BY
              (gSeparatedCases  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}p\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  ((Progress(gEliminatePoints)  THENA  Auto)
                ORELSE  (InstLemma  `right-angle-SAS`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
                )))

---

Home Index