---

Step * of Lemma greatest-cevian-is-farthest-from-perp

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (a # bc ⇒ ad  ⊥d bc ⇒ (∀x,y:{x:Point| Colinear(b;c;x)} .  (d-x-y ⇒ |ax| < |ay|)))
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. y : {x:Point| Colinear(b;c;x)} 
10. d-x-y
11. 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. y : {x:Point| Colinear(b;c;x)} 
10. d-x-y
11. 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. y : {x:Point| Colinear(b;c;x)} 
10. d-x-y
11. a # dx
⊢ |ax| < |ay|

---

Latex:

---

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


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