Step
*
1
2
1
1
2
1
2
1
1
of Lemma
Euclid-Prop24
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. edf < bac
13. a' : Point
14. x' : Point
15. z' : Point
16. eda' ≅a bac
17. x'-z'-a'
18. out(d ex')
19. out(d fz')
20. g : Point
21. dg ≅ df
22. out(d ga')
23. f # dg
24. x : Point
25. f=x=g
26. s : Point
27. e-s-g
28. out(d z's)
29. x'dz' ≅a eds
30. a'dz' ≅a gds
31. out(d fs)
32. t : Point
33. s-t-g
34. out(d xt)
35. fdx ≅a sdt
36. gdx ≅a gdt
37. tf ≅ tg
38. ∃f':Point. (out(e f's) ∧ ef' ≅ ef)
39. eg > ef ⇒ bc > ef
⊢ bc > ef
BY
{ ((Assert e-t-g BY
(((D 0 THEN Auto) THEN (Assert e_s_t BY Auto)) THEN Auto))
THEN (Assert f # eg ⇐⇒ f # tg BY
RepeatFor 2 ((D 0 THENA Auto)))
) }
1
.....aux.....
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. edf < bac
13. a' : Point
14. x' : Point
15. z' : Point
16. eda' ≅a bac
17. x'-z'-a'
18. out(d ex')
19. out(d fz')
20. g : Point
21. dg ≅ df
22. out(d ga')
23. f # dg
24. x : Point
25. f=x=g
26. s : Point
27. e-s-g
28. out(d z's)
29. x'dz' ≅a eds
30. a'dz' ≅a gds
31. out(d fs)
32. t : Point
33. s-t-g
34. out(d xt)
35. fdx ≅a sdt
36. gdx ≅a gdt
37. tf ≅ tg
38. ∃f':Point. (out(e f's) ∧ ef' ≅ ef)
39. eg > ef ⇒ bc > ef
40. e-t-g
41. f # eg
⊢ f # tg
2
.....aux.....
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. edf < bac
13. a' : Point
14. x' : Point
15. z' : Point
16. eda' ≅a bac
17. x'-z'-a'
18. out(d ex')
19. out(d fz')
20. g : Point
21. dg ≅ df
22. out(d ga')
23. f # dg
24. x : Point
25. f=x=g
26. s : Point
27. e-s-g
28. out(d z's)
29. x'dz' ≅a eds
30. a'dz' ≅a gds
31. out(d fs)
32. t : Point
33. s-t-g
34. out(d xt)
35. fdx ≅a sdt
36. gdx ≅a gdt
37. tf ≅ tg
38. ∃f':Point. (out(e f's) ∧ ef' ≅ ef)
39. eg > ef ⇒ bc > ef
40. e-t-g
41. f # tg
⊢ f # eg
3
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. edf < bac
13. a' : Point
14. x' : Point
15. z' : Point
16. eda' ≅a bac
17. x'-z'-a'
18. out(d ex')
19. out(d fz')
20. g : Point
21. dg ≅ df
22. out(d ga')
23. f # dg
24. x : Point
25. f=x=g
26. s : Point
27. e-s-g
28. out(d z's)
29. x'dz' ≅a eds
30. a'dz' ≅a gds
31. out(d fs)
32. t : Point
33. s-t-g
34. out(d xt)
35. fdx ≅a sdt
36. gdx ≅a gdt
37. tf ≅ tg
38. ∃f':Point. (out(e f's) ∧ ef' ≅ ef)
39. eg > ef ⇒ bc > ef
40. e-t-g
41. f # eg ⇐⇒ f # tg
⊢ bc > ef
Latex:
Latex:
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a \# bc
9. d \# ef
10. ab \mcong{} de
11. ac \mcong{} df
12. edf < bac
13. a' : Point
14. x' : Point
15. z' : Point
16. eda' \mcong{}\msuba{} bac
17. x'-z'-a'
18. out(d ex')
19. out(d fz')
20. g : Point
21. dg \mcong{} df
22. out(d ga')
23. f \# dg
24. x : Point
25. f=x=g
26. s : Point
27. e-s-g
28. out(d z's)
29. x'dz' \mcong{}\msuba{} eds
30. a'dz' \mcong{}\msuba{} gds
31. out(d fs)
32. t : Point
33. s-t-g
34. out(d xt)
35. fdx \mcong{}\msuba{} sdt
36. gdx \mcong{}\msuba{} gdt
37. tf \mcong{} tg
38. \mexists{}f':Point. (out(e f's) \mwedge{} ef' \mcong{} ef)
39. eg > ef {}\mRightarrow{} bc > ef
\mvdash{} bc > ef
By
Latex:
((Assert e-t-g BY
(((D 0 THEN Auto) THEN (Assert e\_s\_t BY Auto)) THEN Auto))
THEN (Assert f \# eg \mLeftarrow{}{}\mRightarrow{} f \# tg BY
RepeatFor 2 ((D 0 THENA Auto)))
)
Home
Index