---

Step * 1 1 1 1 1 of Lemma geo-vert-angle-SAS


1. e : BasicGeometry
2. a : Point
3. p : Point
4. q : Point
5. p' : Point
6. q' : Point
7. p-a-q
8. p'-a-q'
9. pa ≅ p'a
10. qa ≅ q'a
11. p ≠ p'
12. q ≠ q'
13. r1 : Point
14. a-q-r1
15. qr1 ≅ ap
16. r2 : Point
17. a-q'-r2
18. q'r2 ≅ ap
19. r3 : Point
20. a-p-r3
21. pr3 ≅ aq
22. r4 : Point
23. a-p'-r4
24. p'r4 ≅ aq
25. r1=a=r3
26. r2=a=r4
27. r4r3 ≅ r2r1
28. r1r4 ≅ r3r2
⊢ p'q ≅ pq'
BY
{ (InstLemma `geo-inner-five-segment` [⌜e⌝;⌜r4⌝;⌜p'⌝;⌜a⌝;⌜q⌝;⌜r3⌝;⌜p⌝;⌜a⌝;⌜q'⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. e : BasicGeometry
2. a : Point
3. p : Point
4. q : Point
5. p' : Point
6. q' : Point
7. p-a-q
8. p'-a-q'
9. pa ≅ p'a
10. qa ≅ q'a
11. p ≠ p'
12. q ≠ q'
13. r1 : Point
14. a-q-r1
15. qr1 ≅ ap
16. r2 : Point
17. a-q'-r2
18. q'r2 ≅ ap
19. r3 : Point
20. a-p-r3
21. pr3 ≅ aq
22. r4 : Point
23. a-p'-r4
24. p'r4 ≅ aq
25. r1=a=r3
26. r2=a=r4
27. r4r3 ≅ r2r1
28. r1r4 ≅ r3r2
⊢ r4q ≅ r3q'

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  q  :  Point
5.  p'  :  Point
6.  q'  :  Point
7.  p-a-q
8.  p'-a-q'
9.  pa  \mcong{}  p'a
10.  qa  \mcong{}  q'a
11.  p  \mneq{}  p'
12.  q  \mneq{}  q'
13.  r1  :  Point
14.  a-q-r1
15.  qr1  \mcong{}  ap
16.  r2  :  Point
17.  a-q'-r2
18.  q'r2  \mcong{}  ap
19.  r3  :  Point
20.  a-p-r3
21.  pr3  \mcong{}  aq
22.  r4  :  Point
23.  a-p'-r4
24.  p'r4  \mcong{}  aq
25.  r1=a=r3
26.  r2=a=r4
27.  r4r3  \mcong{}  r2r1
28.  r1r4  \mcong{}  r3r2
\mvdash{}  p'q  \mcong{}  pq'


By

---

Latex:
(InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}r4\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r3\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}q'\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index