---

Step * of Lemma geo-perp-is-shortest-path

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (a # bc ⇒ ad  ⊥d bc ⇒ (∀x:{x:Point| Colinear(b;c;x)} . (d ≠ x ⇒ |ad| < |ax|)))
BY
{ (Auto THEN (Assert a # dx BY ((InstLemma `geo-sep-or` [⌜e⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THEN Auto) THEN D -1))) }

1
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. ad  ⊥d bc
8. x : {x:Point| Colinear(b;c;x)} 
9. d ≠ x
10. b ≠ d
⊢ a # dx

2
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. ad  ⊥d bc
8. x : {x:Point| Colinear(b;c;x)} 
9. d ≠ x
10. c ≠ d
⊢ a # dx

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. ad  ⊥d bc
8. x : {x:Point| Colinear(b;c;x)} 
9. d ≠ x
10. a # dx
⊢ |ad| < |ax|

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (a  \#  bc  {}\mRightarrow{}  ad    \mbot{}d  bc  {}\mRightarrow{}  (\mforall{}x:\{x:Point|  Colinear(b;c;x)\}  .  (d  \mneq{}  x  {}\mRightarrow{}  |ad|  <  |ax|)))


By

---

Latex:
(Auto  THEN  (Assert  a  \#  dx  BY  ((InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1)))

---

Home Index