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


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


Latex:


Latex:

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


By


Latex:
Auto




Home Index