Metamath Proof Explorer

Table of Contents - 21.3.12. Constructible Numbers

This section defines the set of constructible points as complex numbers which can be drawn starting from two points (we take and ), and taking intersections of circles and lines.

This construction is useful for proving the impossibility of doubling the cube (2sqr3nconstr), and of angle trisection (cos9thpinconstr)

1. cconstr
2. df-constr
3. constrrtll
4. constrrtlc1
5. constrrtlc2
6. constrrtcclem
7. constrrtcc
8. isconstr
9. constr0
10. constrsuc
11. constrlim
12. constrsscn
13. constrsslem
14. constr01
15. constrss
16. constrmon
17. constrconj
18. constrfin
19. constrelextdg2
20. constrextdg2lem
21. constrextdg2
22. constrext2chnlem
23. constrfiss
24. constrllcllem
25. constrlccllem
26. constrcccllem
27. constrcbvlem
28. constrllcl
29. constrlccl
30. constrcccl
31. constrext2chn
32. constrcn
33. nn0constr
34. constraddcl
35. constrnegcl
36. zconstr
37. constrdircl
38. iconstr
39. constrremulcl
40. constrcjcl
41. constrrecl
42. constrimcl
43. constrmulcl
44. constrreinvcl
45. constrinvcl
46. constrcon
47. constrsdrg
48. constrfld
49. constrresqrtcl
50. constrabscl
51. constrsqrtcl
52. Impossible constructions
    1. 2sqr3minply
    2. 2sqr3nconstr
    3. cos9thpiminplylem1
    4. cos9thpiminplylem2
    5. cos9thpiminplylem3
    6. cos9thpiminplylem4
    7. cos9thpiminplylem5
    8. cos9thpiminplylem6
    9. cos9thpiminply
    10. cos9thpinconstrlem1
    11. cos9thpinconstrlem2
    12. cos9thpinconstr
    13. trisecnconstr