---

Step * 1 1 1 1 1 1 1 of Lemma Euclid-parallel-exists


1. e : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. p : Point
6. z : Point
7. u : Point
8. u ≠ p
9. q : Point
10. Colinear(u;z;p)
11. xy  ⊥u uz
12. z # xy
13. z ≠ p
14. zp  ⊥p qp
15. q # zp
16. sep : p ≠ q
17. ∃a,b,c,d,v:Point
     ∃sab:a ≠ b
      ∃scd:c ≠ d
       ((<p, q, sep> = <a, b, sab> ∈ LINE)
       ∧ (<x, y, l2> = <c, d, scd> ∈ LINE)
       ∧ a-v-b
       ∧ c-v-d
       ∧ a leftof cd
       ∧ b leftof dc
       ∧ c leftof ba
       ∧ d leftof ab)
⊢ False
BY
{ (ExRepD
   THEN (EqTypeHD (-8) THENA Auto)
   THEN (FLemma `geo-line-eq-to-col` [-8] THENA Auto)
   THEN Reduce -1
   THEN (EqTypeHD (-8) THENA Auto)
   THEN (FLemma `geo-line-eq-to-col` [-9] THENA Auto)
   THEN Reduce -1) }

1
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. p : Point
6. z : Point
7. u : Point
8. u ≠ p
9. q : Point
10. Colinear(u;z;p)
11. xy  ⊥u uz
12. z # xy
13. z ≠ p
14. zp  ⊥p qp
15. q # zp
16. sep : p ≠ q
17. a : Point
18. b : Point
19. c : Point
20. d : Point
21. v : Point
22. sab : a ≠ b
23. scd : c ≠ d
24. <p, q, sep> = <a, b, sab> ∈ (l,m:Line//l ≡ m)
25. <p, q, sep> ∈ Line
26. <a, b, sab> ∈ Line
27. <p, q, sep> ≡ <a, b, sab>
28. <x, y, l2> = <c, d, scd> ∈ (l,m:Line//l ≡ m)
29. <x, y, l2> ∈ Line
30. <c, d, scd> ∈ Line
31. <x, y, l2> ≡ <c, d, scd>
32. a-v-b
33. c-v-d
34. a leftof cd
35. b leftof dc
36. c leftof ba
37. d leftof ab
38. Colinear(p;q;a)
39. Colinear(p;q;b)
40. Colinear(x;y;c) ∧ Colinear(x;y;d)
⊢ False

2
1. e : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. p : Point
6. z : Point
7. u : Point
8. u ≠ p
9. q : Point
10. Colinear(u;z;p)
11. xy  ⊥u uz
12. z # xy
13. z ≠ p
14. zp  ⊥p qp
15. q # zp
16. sep : p ≠ q
17. a : Point
18. b : Point
19. c : Point
20. d : Point
21. v : Point
22. sab : a ≠ b
23. scd : c ≠ d
24. <p, q, sep> = <a, b, sab> ∈ (l,m:Line//l ≡ m)
25. <p, q, sep> ∈ Line
26. <a, b, sab> ∈ Line
27. <p, q, sep> ≡ <a, b, sab>
28. a-v-b
29. c-v-d
30. a leftof cd
31. b leftof dc
32. c leftof ba
33. d leftof ab
34. Colinear(p;q;a)
35. Colinear(p;q;b)
36. Colinear(p;q;a) ∧ Colinear(p;q;b)
⊢ istype((<x, y, l2> ∈ Line) ∧ (<c, d, scd> ∈ Line) ∧ <x, y, l2> ≡ <c, d, scd>)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  Point
3.  y  :  Point
4.  l2  :  x  \mneq{}  y
5.  p  :  Point
6.  z  :  Point
7.  u  :  Point
8.  u  \mneq{}  p
9.  q  :  Point
10.  Colinear(u;z;p)
11.  xy    \mbot{}u  uz
12.  z  \#  xy
13.  z  \mneq{}  p
14.  zp    \mbot{}p  qp
15.  q  \#  zp
16.  sep  :  p  \mneq{}  q
17.  \mexists{}a,b,c,d,v:Point
          \mexists{}sab:a  \mneq{}  b
            \mexists{}scd:c  \mneq{}  d
              ((<p,  q,  sep>  =  <a,  b,  sab>)
              \mwedge{}  (<x,  y,  l2>  =  <c,  d,  scd>)
              \mwedge{}  a-v-b
              \mwedge{}  c-v-d
              \mwedge{}  a  leftof  cd
              \mwedge{}  b  leftof  dc
              \mwedge{}  c  leftof  ba
              \mwedge{}  d  leftof  ab)
\mvdash{}  False


By

---

Latex:
(ExRepD
  THEN  (EqTypeHD  (-8)  THENA  Auto)
  THEN  (FLemma  `geo-line-eq-to-col`  [-8]  THENA  Auto)
  THEN  Reduce  -1
  THEN  (EqTypeHD  (-8)  THENA  Auto)
  THEN  (FLemma  `geo-line-eq-to-col`  [-9]  THENA  Auto)
  THEN  Reduce  -1)

---

Home Index