---

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


1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof pq ∧ y leftof qp)
18. a # b
∧ p # q
∧ (∃a1,b1,c,d,v:Point
    (a1-v-b1
    ∧ c-v-d
    ∧ Colinear(a1;a;b)
    ∧ Colinear(b1;a;b)
    ∧ Colinear(c;p;q)
    ∧ Colinear(d;p;q)
    ∧ a1 leftof cd
    ∧ b1 leftof dc
    ∧ c leftof b1a1
    ∧ d leftof a1b1))
⊢ False
BY
{ (ExRepD THEN (InstLemma `right-angles-not-complementary` [⌜e⌝;⌜v⌝;⌜u⌝;⌜p⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. x : {z:Point| Colinear(z;a;b)} 
18. y : {z:Point| Colinear(z;a;b)} 
19. x leftof pq
20. y leftof qp
21. a # b
22. p # q
23. a1 : Point
24. b1 : Point
25. c : Point
26. d : Point
27. v : Point
28. a1-v-b1
29. c-v-d
30. Colinear(a1;a;b)
31. Colinear(b1;a;b)
32. Colinear(c;p;q)
33. Colinear(d;p;q)
34. a1 leftof cd
35. b1 leftof dc
36. c leftof b1a1
37. d leftof a1b1
⊢ Rvpu

2
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. p : Point
5. z : Point
6. u : Point
7. q : Point
8. Colinear(u;z;p)
9. ab  ⊥u uz
10. z # ab
11. z # p
12. zp  ⊥p qp
13. q # zp
14. a # b
15. p # q
16. u # p
17. x : {z:Point| Colinear(z;a;b)} 
18. y : {z:Point| Colinear(z;a;b)} 
19. x leftof pq
20. y leftof qp
21. a # b
22. p # q
23. a1 : Point
24. b1 : Point
25. c : Point
26. d : Point
27. v : Point
28. a1-v-b1
29. c-v-d
30. Colinear(a1;a;b)
31. Colinear(b1;a;b)
32. Colinear(c;p;q)
33. Colinear(d;p;q)
34. a1 leftof cd
35. b1 leftof dc
36. c leftof b1a1
37. d leftof a1b1
38. u ≡ p
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \#  b\} 
4.  p  :  Point
5.  z  :  Point
6.  u  :  Point
7.  q  :  Point
8.  Colinear(u;z;p)
9.  ab    \mbot{}u  uz
10.  z  \#  ab
11.  z  \#  p
12.  zp    \mbot{}p  qp
13.  q  \#  zp
14.  a  \#  b
15.  p  \#  q
16.  u  \#  p
17.  \mexists{}x,y:\{z:Point|  Colinear(z;a;b)\}  .  (x  leftof  pq  \mwedge{}  y  leftof  qp)
18.  a  \#  b
\mwedge{}  p  \#  q
\mwedge{}  (\mexists{}a1,b1,c,d,v:Point
        (a1-v-b1
        \mwedge{}  c-v-d
        \mwedge{}  Colinear(a1;a;b)
        \mwedge{}  Colinear(b1;a;b)
        \mwedge{}  Colinear(c;p;q)
        \mwedge{}  Colinear(d;p;q)
        \mwedge{}  a1  leftof  cd
        \mwedge{}  b1  leftof  dc
        \mwedge{}  c  leftof  b1a1
        \mwedge{}  d  leftof  a1b1))
\mvdash{}  False


By

---

Latex:
(ExRepD  THEN  (InstLemma  `right-angles-not-complementary`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index