---

Step * 1 1 1 2 1 1 of Lemma isosc-colinear-mid-exists


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c ≠ a
12. c ≠ a'
13. c ≠ b
14. c ≠ b'
15. a=m=b
16. a'c ≅ b'c
17. a' # cb'
18. x : Point
19. a'=x=b'
20. a' # cb'
21. c ≠ x
22. c ≠ m
23. a ≠ a'
24. aa' ≅ bb'
25. ¬c_x_m
26. ¬c_m_x
27. c_a'_a
28. c_b_b'
29. |cb'| = |cb| + |bb'| ∈ Length
30. |ca| = |ca'| + |a'a| ∈ Length
⊢ False
BY
{ ((Subst' |cb'| = |ca'| ∈ Length -2 THENA Auto)
   THEN (Subst' |cb| + |bb'| = |ca| + |bb'| ∈ Length -2 THENA Auto)
   THEN (Subst' |ca'| + |a'a| = |ca| + |bb'| + |a'a| ∈ Length -1 THENA Auto)) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c ≠ a
12. c ≠ a'
13. c ≠ b
14. c ≠ b'
15. a=m=b
16. a'c ≅ b'c
17. a' # cb'
18. x : Point
19. a'=x=b'
20. a' # cb'
21. c ≠ x
22. c ≠ m
23. a ≠ a'
24. aa' ≅ bb'
25. ¬c_x_m
26. ¬c_m_x
27. c_a'_a
28. c_b_b'
29. |ca'| = |ca| + |bb'| ∈ Length
30. |ca| = |ca| + |bb'| + |a'a| ∈ Length
⊢ False

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  m  :  Point
6.  a'  :  Point
7.  b'  :  Point
8.  m'  :  Point
9.  c  \#  ab
10.  ac  \00D0  bc
11.  c  \mneq{}  a
12.  c  \mneq{}  a'
13.  c  \mneq{}  b
14.  c  \mneq{}  b'
15.  a=m=b
16.  a'c  \00D0  b'c
17.  a'  \#  cb'
18.  x  :  Point
19.  a'=x=b'
20.  a'  \#  cb'
21.  c  \mneq{}  x
22.  c  \mneq{}  m
23.  a  \mneq{}  a'
24.  aa'  \00D0  bb'
25.  \mneg{}c\_x\_m
26.  \mneg{}c\_m\_x
27.  c\_a'\_a
28.  c\_b\_b'
29.  |cb'|  =  |cb|  +  |bb'|
30.  |ca|  =  |ca'|  +  |a'a|
\mvdash{}  False


By

---

Latex:
((Subst'  |cb'|  =  |ca'|  -2  THENA  Auto)
  THEN  (Subst'  |cb|  +  |bb'|  =  |ca|  +  |bb'|  -2  THENA  Auto)
  THEN  (Subst'  |ca'|  +  |a'a|  =  |ca|  +  |bb'|  +  |a'a|  -1  THENA  Auto))

---

Home Index