Metamath Proof Explorer

Table of Contents - 5.2. Derive the basic properties from the field axioms

1. Some deductions from the field axioms for complex numbers
   1. cnex
   2. addcl
   3. readdcl
   4. mulcl
   5. remulcl
   6. mulcom
   7. addass
   8. mulass
   9. adddi
   10. recn
   11. reex
   12. reelprrecn
   13. cnelprrecn
   14. mpomulf
   15. elimne0
   16. adddir
   17. 0cn
   18. 0cnd
   19. c0ex
   20. 1cnd
   21. 1ex
   22. cnre
   23. mulrid
   24. mullid
   25. 1re
   26. 1red
   27. 0re
   28. 0red
   29. mulridi
   30. mullidi
   31. addcli
   32. mulcli
   33. mulcomi
   34. mulcomli
   35. addassi
   36. mulassi
   37. adddii
   38. adddiri
   39. recni
   40. readdcli
   41. remulcli
   42. mulridd
   43. mullidd
   44. addcld
   45. mulcld
   46. mulcomd
   47. addassd
   48. mulassd
   49. adddid
   50. adddird
   51. adddirp1d
   52. joinlmuladdmuld
   53. recnd
   54. readdcld
   55. remulcld
2. Infinity and the extended real number system
   1. cpnf
   2. cmnf
   3. cxr
   4. clt
   5. cle
   6. df-pnf
   7. df-mnf
   8. df-xr
   9. df-ltxr
   10. df-le
   11. pnfnre
   12. pnfnre2
   13. mnfnre
   14. ressxr
   15. rexpssxrxp
   16. rexr
   17. 0xr
   18. renepnf
   19. renemnf
   20. rexrd
   21. renepnfd
   22. renemnfd
   23. pnfex
   24. pnfxr
   25. pnfnemnf
   26. mnfnepnf
   27. mnfxr
   28. rexri
   29. 1xr
   30. renfdisj
   31. ltrelxr
   32. ltrel
   33. lerelxr
   34. lerel
   35. xrlenlt
   36. xrlenltd
   37. xrltnle
   38. xrnltled
   39. ssxr
   40. ltxrlt
3. Restate the ordering postulates with extended real "less than"
   1. axlttri
   2. axlttrn
   3. axltadd
   4. axmulgt0
   5. axsup
4. Ordering on reals
   1. lttr
   2. mulgt0
   3. lenlt
   4. ltnle
   5. ltso
   6. gtso
   7. lttri2
   8. lttri3
   9. lttri4
   10. letri3
   11. leloe
   12. eqlelt
   13. ltle
   14. leltne
   15. lelttr
   16. leltletr
   17. ltletr
   18. ltleletr
   19. letr
   20. ltnr
   21. leid
   22. ltne
   23. ltnsym
   24. ltnsym2
   25. letric
   26. ltlen
   27. eqle
   28. eqled
   29. ltadd2
   30. ne0gt0
   31. lecasei
   32. lelttric
   33. ltlecasei
   34. ltnri
   35. eqlei
   36. eqlei2
   37. gtneii
   38. ltneii
   39. lttri2i
   40. lttri3i
   41. letri3i
   42. leloei
   43. ltleni
   44. ltnsymi
   45. lenlti
   46. ltnlei
   47. ltlei
   48. ltleii
   49. ltnei
   50. letrii
   51. lttri
   52. lelttri
   53. ltletri
   54. letri
   55. le2tri3i
   56. ltadd2i
   57. mulgt0i
   58. mulgt0ii
   59. ltnrd
   60. gtned
   61. ltned
   62. ne0gt0d
   63. lttrid
   64. lttri2d
   65. lttri3d
   66. lttri4d
   67. letri3d
   68. leloed
   69. eqleltd
   70. ltlend
   71. lenltd
   72. ltnled
   73. ltled
   74. ltnsymd
   75. nltled
   76. lensymd
   77. letrid
   78. leltned
   79. leneltd
   80. mulgt0d
   81. ltadd2d
   82. letrd
   83. lelttrd
   84. ltadd2dd
   85. ltletrd
   86. lttrd
   87. lelttrdi
   88. dedekind
   89. dedekindle
5. Initial properties of the complex numbers
   1. mul12
   2. mul32
   3. mul31
   4. mul4
   5. mul4r
   6. muladd11
   7. 1p1times
   8. peano2cn
   9. peano2re
   10. readdcan
   11. 00id
   12. mul02lem1
   13. mul02lem2
   14. mul02
   15. mul01
   16. addrid
   17. cnegex
   18. cnegex2
   19. addlid
   20. addcan
   21. addcan2
   22. addcom
   23. addridi
   24. addlidi
   25. mul02i
   26. mul01i
   27. addcomi
   28. addcomli
   29. addcani
   30. addcan2i
   31. mul12i
   32. mul32i
   33. mul4i
   34. mul02d
   35. mul01d
   36. addridd
   37. addlidd
   38. addcomd
   39. addcand
   40. addcan2d
   41. addcanad
   42. addcan2ad
   43. addneintrd
   44. addneintr2d
   45. mul12d
   46. mul32d
   47. mul31d
   48. mul4d
   49. muladd11r
   50. comraddd
   51. ltaddneg
   52. ltaddnegr