---

Step * 1 of Lemma geo-perp-unicity


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. u : Point
6. v : Point
7. a ≠ b
8. Colinear(a;b;u)
9. Colinear(a;b;v)
10. ab ⊥ cu
11. ab ⊥ cv
12. Colinear(a;b;c)
⊢ u ≡ v
BY
{ (Assert ab  ⊥u uc BY
         (RepeatFor 3 (D -3)
          THEN (InstHyp [⌜u⌝;⌜u⌝] (-3)⋅ THENA Auto)
          THEN (FLemma  `right-angle-legs-same` [-1] THENA Auto)
          THEN (D 0 THEN Auto)
          THEN RWO "-6<" 0
          THEN Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. u : Point
6. v : Point
7. a ≠ b
8. Colinear(a;b;u)
9. Colinear(a;b;v)
10. ab ⊥ cu
11. ab ⊥ cv
12. Colinear(a;b;c)
13. ab  ⊥u uc
⊢ u ≡ v

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  u  :  Point
6.  v  :  Point
7.  a  \mneq{}  b
8.  Colinear(a;b;u)
9.  Colinear(a;b;v)
10.  ab  \mbot{}  cu
11.  ab  \mbot{}  cv
12.  Colinear(a;b;c)
\mvdash{}  u  \mequiv{}  v


By

---

Latex:
(Assert  ab    \mbot{}u  uc  BY
              (RepeatFor  3  (D  -3)
                THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
                THEN  (FLemma    `right-angle-legs-same`  [-1]  THENA  Auto)
                THEN  (D  0  THEN  Auto)
                THEN  RWO  "-6<"  0
                THEN  Auto))

---

Home Index