Step * 1 1 1 3 2 1 1 of Lemma geo-lt-add1-iff2

.....aux..... 
1. BasicGeometry
2. a1 Point
3. a2 Point
4. b1 Point
5. b2 Point
6. c1 Point
7. c2 Point
8. Point
9. Point
10. b
11. p' Point
12. B(OXp')
13. q' {p:Point| B(OXp)} 
14. p' |a1a2| |ab| ∈ Length
15. q' |b1b2| ∈ Length
16. B(Xp'q')
17. b
18. p'
19. q'
20. Point
21. B(Xp'P)
22. p'P ≅ c1c2
23. Point
24. B(Xq'Q)
25. q'Q ≅ c1c2
26. |a1a2| |c1c2| |ab| ∈ Length
27. |b1b2| |c1c2| ∈ Length
28. q'
29. B(Xq'P)
30. Q
31. B(XQP)
32. Q <  (Q ≤ P ∧ P)
33. Q <  Q ≤ P ∧ P
⊢ False
BY
(D -1 THEN Auto) }

1
1. BasicGeometry
2. a1 Point
3. a2 Point
4. b1 Point
5. b2 Point
6. c1 Point
7. c2 Point
8. Point
9. Point
10. b
11. p' Point
12. B(OXp')
13. q' {p:Point| B(OXp)} 
14. p' |a1a2| |ab| ∈ Length
15. q' |b1b2| ∈ Length
16. B(Xp'q')
17. b
18. p'
19. q'
20. Point
21. B(Xp'P)
22. p'P ≅ c1c2
23. Point
24. B(Xq'Q)
25. q'Q ≅ c1c2
26. |a1a2| |c1c2| |ab| ∈ Length
27. |b1b2| |c1c2| ∈ Length
28. q'
29. B(Xq'P)
30. Q
31. B(XQP)
32. Q <  (Q ≤ P ∧ P)
⊢ Q ≤ P

2
1. BasicGeometry
2. a1 Point
3. a2 Point
4. b1 Point
5. b2 Point
6. c1 Point
7. c2 Point
8. Point
9. Point
10. b
11. p' Point
12. B(OXp')
13. q' {p:Point| B(OXp)} 
14. p' |a1a2| |ab| ∈ Length
15. q' |b1b2| ∈ Length
16. B(Xp'q')
17. b
18. p'
19. q'
20. Point
21. B(Xp'P)
22. p'P ≅ c1c2
23. Point
24. B(Xq'Q)
25. q'Q ≅ c1c2
26. |a1a2| |c1c2| |ab| ∈ Length
27. |b1b2| |c1c2| ∈ Length
28. q'
29. B(Xq'P)
30. Q
31. B(XQP)
32. Q < P
33. Q ≤ P
34. P
⊢ False


Latex:


Latex:
.....aux..... 
1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  a  :  Point
9.  b  :  Point
10.  a  \#  b
11.  p'  :  Point
12.  B(OXp')
13.  q'  :  \{p:Point|  B(OXp)\} 
14.  p'  =  |a1a2|  +  |ab|
15.  q'  =  |b1b2|
16.  B(Xp'q')
17.  a  \#  b
18.  X  \#  p'
19.  X  \#  q'
20.  P  :  Point
21.  B(Xp'P)
22.  p'P  \mcong{}  c1c2
23.  Q  :  Point
24.  B(Xq'Q)
25.  q'Q  \mcong{}  c1c2
26.  P  =  |a1a2|  +  |c1c2|  +  |ab|
27.  Q  =  |b1b2|  +  |c1c2|
28.  P  \#  q'
29.  B(Xq'P)
30.  P  \#  Q
31.  B(XQP)
32.  Q  <  P  {}\mRightarrow{}  (Q  \mleq{}  P  \mwedge{}  Q  \#  P)
33.  Q  <  P  \mLeftarrow{}{}  Q  \mleq{}  P  \mwedge{}  Q  \#  P
\mvdash{}  False


By


Latex:
(D  -1  THEN  Auto)




Home Index