Metamath Proof Explorer

Table of Contents - 10.8. The complex numbers as an algebraic extensible structure

1. Definition and basic properties
   1. cpsmet
   2. cxmet
   3. cmet
   4. cbl
   5. cfbas
   6. cfg
   7. cmopn
   8. cmetu
   9. df-psmet
   10. df-xmet
   11. df-met
   12. df-bl
   13. df-mopn
   14. df-fbas
   15. df-fg
   16. df-metu
   17. ccnfld
   18. df-cnfld
   19. cnfldstr
   20. cnfldex
   21. cnfldbas
   22. mpocnfldadd
   23. cnfldadd
   24. mpocnfldmul
   25. cnfldmul
   26. cnfldcj
   27. cnfldtset
   28. cnfldle
   29. cnfldds
   30. cnfldunif
   31. cnfldfun
   32. cnfldfunALT
   33. dfcnfldOLD
   34. cnfldstrOLD
   35. cnfldexOLD
   36. cnfldbasOLD
   37. cnfldaddOLD
   38. cnfldmulOLD
   39. cnfldcjOLD
   40. cnfldtsetOLD
   41. cnfldleOLD
   42. cnflddsOLD
   43. cnfldunifOLD
   44. cnfldfunOLD
   45. cnfldfunALTOLD
   46. xrsstr
   47. xrsex
   48. xrsadd
   49. xrsmul
   50. xrstset
   51. cncrng
   52. cncrngOLD
   53. cnring
   54. xrsmcmn
   55. cnfld0
   56. cnfld1
   57. cnfld1OLD
   58. cnfldneg
   59. cnfldplusf
   60. cnfldsub
   61. cndrng
   62. cndrngOLD
   63. cnflddiv
   64. cnflddivOLD
   65. cnfldinv
   66. cnfldmulg
   67. cnfldexp
   68. cnsrng
   69. xrsmgm
   70. xrsnsgrp
   71. xrsmgmdifsgrp
   72. xrsds
   73. xrsdsval
   74. xrsdsreval
   75. xrsdsreclblem
   76. xrsdsreclb
   77. cnsubmlem
   78. cnsubglem
   79. cnsubrglem
   80. cnsubrglemOLD
   81. cnsubdrglem
   82. qsubdrg
   83. zsubrg
   84. gzsubrg
   85. nn0subm
   86. rege0subm
   87. absabv
   88. zsssubrg
   89. qsssubdrg
   90. cnsubrg
   91. cnmgpabl
   92. cnmgpid
   93. cnmsubglem
   94. rpmsubg
   95. gzrngunitlem
   96. gzrngunit
   97. gsumfsum
   98. regsumfsum
   99. expmhm
   100. nn0srg
   101. rge0srg
   102. xrge0plusg
   103. xrs1mnd
   104. xrs10
   105. xrs1cmn
   106. xrge0subm
   107. xrge0cmn
   108. xrge0omnd
2. Ring of integers
   1. czring
   2. df-zring
   3. zringcrng
   4. zringring
   5. zringrng
   6. zringabl
   7. zringgrp
   8. zringbas
   9. zringplusg
   10. zringsub
   11. zringmulg
   12. zringmulr
   13. zring0
   14. zring1
   15. zringnzr
   16. dvdsrzring
   17. zringlpirlem1
   18. zringlpirlem2
   19. zringlpirlem3
   20. zringinvg
   21. zringunit
   22. zringlpir
   23. zringndrg
   24. zringcyg
   25. zringsubgval
   26. zringmpg
   27. prmirredlem
   28. dfprm2
   29. prmirred
   30. expghm
   31. mulgghm2
   32. mulgrhm
   33. mulgrhm2
   34. irinitoringc
   35. nzerooringczr
   36. Example for a condition for a non-unital ring to be unital
3. Algebraic constructions based on the complex numbers
   1. czrh
   2. czlm
   3. cchr
   4. czn
   5. df-zrh
   6. df-zlm
   7. df-chr
   8. df-zn
   9. zrhval
   10. zrhval2
   11. zrhmulg
   12. zrhrhmb
   13. zrhrhm
   14. zrh1
   15. zrh0
   16. zrhpropd
   17. zlmval
   18. zlmlem
   19. zlmbas
   20. zlmplusg
   21. zlmmulr
   22. zlmsca
   23. zlmvsca
   24. zlmlmod
   25. chrval
   26. chrcl
   27. chrid
   28. chrdvds
   29. chrcong
   30. dvdschrmulg
   31. fermltlchr
   32. chrnzr
   33. chrrhm
   34. domnchr
   35. znlidl
   36. zncrng2
   37. znval
   38. znle
   39. znval2
   40. znbaslem
   41. znbas2
   42. znadd
   43. znmul
   44. znzrh
   45. znbas
   46. zncrng
   47. znzrh2
   48. znzrhval
   49. znzrhfo
   50. zncyg
   51. zndvds
   52. zndvds0
   53. znf1o
   54. zzngim
   55. znle2
   56. znleval
   57. znleval2
   58. zntoslem
   59. zntos
   60. znhash
   61. znfi
   62. znfld
   63. znidomb
   64. znchr
   65. znunit
   66. znunithash
   67. znrrg
   68. cygznlem1
   69. cygznlem2a
   70. cygznlem2
   71. cygznlem3
   72. cygzn
   73. cygth
   74. cyggic
   75. frgpcyg
   76. freshmansdream
   77. frobrhm
   78. ofldchr
4. Signs as subgroup of the complex numbers
   1. cnmsgnsubg
   2. cnmsgnbas
   3. cnmsgngrp
   4. psgnghm
   5. psgnghm2
   6. psgninv
   7. psgnco
5. Embedding of permutation signs into a ring
   1. zrhpsgnmhm
   2. zrhpsgninv
   3. evpmss
   4. psgnevpmb
   5. psgnodpm
   6. psgnevpm
   7. psgnodpmr
   8. zrhpsgnevpm
   9. zrhpsgnodpm
   10. cofipsgn
   11. zrhpsgnelbas
   12. zrhcopsgnelbas
   13. evpmodpmf1o
   14. pmtrodpm
   15. psgnfix1
   16. psgnfix2
   17. psgndiflemB
   18. psgndiflemA
   19. psgndif
   20. copsgndif
6. The ordered field of real numbers
   1. crefld
   2. df-refld
   3. rebase
   4. remulg
   5. resubdrg
   6. resubgval
   7. replusg
   8. remulr
   9. re0g
   10. re1r
   11. rele2
   12. relt
   13. reds
   14. redvr
   15. retos
   16. refld
   17. refldcj
   18. resrng
   19. regsumsupp
   20. rzgrp