---

Step * of Lemma eu-eq_dist-axiomA9

∀e:EuclideanPlane. ∀a1,a2,a3,a4,a5,a6,b:Point.  (D(a1;a2;a3;a4;a5;a6) ⇒ (a4 ≠ b ∨ D(a1;a2;a3;b;a5;a6)))
BY
{ (Auto
   THEN (FLemma `dist-lemma-lt` [-1] THEN Auto)
   THEN (Assert |a5a6| ≠ |a1a2| + |a3a4| BY
               (InstLemma `geo-sep-iff-or-lt` [⌜e⌝;⌜|a5a6|⌝;⌜|a1a2| + |a3a4|⌝]⋅ THEN Auto))
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜|a5a6|⌝;⌜|a1a2| + |a3a4|⌝;⌜|a1a2| + |a3b|⌝]⋅ THENA Auto)
   THEN D -1) }

1
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. a3 : Point
5. a4 : Point
6. a5 : Point
7. a6 : Point
8. b : Point
9. D(a1;a2;a3;a4;a5;a6)
10. |a5a6| < |a1a2| + |a3a4|
11. |a5a6| ≠ |a1a2| + |a3a4|
12. |a5a6| ≠ |a1a2| + |a3b|
⊢ a4 ≠ b ∨ D(a1;a2;a3;b;a5;a6)

2
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. a3 : Point
5. a4 : Point
6. a5 : Point
7. a6 : Point
8. b : Point
9. D(a1;a2;a3;a4;a5;a6)
10. |a5a6| < |a1a2| + |a3a4|
11. |a5a6| ≠ |a1a2| + |a3a4|
12. |a1a2| + |a3a4| ≠ |a1a2| + |a3b|
⊢ a4 ≠ b ∨ D(a1;a2;a3;b;a5;a6)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a1,a2,a3,a4,a5,a6,b:Point.
    (D(a1;a2;a3;a4;a5;a6)  {}\mRightarrow{}  (a4  \mneq{}  b  \mvee{}  D(a1;a2;a3;b;a5;a6)))


By

---

Latex:
(Auto
  THEN  (FLemma  `dist-lemma-lt`  [-1]  THEN  Auto)
  THEN  (Assert  |a5a6|  \mneq{}  |a1a2|  +  |a3a4|  BY
                          (InstLemma  `geo-sep-iff-or-lt`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}|a5a6|\mkleeneclose{};\mkleeneopen{}|a1a2|  +  |a3a4|\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}|a5a6|\mkleeneclose{};\mkleeneopen{}|a1a2|  +  |a3a4|\mkleeneclose{};\mkleeneopen{}|a1a2|  +  |a3b|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index