Step
*
1
3
1
1
of Lemma
geo-lt-add1_2
1. e : BasicGeometry
2. p : {a:Point| O_X_a}
3. q : {a:Point| O_X_a}
4. r : {a:Point| O_X_a}
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p}
12. q' : {p:Point| O_X_p}
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1
19. rp1 ≅ Xp'
20. q1 : Point
21. X-r-q1
22. rq1 ≅ Xq'
23. p1 = p + r + |ab| ∈ Length
24. q1 = q + r ∈ Length
25. p' ≤ q'
26. X_p'_q'
27. Colinear(X;p1;q1)
⊢ X_p1_q1
BY
{ (gColinearCases (-1) THENA Auto) }
1
1. e : BasicGeometry
2. p : {a:Point| O_X_a}
3. q : {a:Point| O_X_a}
4. r : {a:Point| O_X_a}
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p}
12. q' : {p:Point| O_X_p}
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1
19. rp1 ≅ Xp'
20. q1 : Point
21. X-r-q1
22. rq1 ≅ Xq'
23. p1 = p + r + |ab| ∈ Length
24. q1 = q + r ∈ Length
25. p' ≤ q'
26. X_p'_q'
27. Colinear(X;p1;q1)
28. X ≡ p1
⊢ X_p1_q1
2
1. e : BasicGeometry
2. p : {a:Point| O_X_a}
3. q : {a:Point| O_X_a}
4. r : {a:Point| O_X_a}
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p}
12. q' : {p:Point| O_X_p}
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1
19. rp1 ≅ Xp'
20. q1 : Point
21. X-r-q1
22. rq1 ≅ Xq'
23. p1 = p + r + |ab| ∈ Length
24. q1 = q + r ∈ Length
25. p' ≤ q'
26. X_p'_q'
27. Colinear(X;p1;q1)
28. p1 ≡ q1
⊢ X_p1_q1
3
1. e : BasicGeometry
2. p : {a:Point| O_X_a}
3. q : {a:Point| O_X_a}
4. r : {a:Point| O_X_a}
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p}
12. q' : {p:Point| O_X_p}
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1
19. rp1 ≅ Xp'
20. q1 : Point
21. X-r-q1
22. rq1 ≅ Xq'
23. p1 = p + r + |ab| ∈ Length
24. q1 = q + r ∈ Length
25. p' ≤ q'
26. X_p'_q'
27. Colinear(X;p1;q1)
28. q1 ≡ X
⊢ X_p1_q1
4
1. e : BasicGeometry
2. p : {a:Point| O_X_a}
3. q : {a:Point| O_X_a}
4. r : {a:Point| O_X_a}
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p}
12. q' : {p:Point| O_X_p}
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1
19. rp1 ≅ Xp'
20. q1 : Point
21. X-r-q1
22. rq1 ≅ Xq'
23. p1 = p + r + |ab| ∈ Length
24. q1 = q + r ∈ Length
25. p' ≤ q'
26. X_p'_q'
27. Colinear(X;p1;q1)
28. p1-q1-X
⊢ X_p1_q1
5
1. e : BasicGeometry
2. p : {a:Point| O_X_a}
3. q : {a:Point| O_X_a}
4. r : {a:Point| O_X_a}
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p}
12. q' : {p:Point| O_X_p}
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1
19. rp1 ≅ Xp'
20. q1 : Point
21. X-r-q1
22. rq1 ≅ Xq'
23. p1 = p + r + |ab| ∈ Length
24. q1 = q + r ∈ Length
25. p' ≤ q'
26. X_p'_q'
27. Colinear(X;p1;q1)
28. q1-X-p1
⊢ X_p1_q1
Latex:
Latex:
1. e : BasicGeometry
2. p : \{a:Point| O\_X\_a\}
3. q : \{a:Point| O\_X\_a\}
4. r : \{a:Point| O\_X\_a\}
5. X \mneq{} p
6. X \mneq{} q
7. X \mneq{} r
8. a : Point
9. b : Point
10. a \mneq{} b
11. p' : \{p:Point| O\_X\_p\}
12. q' : \{p:Point| O\_X\_p\}
13. p' = p + |ab|
14. q' = q
15. X\_p'\_q'
16. a \mneq{} b
17. p1 : Point
18. X-r-p1
19. rp1 \mcong{} Xp'
20. q1 : Point
21. X-r-q1
22. rq1 \mcong{} Xq'
23. p1 = p + r + |ab|
24. q1 = q + r
25. p' \mleq{} q'
26. X\_p'\_q'
27. Colinear(X;p1;q1)
\mvdash{} X\_p1\_q1
By
Latex:
(gColinearCases (-1) THENA Auto)
Home
Index