---

Step * of Lemma Euclid-erect-perp

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:{c:Point| Colinear(a;b;c)} .  (∃p:Point [(ab  ⊥c pc ∧ p # ab)])
BY
{ (Auto
   THEN (Assert ∃d:Point. (Colinear(a;b;d) ∧ c ≠ d) BY
               ((InstLemma `geo-sep-or` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)
                THEN (D -1 THENL [D 0 With ⌜a⌝ ; D 0 With ⌜b⌝ ])
                THEN Auto))
   THEN ExRepD
   THEN DSetVars
   THEN gSymmetricPoint ⌜c⌝ ⌜d⌝ `d\''⋅
   THEN (Assert d ≠ d' BY
               (D -1 THEN Auto))
   THEN (InstLemma `Euclid-Prop1` [⌜e⌝;⌜d⌝;⌜d'⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `p' (-2)
   THEN D 0 With ⌜p⌝ 
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a ≠ b
5. c : Point
6. Colinear(a;b;c)
7. d : Point
8. Colinear(a;b;d)
9. c ≠ d
10. d' : Point
11. d=c=d'
12. d ≠ d'
13. p : Point
14. EQΔ(p;d';d)
⊢ ab  ⊥c pc

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a ≠ b
5. c : Point
6. Colinear(a;b;c)
7. d : Point
8. Colinear(a;b;d)
9. c ≠ d
10. d' : Point
11. d=c=d'
12. d ≠ d'
13. p : Point
14. EQΔ(p;d';d)
15. ab  ⊥c pc
⊢ p # ab

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}d:Point.  (Colinear(a;b;d)  \mwedge{}  c  \mneq{}  d)  BY
                          ((InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (D  -1  THENL  [D  0  With  \mkleeneopen{}a\mkleeneclose{}  ;  D  0  With  \mkleeneopen{}b\mkleeneclose{}  ])
                            THEN  Auto))
  THEN  ExRepD
  THEN  DSetVars
  THEN  gSymmetricPoint  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}d\mkleeneclose{}  `d\mbackslash{}''\mcdot{}
  THEN  (Assert  d  \mneq{}  d'  BY
                          (D  -1  THEN  Auto))
  THEN  (InstLemma  `Euclid-Prop1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `p'  (-2)
  THEN  D  0  With  \mkleeneopen{}p\mkleeneclose{} 
  THEN  Auto)

---

Home Index