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. cnfldfunOLD
    31. cnfldfunALT
    32. xrsstr
    33. xrsex
    34. xrsbas
    35. xrsadd
    36. xrsmul
    37. xrstset
    38. xrsle
    39. cncrng
    40. cnring
    41. xrsmcmn
    42. cnfld0
    43. cnfld1
    44. cnfldneg
    45. cnfldplusf
    46. cnfldsub
    47. cndrng
    48. cnflddiv
    49. cnfldinv
    50. cnfldmulg
    51. cnfldexp
    52. cnsrng
    53. xrsmgm
    54. xrsnsgrp
    55. xrsmgmdifsgrp
    56. xrs1mnd
    57. xrs10
    58. xrs1cmn
    59. xrge0subm
    60. xrge0cmn
    61. xrsds
    62. xrsdsval
    63. xrsdsreval
    64. xrsdsreclblem
    65. xrsdsreclb
    66. cnsubmlem
    67. cnsubglem
    68. cnsubrglem
    69. cnsubdrglem
    70. qsubdrg
    71. zsubrg
    72. gzsubrg
    73. nn0subm
    74. rege0subm
    75. absabv
    76. zsssubrg
    77. qsssubdrg
    78. cnsubrg
    79. cnmgpabl
    80. cnmgpid
    81. cnmsubglem
    82. rpmsubg
    83. gzrngunitlem
    84. gzrngunit
    85. gsumfsum
    86. regsumfsum
    87. expmhm
    88. nn0srg
    89. rge0srg
  2. Ring of integers
    1. czring
    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. zlmlemOLD
    20. zlmbas
    21. zlmbasOLD
    22. zlmplusg
    23. zlmplusgOLD
    24. zlmmulr
    25. zlmmulrOLD
    26. zlmsca
    27. zlmvsca
    28. zlmlmod
    29. chrval
    30. chrcl
    31. chrid
    32. chrdvds
    33. chrcong
    34. chrnzr
    35. chrrhm
    36. domnchr
    37. znlidl
    38. zncrng2
    39. znval
    40. znle
    41. znval2
    42. znbaslem
    43. znbaslemOLD
    44. znbas2
    45. znbas2OLD
    46. znadd
    47. znaddOLD
    48. znmul
    49. znmulOLD
    50. znzrh
    51. znbas
    52. zncrng
    53. znzrh2
    54. znzrhval
    55. znzrhfo
    56. zncyg
    57. zndvds
    58. zndvds0
    59. znf1o
    60. zzngim
    61. znle2
    62. znleval
    63. znleval2
    64. zntoslem
    65. zntos
    66. znhash
    67. znfi
    68. znfld
    69. znidomb
    70. znchr
    71. znunit
    72. znunithash
    73. znrrg
    74. cygznlem1
    75. cygznlem2a
    76. cygznlem2
    77. cygznlem3
    78. cygzn
    79. cygth
    80. cyggic
    81. 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