---

Step * of Lemma isosceles-sep-implies-lsep

∀e:EuclideanPlane. ∀a,b,x:Point.  (xa ≅ xb ⇒ a ≠ b ⇒ (∀m:{m:Point| a=m=b} . m ≠ x) ⇒ x # ab)
BY
{ (Auto
   THEN (InstLemma  `Euclid-midpoint` [⌜e⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (FLemma  `midpoint-sep` [-1] THENA Auto)
   THEN (InstHyp [⌜d⌝] (7)⋅ THENA Auto)
   THEN ((InstLemma  `Euclid-erect-2perp` [⌜e⌝;⌜a⌝;⌜b⌝;⌜d⌝]⋅ THEN Auto) THEN ExRepD)
   THEN (Assert Colinear(x;p;d) BY
               (InstLemma  `upper-dimension-axiom` [⌜e⌝;⌜x⌝;⌜p⌝;⌜d⌝;⌜a⌝;⌜b⌝]⋅ THEN EAuto 1))) }

1
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. xa ≅ xb
6. a ≠ b
7. ∀m:{m:Point| a=m=b} . m ≠ x
8. d : Point
9. a=d=b
10. a ≠ d
11. b ≠ d
12. d ≠ x
13. q : Point
14. p : Point
15. ab  ⊥d pd
16. ab  ⊥d qd
17. p leftof ab
18. q leftof ba
⊢ pa ≅ pb

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. xa ≅ xb
6. a ≠ b
7. ∀m:{m:Point| a=m=b} . m ≠ x
8. d : Point
9. a=d=b
10. a ≠ d
11. b ≠ d
12. d ≠ x
13. q : Point
14. p : Point
15. ab  ⊥d pd
16. ab  ⊥d qd
17. p leftof ab
18. q leftof ba
19. Colinear(x;p;d)
⊢ x # ab

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x:Point.    (xa  \mcong{}  xb  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  (\mforall{}m:\{m:Point|  a=m=b\}  .  m  \mneq{}  x)  {}\mRightarrow{}  x  \#  ab)


By

---

Latex:
(Auto
  THEN  (InstLemma    `Euclid-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (FLemma    `midpoint-sep`  [-1]  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}d\mkleeneclose{}]  (7)\mcdot{}  THENA  Auto)
  THEN  ((InstLemma    `Euclid-erect-2perp`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
  THEN  (Assert  Colinear(x;p;d)  BY
                          (InstLemma    `upper-dimension-axiom`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)))

---

Home Index