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. xrsstr
   34. xrsex
   35. xrsadd
   36. xrsmul
   37. xrstset
   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. xrsds
   56. xrsdsval
   57. xrsdsreval
   58. xrsdsreclblem
   59. xrsdsreclb
   60. cnsubmlem
   61. cnsubglem
   62. cnsubrglem
   63. cnsubdrglem
   64. qsubdrg
   65. zsubrg
   66. gzsubrg
   67. nn0subm
   68. rege0subm
   69. absabv
   70. zsssubrg
   71. qsssubdrg
   72. cnsubrg
   73. cnmgpabl
   74. cnmgpid
   75. cnmsubglem
   76. rpmsubg
   77. gzrngunitlem
   78. gzrngunit
   79. gsumfsum
   80. regsumfsum
   81. expmhm
   82. nn0srg
   83. rge0srg
   84. xrge0plusg
   85. xrs1mnd
   86. xrs10
   87. xrs1cmn
   88. xrge0subm
   89. xrge0cmn
   90. 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