---

Step * 1 of Lemma geo-lt-angle-construction

.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ¬out(b ac)
9. p : Point
10. p' : Point
11. x' : Point
12. z' : Point
13. xyz ≅a abp
14. b_p'_p
15. out(b ax')
16. out(b cz')
17. ¬a_b_p
18. x'_p'_z'
19. p' ≠ z'
20. x # yz
21. a # bc
⊢ x'bp' ≅a xyz
BY
{ ((Assert b ≠ p' BY
          ((InstLemma  `out-preserves-lsep` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜x'⌝;⌜z'⌝]⋅ THEN Auto)
           THEN InstLemma  `colinear-lsep` [⌜e⌝;⌜x'⌝;⌜z'⌝;⌜b⌝;⌜p'⌝]⋅
           THEN Auto))
   THEN (InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜p⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜x'⌝;⌜p'⌝;⌜x⌝;⌜z⌝]⋅ THEN EAuto 1)
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  \mneg{}out(b  ac)
9.  p  :  Point
10.  p'  :  Point
11.  x'  :  Point
12.  z'  :  Point
13.  xyz  \mcong{}\msuba{}  abp
14.  b\_p'\_p
15.  out(b  ax')
16.  out(b  cz')
17.  \mneg{}a\_b\_p
18.  x'\_p'\_z'
19.  p'  \mneq{}  z'
20.  x  \#  yz
21.  a  \#  bc
\mvdash{}  x'bp'  \mcong{}\msuba{}  xyz


By

---

Latex:
((Assert  b  \mneq{}  p'  BY
                ((InstLemma    `out-preserves-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  InstLemma    `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}
                  THEN  Auto))
  THEN  (InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
              THEN  EAuto  1
              )
  THEN  D  0
  THEN  Auto)

---

Home Index