Step
*
1
2
1
1
2
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. (((s-t-g ∧ out(d xt)) ∧ fdx ≅a sdt) ∧ gdx ≅a gdt)
⊢ bc > ef
BY
{ (ExRepD THEN Assert ⌜tf ≅ tg⌝⋅) }
1
.....assertion.....
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
⊢ tf ≅ tg
2
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
⊢ 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. \mexists{}t:Point. (((s-t-g \mwedge{} out(d xt)) \mwedge{} fdx \mcong{}\msuba{} sdt) \mwedge{} gdx \mcong{}\msuba{} gdt)
\mvdash{} bc > ef
By
Latex:
(ExRepD THEN Assert \mkleeneopen{}tf \mcong{} tg\mkleeneclose{}\mcdot{})
Home
Index