---

Step * of Lemma eu-eq_dist-axiomsC-five-segment

∀e:EuclideanPlane. ∀x,y,z,x',y',z',u,u':Point.
  (Dcong(e;x;y;x';y')
  ⇒ Dcong(e;y;z;y';z')
  ⇒ Dcong(e;x;u;x';u')
  ⇒ Dcong(e;y;u;y';u')
  ⇒ (Dbet(e;x;y;z) ∧ Dsep(e;x;y) ∧ Dsep(e;y;z))
  ⇒ (Dbet(e;x';y';z') ∧ Dsep(e;x';y') ∧ Dsep(e;y';z'))
  ⇒ Dcong(e;z;u;z';u'))
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 (FLemma `Dcong-iff-cong` [10] THENA Auto)
    THEN (FLemma `Dcong-iff-cong` [11] THENA Auto)
    THEN (FLemma `Dcong-iff-cong` [12] THENA Auto)
    THEN (FLemma `Dcong-iff-cong` [13] THENA Auto))
   THEN Assert ⌜zu ≅ z'u'⌝⋅
   ) }

1
.....assertion..... 
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. x' : Point
6. y' : Point
7. z' : Point
8. u : Point
9. u' : Point
10. Dcong(e;x;y;x';y')
11. Dcong(e;y;z;y';z')
12. Dcong(e;x;u;x';u')
13. Dcong(e;y;u;y';u')
14. Dbet(e;x;y;z)
15. Dsep(e;x;y)
16. Dsep(e;y;z)
17. Dbet(e;x';y';z')
18. Dsep(e;x';y')
19. Dsep(e;y';z')
20. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
21. xy ≅ x'y'
22. yz ≅ y'z'
23. xu ≅ x'u'
24. yu ≅ y'u'
⊢ zu ≅ z'u'

2
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. z : Point
5. x' : Point
6. y' : Point
7. z' : Point
8. u : Point
9. u' : Point
10. Dcong(e;x;y;x';y')
11. Dcong(e;y;z;y';z')
12. Dcong(e;x;u;x';u')
13. Dcong(e;y;u;y';u')
14. Dbet(e;x;y;z)
15. Dsep(e;x;y)
16. Dsep(e;y;z)
17. Dbet(e;x';y';z')
18. Dsep(e;x';y')
19. Dsep(e;y';z')
20. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
21. xy ≅ x'y'
22. yz ≅ y'z'
23. xu ≅ x'u'
24. yu ≅ y'u'
25. zu ≅ z'u'
⊢ Dcong(e;z;u;z';u')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}x,y,z,x',y',z',u,u':Point.
    (Dcong(e;x;y;x';y')
    {}\mRightarrow{}  Dcong(e;y;z;y';z')
    {}\mRightarrow{}  Dcong(e;x;u;x';u')
    {}\mRightarrow{}  Dcong(e;y;u;y';u')
    {}\mRightarrow{}  (Dbet(e;x;y;z)  \mwedge{}  Dsep(e;x;y)  \mwedge{}  Dsep(e;y;z))
    {}\mRightarrow{}  (Dbet(e;x';y';z')  \mwedge{}  Dsep(e;x';y')  \mwedge{}  Dsep(e;y';z'))
    {}\mRightarrow{}  Dcong(e;z;u;z';u'))


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  (FLemma  `Dcong-iff-cong`  [10]  THENA  Auto)
    THEN  (FLemma  `Dcong-iff-cong`  [11]  THENA  Auto)
    THEN  (FLemma  `Dcong-iff-cong`  [12]  THENA  Auto)
    THEN  (FLemma  `Dcong-iff-cong`  [13]  THENA  Auto))
  THEN  Assert  \mkleeneopen{}zu  \mcong{}  z'u'\mkleeneclose{}\mcdot{}
  )

---

Home Index