---

Step * 1 1 1 1 of Lemma Euclid-Prop31


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. a # b
6. x # ab
7. z : Point
8. u : Point
9. q : Point
10. Colinear(u;z;x)
11. ab  ⊥u uz
12. z # ab
13. z # x
14. zx  ⊥x qx
15. q # zx
16. x # q
17. a # b
18. x # q
19. a # b
∧ x # q
∧ (∃a1,b1,c1,d1,v:Point
    (a1-v-b1
    ∧ c1-v-d1
    ∧ Colinear(a1;a;b)
    ∧ Colinear(b1;a;b)
    ∧ Colinear(c1;x;q)
    ∧ Colinear(d1;x;q)
    ∧ a1 leftof c1d1
    ∧ b1 leftof d1c1))
⊢ False
BY
{ (ExRepD THEN (InstLemma `right-angles-not-complementary` [⌜e⌝;⌜v⌝;⌜u⌝;⌜x⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. a # b
6. x # ab
7. z : Point
8. u : Point
9. q : Point
10. Colinear(u;z;x)
11. ab  ⊥u uz
12. z # ab
13. z # x
14. zx  ⊥x qx
15. q # zx
16. x # q
17. a # b
18. x # q
19. a # b
20. x # q
21. a1 : Point
22. b1 : Point
23. c1 : Point
24. d1 : Point
25. v : Point
26. a1-v-b1
27. c1-v-d1
28. Colinear(a1;a;b)
29. Colinear(b1;a;b)
30. Colinear(c1;x;q)
31. Colinear(d1;x;q)
32. a1 leftof c1d1
33. b1 leftof d1c1
⊢ Rvxu

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. a # b
6. x # ab
7. z : Point
8. u : Point
9. q : Point
10. Colinear(u;z;x)
11. ab  ⊥u uz
12. z # ab
13. z # x
14. zx  ⊥x qx
15. q # zx
16. x # q
17. a # b
18. x # q
19. a # b
20. x # q
21. a1 : Point
22. b1 : Point
23. c1 : Point
24. d1 : Point
25. v : Point
26. a1-v-b1
27. c1-v-d1
28. Colinear(a1;a;b)
29. Colinear(b1;a;b)
30. Colinear(c1;x;q)
31. Colinear(d1;x;q)
32. a1 leftof c1d1
33. b1 leftof d1c1
34. u ≡ x
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  x  :  Point
5.  a  \#  b
6.  x  \#  ab
7.  z  :  Point
8.  u  :  Point
9.  q  :  Point
10.  Colinear(u;z;x)
11.  ab    \mbot{}u  uz
12.  z  \#  ab
13.  z  \#  x
14.  zx    \mbot{}x  qx
15.  q  \#  zx
16.  x  \#  q
17.  a  \#  b
18.  x  \#  q
19.  a  \#  b
\mwedge{}  x  \#  q
\mwedge{}  (\mexists{}a1,b1,c1,d1,v:Point
        (a1-v-b1
        \mwedge{}  c1-v-d1
        \mwedge{}  Colinear(a1;a;b)
        \mwedge{}  Colinear(b1;a;b)
        \mwedge{}  Colinear(c1;x;q)
        \mwedge{}  Colinear(d1;x;q)
        \mwedge{}  a1  leftof  c1d1
        \mwedge{}  b1  leftof  d1c1))
\mvdash{}  False


By

---

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

---

Home Index