---

Step * 1 of Lemma Euclid-erect-perp


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
BY
{ ((InstLemma `implies-right-angle` [⌜e⌝;⌜p⌝;⌜c⌝;⌜d⌝;⌜d'⌝]⋅ THENA EAuto 1)
   THEN (Assert ⌜p ≠ c⌝⋅ THENM ((RWO "geo-perp-in-iff" 0 THEN Auto) THEN InstConcl [⌜d⌝;⌜p⌝]⋅ THEN EAuto 1))
   ) }

1
.....assertion..... 
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. Rpcd
⊢ p ≠ c

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  a  \mneq{}  b
5.  c  :  Point
6.  Colinear(a;b;c)
7.  d  :  Point
8.  Colinear(a;b;d)
9.  c  \mneq{}  d
10.  d'  :  Point
11.  d=c=d'
12.  d  \mneq{}  d'
13.  p  :  Point
14.  EQ\mDelta{}(p;d';d)
\mvdash{}  ab    \mbot{}c  pc


By

---

Latex:
((InstLemma  `implies-right-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  (Assert  \mkleeneopen{}p  \mneq{}  c\mkleeneclose{}\mcdot{}
            THENM  ((RWO  "geo-perp-in-iff"  0  THEN  Auto)  THEN  InstConcl  [\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
            )
  )

---

Home Index