---

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


1. e : BasicGeometry
2. A : Point
3. P : Point
4. Q : Point
5. p : Point
6. q : Point
7. B(pAP)
8. pA ≅ AP
9. B(qAQ)
10. qA ≅ AQ
11. A # P
12. A # Q
⊢ PQ ≅ pq
BY
{ (((gProlong ⌜A⌝ ⌜P⌝ `X' ⌜A⌝ ⌜Q⌝⋅ THEN Auto) THEN gProlong ⌜A⌝ ⌜p⌝ `x' ⌜A⌝ ⌜Q⌝⋅ THEN Auto)
   THEN (gProlong ⌜A⌝ ⌜Q⌝ `Y' ⌜A⌝ ⌜P⌝⋅ THEN Auto)
   THEN gProlong ⌜A⌝ ⌜q⌝ `y' ⌜A⌝ ⌜P⌝⋅
   THEN Auto) }

1
1. e : BasicGeometry
2. A : Point
3. P : Point
4. Q : Point
5. p : Point
6. q : Point
7. B(pAP)
8. pA ≅ AP
9. B(qAQ)
10. qA ≅ AQ
11. A # P
12. A # Q
13. X : Point
14. B(APX)
15. PX ≅ AQ
16. x : Point
17. B(Apx)
18. px ≅ AQ
19. Y : Point
20. B(AQY)
21. QY ≅ AP
22. y : Point
23. B(Aqy)
24. qy ≅ AP
⊢ PQ ≅ pq

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  P  :  Point
4.  Q  :  Point
5.  p  :  Point
6.  q  :  Point
7.  B(pAP)
8.  pA  \mcong{}  AP
9.  B(qAQ)
10.  qA  \mcong{}  AQ
11.  A  \#  P
12.  A  \#  Q
\mvdash{}  PQ  \mcong{}  pq


By

---

Latex:
(((gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}P\mkleeneclose{}  `X'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}Q\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}p\mkleeneclose{}  `x'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}Q\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}Q\mkleeneclose{}  `Y'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}P\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}q\mkleeneclose{}  `y'  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}P\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index