---

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


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. P : 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. BD ≅ DB
14. ¬¬(∃b':Point. (Cong3(BPD,Db'B) ∧ Colinear(D;b';B)))
⊢ {A=P=C ∧ B=P=D}
BY
{ (Unfold `guard` 0
   THEN (DoubleNegation THENA (BLemma `stable__and` THEN Auto))
   THEN (SupposeMore (-1) THENA Auto)
   THEN ExRepD
   THEN (RenameVar `P\'' (-3) THEN Thin (-4))
   THEN (D -2 THEN ExRepD)
   THEN (Assert FSC(B;D;P;A  D;B;P';C) BY
               RepeatFor 2 ((D 0 THEN Auto)))
   THEN (Assert FSC(B;D;P;C  D;B;P';A) BY
               RepeatFor 2 ((D 0 THEN Auto)))) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. P : 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 ≅ P'B
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)
⊢ ¬¬(A=P=C ∧ B=P=D)

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  D  :  Point
6.  P  :  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.  BD  \mcong{}  DB
14.  \mneg{}\mneg{}(\mexists{}b':Point.  (Cong3(BPD,Db'B)  \mwedge{}  Colinear(D;b';B)))
\mvdash{}  \{A=P=C  \mwedge{}  B=P=D\}


By

---

Latex:
(Unfold  `guard`  0
  THEN  (DoubleNegation  THENA  (BLemma  `stable\_\_and`  THEN  Auto))
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RenameVar  `P\mbackslash{}''  (-3)  THEN  Thin  (-4))
  THEN  (D  -2  THEN  ExRepD)
  THEN  (Assert  FSC(B;D;P;A    D;B;P';C)  BY
                          RepeatFor  2  ((D  0  THEN  Auto)))
  THEN  (Assert  FSC(B;D;P;C    D;B;P';A)  BY
                          RepeatFor  2  ((D  0  THEN  Auto))))

---

Home Index