Metamath Proof Explorer

Table of Contents - 10.10. 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. cnfldadd
   23. cnfldmul
   24. cnfldcj
   25. cnfldtset
   26. cnfldle
   27. cnfldds
   28. cnfldunif
   29. cnfldfun
   30. cnfldfunALT
   31. xrsstr
   32. xrsex
   33. xrsbas
   34. xrsadd
   35. xrsmul
   36. xrstset
   37. xrsle
   38. cncrng
   39. cnring
   40. xrsmcmn
   41. cnfld0
   42. cnfld1
   43. cnfldneg
   44. cnfldplusf
   45. cnfldsub
   46. cndrng
   47. cnflddiv
   48. cnfldinv
   49. cnfldmulg
   50. cnfldexp
   51. cnsrng
   52. xrsmgm
   53. xrsnsgrp
   54. xrsmgmdifsgrp
   55. xrs1mnd
   56. xrs10
   57. xrs1cmn
   58. xrge0subm
   59. xrge0cmn
   60. xrsds
   61. xrsdsval
   62. xrsdsreval
   63. xrsdsreclblem
   64. xrsdsreclb
   65. cnsubmlem
   66. cnsubglem
   67. cnsubrglem
   68. cnsubdrglem
   69. qsubdrg
   70. zsubrg
   71. gzsubrg
   72. nn0subm
   73. rege0subm
   74. absabv
   75. zsssubrg
   76. qsssubdrg
   77. cnsubrg
   78. cnmgpabl
   79. cnmgpid
   80. cnmsubglem
   81. rpmsubg
   82. gzrngunitlem
   83. gzrngunit
   84. gsumfsum
   85. regsumfsum
   86. expmhm
   87. nn0srg
   88. rge0srg
2. Ring of integers
   1. zring
   2. df-zring
   3. zringcrng
   4. zringring
   5. zringabl
   6. zringgrp
   7. zringbas
   8. zringplusg
   9. zringmulg
   10. zringmulr
   11. zring0
   12. zring1
   13. zringnzr
   14. dvdsrzring
   15. zringlpirlem1
   16. zringlpirlem2
   17. zringlpirlem3
   18. zringinvg
   19. zringunit
   20. zringlpir
   21. zringndrg
   22. zringcyg
   23. zringmpg
   24. prmirredlem
   25. dfprm2
   26. prmirred
   27. expghm
   28. mulgghm2
   29. mulgrhm
   30. mulgrhm2
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. zlmassa
   26. chrval
   27. chrcl
   28. chrid
   29. chrdvds
   30. chrcong
   31. chrnzr
   32. chrrhm
   33. domnchr
   34. znlidl
   35. zncrng2
   36. znval
   37. znle
   38. znval2
   39. znbaslem
   40. znbas2
   41. znadd
   42. znmul
   43. znzrh
   44. znbas
   45. zncrng
   46. znzrh2
   47. znzrhval
   48. znzrhfo
   49. zncyg
   50. zndvds
   51. zndvds0
   52. znf1o
   53. zzngim
   54. znle2
   55. znleval
   56. znleval2
   57. zntoslem
   58. zntos
   59. znhash
   60. znfi
   61. znfld
   62. znidomb
   63. znchr
   64. znunit
   65. znunithash
   66. znrrg
   67. cygznlem1
   68. cygznlem2a
   69. cygznlem2
   70. cygznlem3
   71. cygzn
   72. cygth
   73. cyggic
   74. frgpcyg
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. recrng
   19. regsumsupp
   20. rzgrp