---

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

No Annotations
∀e:BasicGeometry. ∀A,B,C,D,P:Point.
  ((¬Colinear(A;B;C)) ⇒ B # D ⇒ AB ≅ CD ⇒ BC ≅ DA ⇒ Colinear(A;P;C) ⇒ Colinear(B;P;D) ⇒ {A=P=C ∧ B=P=D})
BY
{ (Auto THEN (Assert BD ≅ DB BY Auto) THEN (FLemma `geo-colinear-cong-tri-exists` [-1;-2]⋅ THENA 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. BD ≅ DB
14. ¬¬(∃b':Point. (Cong3(BPD,Db'B) ∧ Colinear(D;b';B)))
⊢ {A=P=C ∧ B=P=D}

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}A,B,C,D,P:Point.
    ((\mneg{}Colinear(A;B;C))
    {}\mRightarrow{}  B  \#  D
    {}\mRightarrow{}  AB  \mcong{}  CD
    {}\mRightarrow{}  BC  \mcong{}  DA
    {}\mRightarrow{}  Colinear(A;P;C)
    {}\mRightarrow{}  Colinear(B;P;D)
    {}\mRightarrow{}  \{A=P=C  \mwedge{}  B=P=D\})


By

---

Latex:
(Auto
  THEN  (Assert  BD  \mcong{}  DB  BY
                          Auto)
  THEN  (FLemma  `geo-colinear-cong-tri-exists`  [-1;-2]\mcdot{}  THENA  Auto))

---

Home Index