---

Step * of Lemma geo-perp-colinear

∀e:EuclideanPlane. ∀a,b,c,x,y:Point.  (b ≠ a ⇒ c ≠ b ⇒ Colinear(a;b;c) ⇒ bc ⊥ xy ⇒ ab ⊥ xy)
BY
{ (Auto THEN RepeatFor 4 (ParallelLast)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. b ≠ a
8. c ≠ b
9. Colinear(a;b;c)
10. x@0 : Point
11. Colinear(x;y;x@0) ∧ (∀u,v:Point.  (Colinear(b;c;u) ⇒ Colinear(x;y;v) ⇒ Rux@0v))
12. Colinear(b;c;x@0)
⊢ Colinear(a;b;x@0)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. b ≠ a
8. c ≠ b
9. Colinear(a;b;c)
10. x@0 : Point
11. Colinear(b;c;x@0)
12. Colinear(x;y;x@0) ∧ (∀u,v:Point.  (Colinear(b;c;u) ⇒ Colinear(x;y;v) ⇒ Rux@0v))
⊢ Colinear(x;y;x@0) ∧ (∀u,v:Point.  (Colinear(a;b;u) ⇒ Colinear(x;y;v) ⇒ Rux@0v))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.    (b  \mneq{}  a  {}\mRightarrow{}  c  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  bc  \mbot{}  xy  {}\mRightarrow{}  ab  \mbot{}  xy)


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast))

---

Home Index