Step
*
2
2
2
1
1
1
1
1
3
of Lemma
tarski-erect-perp-same-side
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
⊢ geo-tar-same-side(e;c;d;a;b)
BY
{ ((Unfold `geo-tar-same-side` 0 THEN InstConcl [⌜p⌝]⋅ THEN Auto) THEN Unfold `geo-tar-opp-side` 0 THEN GenRepD) }
1
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
⊢ c # ab
2
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
⊢ p # ab
3
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
⊢ ∃t:Point. (Colinear(a;b;t) ∧ B(ctp))
4
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
45. geo-tar-opp-side(e;c;p;a;b)
⊢ d # ab
5
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
45. geo-tar-opp-side(e;c;p;a;b)
⊢ p # ab
6
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa ≅ da
29. p # c2a
30. a # dp
31. c2=p1=p
32. ab ⊥a p1a
33. p1 # ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c # c'c1
38. c # x
39. c' # x
40. c1 # p
41. c' # p
42. q1 : Point
43. p-q1-c
44. x-q1-b
45. geo-tar-opp-side(e;c;p;a;b)
⊢ ∃t:Point. (Colinear(a;b;t) ∧ B(dtp))
Latex:
Latex:
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c \# ba
7. x : Point
8. Colinear(a;b;x)
9. ab \mbot{}x cx
10. b \# x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b \mcong{} cb
16. c' \# c1b
17. b \# cc'
18. c1=p=c'
19. ba \mbot{}b pb
20. p \# ba
21. d : Point
22. p-b-d
23. bd \mcong{} pb
24. c2 : Point
25. p1 : Point
26. d=a=c2
27. d=b=p
28. pa \mcong{} da
29. p \# c2a
30. a \# dp
31. c2=p1=p
32. ab \mbot{}a p1a
33. p1 \# ab
34. q : Point
35. p1-q-d
36. a-q-b
37. c \# c'c1
38. c \# x
39. c' \# x
40. c1 \# p
41. c' \# p
42. q1 : Point
43. p-q1-c
44. x-q1-b
\mvdash{} geo-tar-same-side(e;c;d;a;b)
By
Latex:
((Unfold `geo-tar-same-side` 0 THEN InstConcl [\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THEN Auto)
THEN Unfold `geo-tar-opp-side` 0
THEN GenRepD)
Home
Index