---

Step * of Lemma eu-eq_dist-axiomsC-Pasch

∀e:EuclideanPlane. ∀x,y,z,u,t:Point.
  (((((Dbet(e;x;t;u) ∧ Dsep(e;x;t)) ∧ Dbet(e;y;u;z)) ∧ Dtri(e;x;y;u)) ∧ Dtri(e;u;z;t))
  ⇒ (∃v:Point. ((Dbet(e;x;v;y) ∧ Dsep(e;x;v) ∧ Dsep(e;v;y)) ∧ Dbet(e;z;t;v) ∧ Dsep(e;z;t) ∧ Dsep(e;t;v))))
BY
{ (Auto
   THEN (Assert ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|) BY
               ((Auto THEN (Assert B # AC BY Auto)) THEN FLemma  `Euclid-Prop20_cycle` [-1]  THEN Auto))
   THEN (InstLemma `outer-pasch-strict` [⌜e⌝;⌜z⌝;⌜u⌝;⌜y⌝;⌜t⌝;⌜x⌝]⋅ THENA Auto)) }

1
.....wf..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. u : Point
6. t : Point
7. Dbet(e;x;t;u)
8. Dsep(e;x;t)
9. Dbet(e;y;u;z)
10. Dtri(e;x;y;u)
11. Dtri(e;u;z;t)
12. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
⊢ y ∈ {c:Point| z_u_c} 

2
.....wf..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. u : Point
6. t : Point
7. Dbet(e;x;t;u)
8. Dsep(e;x;t)
9. Dbet(e;y;u;z)
10. Dtri(e;x;y;u)
11. Dtri(e;u;z;t)
12. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
⊢ x ∈ {y:Point| u-t-y} 

3
.....antecedent..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. u : Point
6. t : Point
7. Dbet(e;x;t;u)
8. Dsep(e;x;t)
9. Dbet(e;y;u;z)
10. Dtri(e;x;y;u)
11. Dtri(e;u;z;t)
12. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
⊢ t # zu

4
.....antecedent..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. u : Point
6. t : Point
7. Dbet(e;x;t;u)
8. Dsep(e;x;t)
9. Dbet(e;y;u;z)
10. Dtri(e;x;y;u)
11. Dtri(e;u;z;t)
12. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
⊢ u ≠ y

5
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. u : Point
6. t : Point
7. Dbet(e;x;t;u)
8. Dsep(e;x;t)
9. Dbet(e;y;u;z)
10. Dtri(e;x;y;u)
11. Dtri(e;u;z;t)
12. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
13. ∃p:Point [(z-t-p ∧ y-p-x)]
⊢ ∃v:Point. ((Dbet(e;x;v;y) ∧ Dsep(e;x;v) ∧ Dsep(e;v;y)) ∧ Dbet(e;z;t;v) ∧ Dsep(e;z;t) ∧ Dsep(e;t;v))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}x,y,z,u,t:Point.
    (((((Dbet(e;x;t;u)  \mwedge{}  Dsep(e;x;t))  \mwedge{}  Dbet(e;y;u;z))  \mwedge{}  Dtri(e;x;y;u))  \mwedge{}  Dtri(e;u;z;t))
    {}\mRightarrow{}  (\mexists{}v:Point
              ((Dbet(e;x;v;y)  \mwedge{}  Dsep(e;x;v)  \mwedge{}  Dsep(e;v;y))  \mwedge{}  Dbet(e;z;t;v)  \mwedge{}  Dsep(e;z;t)  \mwedge{}  Dsep(e;t;v))))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}A,B,C:Point.    (A  \#  BC  {}\mRightarrow{}  |AC|  <  |AB|  +  |BC|)  BY
                          ((Auto  THEN  (Assert  B  \#  AC  BY  Auto))
                            THEN  FLemma    `Euclid-Prop20\_cycle`  [-1] 
                            THEN  Auto))
  THEN  (InstLemma  `outer-pasch-strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index