---

Step * 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
⊢ p'q ≅ pq'
BY
{ ((Assert r1=a=r3 BY
          (Assert ⌜|ar1| = |ar3| ∈ Length⌝⋅ THEN Auto THEN D 0 THEN Auto))
   THEN (Assert r2=a=r4 BY
               (Assert ⌜|ar2| = |ar4| ∈ Length⌝⋅ THEN Auto THEN D 0 THEN Auto))
   ) }

1
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
⊢ p'q ≅ pq'

---

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
\mvdash{}  p'q  \mcong{}  pq'


By

---

Latex:
((Assert  r1=a=r3  BY
                (Assert  \mkleeneopen{}|ar1|  =  |ar3|\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto))
  THEN  (Assert  r2=a=r4  BY
                          (Assert  \mkleeneopen{}|ar2|  =  |ar4|\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto))
  )

---

Home Index