---

Step * 1 1 1 2 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
⊢ ¬¬(A=P=C ∧ B=P=D)
BY
{ (gSeparatedCases ⌜A⌝ ⌜C⌝⋅ THENA Auto) }

1
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)

2
1. e : BasicGeometry
2. C : Point
3. P : Point
4. A : Point
5. B : Point
6. D : Point
7. ¬Colinear(C;B;C)
8. B # D
9. CB ≅ CD
10. BC ≅ DC
11. Colinear(C;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. PC ≅ PC
21. PC ≅ PC
22. P' ≡ P
23. A ≡ C
⊢ ¬¬(A=P=C ∧ B=P=D)

---

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
\mvdash{}  \mneg{}\mneg{}(A=P=C  \mwedge{}  B=P=D)


By

---

Latex:
(gSeparatedCases  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index