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. mpoaddf
   15. mpomulf
   16. elimne0
   17. adddir
   18. 0cn
   19. 0cnd
   20. c0ex
   21. 1cnd
   22. 1ex
   23. cnre
   24. mulrid
   25. mullid
   26. 1re
   27. 1red
   28. 0re
   29. 0red
   30. pr01ssre
   31. mulridi
   32. mullidi
   33. addcli
   34. mulcli
   35. mulcomi
   36. mulcomli
   37. addassi
   38. mulassi
   39. adddii
   40. adddiri
   41. recni
   42. readdcli
   43. remulcli
   44. mulridd
   45. mullidd
   46. addcld
   47. mulcld
   48. mulcomd
   49. addassd
   50. mulassd
   51. adddid
   52. adddird
   53. adddirp1d
   54. joinlmuladdmuld
   55. recnd
   56. readdcld
   57. 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. xrltnled
   39. xrnltled
   40. ssxr
   41. 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. comraddi
   52. ltaddneg
   53. ltaddnegr