---

Step * 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
⊢ p'q ≅ pq'
BY
{ (((FLemma `geo-midpoint-diagonals-congruent` [-1;-2] THENA Auto)
    THEN InstLemma `geo-midpoint-diagonals-congruent` [⌜e⌝;⌜a⌝;⌜r1⌝;⌜r4⌝;⌜r3⌝;⌜r2⌝]⋅
    )
   THEN EAuto 1
   ) }

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
27. r4r3 ≅ r2r1
28. r1r4 ≅ r3r2
⊢ 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
25.  r1=a=r3
26.  r2=a=r4
\mvdash{}  p'q  \mcong{}  pq'


By

---

Latex:
(((FLemma  `geo-midpoint-diagonals-congruent`  [-1;-2]  THENA  Auto)
    THEN  InstLemma  `geo-midpoint-diagonals-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}r4\mkleeneclose{};\mkleeneopen{}r3\mkleeneclose{};\mkleeneopen{}r2\mkleeneclose{}]\mcdot{}
    )
  THEN  EAuto  1
  )

---

Home Index