---

Step * 1 1 1 2 1 1 of Lemma opposite-side-congruent-diagonals-midpoint


1. e : BasicGeometry
2. P : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. ¬Colinear(A;B;C)
8. B # D
9. AB ≅ CD
10. BC ≅ DA
11. Colinear(A;P;C)
12. Colinear(B;P;D)
13. P' : Point
14. BP ≅ DP
15. PD ≅ PB
16. DB ≅ BD
17. Colinear(D;P;B)
18. FSC(B;D;P;A  D;B;P';C)
19. FSC(B;D;P;C  D;B;P';A)
20. PA ≅ PC
21. PC ≅ PA
22. P' ≡ P
23. A # C
⊢ ¬¬(A=P=C ∧ B=P=D)
BY
{ ((RemoveDoubleNegation THEN Auto) THEN BLemma `colinear-implies-midpoint` THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  P  :  Point
3.  A  :  Point
4.  B  :  Point
5.  C  :  Point
6.  D  :  Point
7.  \mneg{}Colinear(A;B;C)
8.  B  \#  D
9.  AB  \mcong{}  CD
10.  BC  \mcong{}  DA
11.  Colinear(A;P;C)
12.  Colinear(B;P;D)
13.  P'  :  Point
14.  BP  \mcong{}  DP
15.  PD  \mcong{}  PB
16.  DB  \mcong{}  BD
17.  Colinear(D;P;B)
18.  FSC(B;D;P;A    D;B;P';C)
19.  FSC(B;D;P;C    D;B;P';A)
20.  PA  \mcong{}  PC
21.  PC  \mcong{}  PA
22.  P'  \mequiv{}  P
23.  A  \#  C
\mvdash{}  \mneg{}\mneg{}(A=P=C  \mwedge{}  B=P=D)


By

---

Latex:
((RemoveDoubleNegation  THEN  Auto)  THEN  BLemma  `colinear-implies-midpoint`  THEN  Auto)

---

Home Index