---

Step * 1 1 1 1 1 1 1 2 of Lemma geo-midpoint-diagonals-congruent


1. e : BasicGeometry
2. Q : Point
3. A : Point
4. P : Point
5. p : Point
6. q : Point
7. B(pAQ)
8. pA ≅ AQ
9. B(qAQ)
10. qA ≅ AQ
11. A # Q
12. A # Q
13. X : Point
14. B(AQX)
15. QX ≅ AQ
16. x : Point
17. B(Apx)
18. px ≅ AQ
19. Y : Point
20. B(AQY)
21. QY ≅ AQ
22. y : Point
23. B(Aqy)
24. qy ≅ AQ
25. x=A=X
26. y=A=Y
27. Ax ≅ Ay
28. XA ≅ yA
29. Ax ≅ AY
30. xy ≅ YX
31. P ≡ Q
⊢ QQ ≅ pq
BY
{ (InstLemma `seg-midpoints-equal` [⌜e⌝;⌜p⌝;⌜q⌝;⌜A⌝;⌜Q⌝]⋅ THENA (Auto THEN D 0 THEN Auto)) }

1
1. e : BasicGeometry
2. Q : Point
3. A : Point
4. P : Point
5. p : Point
6. q : Point
7. B(pAQ)
8. pA ≅ AQ
9. B(qAQ)
10. qA ≅ AQ
11. A # Q
12. A # Q
13. X : Point
14. B(AQX)
15. QX ≅ AQ
16. x : Point
17. B(Apx)
18. px ≅ AQ
19. Y : Point
20. B(AQY)
21. QY ≅ AQ
22. y : Point
23. B(Aqy)
24. qy ≅ AQ
25. x=A=X
26. y=A=Y
27. Ax ≅ Ay
28. XA ≅ yA
29. Ax ≅ AY
30. xy ≅ YX
31. P ≡ Q
32. p ≡ q
⊢ QQ ≅ pq

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  Q  :  Point
3.  A  :  Point
4.  P  :  Point
5.  p  :  Point
6.  q  :  Point
7.  B(pAQ)
8.  pA  \mcong{}  AQ
9.  B(qAQ)
10.  qA  \mcong{}  AQ
11.  A  \#  Q
12.  A  \#  Q
13.  X  :  Point
14.  B(AQX)
15.  QX  \mcong{}  AQ
16.  x  :  Point
17.  B(Apx)
18.  px  \mcong{}  AQ
19.  Y  :  Point
20.  B(AQY)
21.  QY  \mcong{}  AQ
22.  y  :  Point
23.  B(Aqy)
24.  qy  \mcong{}  AQ
25.  x=A=X
26.  y=A=Y
27.  Ax  \mcong{}  Ay
28.  XA  \mcong{}  yA
29.  Ax  \mcong{}  AY
30.  xy  \mcong{}  YX
31.  P  \mequiv{}  Q
\mvdash{}  QQ  \mcong{}  pq


By

---

Latex:
(InstLemma  `seg-midpoints-equal`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  D  0  THEN  Auto))

---

Home Index