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. 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. zringsubgval
   24. zringmpg
   25. prmirredlem
   26. dfprm2
   27. prmirred
   28. expghm
   29. mulgghm2
   30. mulgrhm
   31. 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. chrval
   26. chrcl
   27. chrid
   28. chrdvds
   29. chrcong
   30. chrnzr
   31. chrrhm
   32. domnchr
   33. znlidl
   34. zncrng2
   35. znval
   36. znle
   37. znval2
   38. znbaslem
   39. znbas2
   40. znadd
   41. znmul
   42. znzrh
   43. znbas
   44. zncrng
   45. znzrh2
   46. znzrhval
   47. znzrhfo
   48. zncyg
   49. zndvds
   50. zndvds0
   51. znf1o
   52. zzngim
   53. znle2
   54. znleval
   55. znleval2
   56. zntoslem
   57. zntos
   58. znhash
   59. znfi
   60. znfld
   61. znidomb
   62. znchr
   63. znunit
   64. znunithash
   65. znrrg
   66. cygznlem1
   67. cygznlem2a
   68. cygznlem2
   69. cygznlem3
   70. cygzn
   71. cygth
   72. cyggic
   73. 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