---

Step * of Lemma Euclid-drop-perp-0

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.
  ∃x:Point. (∃p:Point [(Colinear(p;x;c) ∧ ab  ⊥p px ∧ x # ab ∧ x # c)])
BY
{ ((Auto THEN (Assert a # b BY (DVar `b' THEN Unhide THEN Auto)))
   THEN (InstLemma `colinear-equidistant-points-exist` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (CompassCompass2 ⌜u⌝ ⌜v⌝ ⌜v⌝ ⌜u⌝ `x' `y'⋅
         THENA ((Auto THEN InstConcl [⌜v⌝;⌜u⌝]⋅ THEN Auto) THEN (Assert v # u BY Auto) THEN Auto)
         )
   THEN (Assert x # ab BY
               ((Assert x # uv BY Auto) THEN InstLemma `colinear-lsep-general` [⌜e⌝;⌜u⌝;⌜v⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto))
   THEN (Assert y # ab BY
               ((Assert y # uv BY Auto) THEN InstLemma `colinear-lsep-general` [⌜e⌝;⌜u⌝;⌜v⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto))
   THEN (Assert x # y BY
               (Auto THEN EasyGeometry))
   THEN InstLemma `geo-sep-or` [⌜e⌝;⌜x⌝;⌜y⌝;⌜c⌝]⋅
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. a # b
6. u : Point
7. v : Point
8. Colinear(a;b;u)
9. Colinear(a;b;v)
10. u # v
11. cu ≅ cv
12. x : Point
13. y : Point
14. ux ≅ uv
15. uy ≅ uv
16. vx ≅ vu
17. vy ≅ vu
18. x leftof uv
19. y leftof vu
20. x # ab
21. y # ab
22. x # y
23. x # c ∨ y # c
⊢ ∃x:Point. (∃p:Point [(Colinear(p;x;c) ∧ ab  ⊥p px ∧ x # ab ∧ x # c)])

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:Point.
    \mexists{}x:Point.  (\mexists{}p:Point  [(Colinear(p;x;c)  \mwedge{}  ab    \mbot{}p  px  \mwedge{}  x  \#  ab  \mwedge{}  x  \#  c)])


By

---

Latex:
((Auto  THEN  (Assert  a  \#  b  BY  (DVar  `b'  THEN  Unhide  THEN  Auto)))
  THEN  (InstLemma  `colinear-equidistant-points-exist`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (CompassCompass2  \mkleeneopen{}u\mkleeneclose{}  \mkleeneopen{}v\mkleeneclose{}  \mkleeneopen{}v\mkleeneclose{}  \mkleeneopen{}u\mkleeneclose{}  `x'  `y'\mcdot{}
              THENA  ((Auto  THEN  InstConcl  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  (Assert  v  \#  u  BY  Auto)  THEN  Auto)
              )
  THEN  (Assert  x  \#  ab  BY
                          ((Assert  x  \#  uv  BY
                                          Auto)
                            THEN  InstLemma  `colinear-lsep-general`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (Assert  y  \#  ab  BY
                          ((Assert  y  \#  uv  BY
                                          Auto)
                            THEN  InstLemma  `colinear-lsep-general`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (Assert  x  \#  y  BY
                          (Auto  THEN  EasyGeometry))
  THEN  InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index