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. elimne0
   15. adddir
   16. 0cn
   17. 0cnd
   18. c0ex
   19. 1cnd
   20. 1ex
   21. cnre
   22. mulid1
   23. mulid2
   24. 1re
   25. 1red
   26. 0re
   27. 0red
   28. mulid1i
   29. mulid2i
   30. addcli
   31. mulcli
   32. mulcomi
   33. mulcomli
   34. addassi
   35. mulassi
   36. adddii
   37. adddiri
   38. recni
   39. readdcli
   40. remulcli
   41. mulid1d
   42. mulid2d
   43. addcld
   44. mulcld
   45. mulcomd
   46. addassd
   47. mulassd
   48. adddid
   49. adddird
   50. adddirp1d
   51. joinlmuladdmuld
   52. recnd
   53. readdcld
   54. 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. ltletr
   17. ltleletr
   18. letr
   19. ltnr
   20. leid
   21. ltne
   22. ltnsym
   23. ltnsym2
   24. letric
   25. ltlen
   26. eqle
   27. eqled
   28. ltadd2
   29. ne0gt0
   30. lecasei
   31. lelttric
   32. ltlecasei
   33. ltnri
   34. eqlei
   35. eqlei2
   36. gtneii
   37. ltneii
   38. lttri2i
   39. lttri3i
   40. letri3i
   41. leloei
   42. ltleni
   43. ltnsymi
   44. lenlti
   45. ltnlei
   46. ltlei
   47. ltleii
   48. ltnei
   49. letrii
   50. lttri
   51. lelttri
   52. ltletri
   53. letri
   54. le2tri3i
   55. ltadd2i
   56. mulgt0i
   57. mulgt0ii
   58. ltnrd
   59. gtned
   60. ltned
   61. ne0gt0d
   62. lttrid
   63. lttri2d
   64. lttri3d
   65. lttri4d
   66. letri3d
   67. leloed
   68. eqleltd
   69. ltlend
   70. lenltd
   71. ltnled
   72. ltled
   73. ltnsymd
   74. nltled
   75. lensymd
   76. letrid
   77. leltned
   78. leneltd
   79. mulgt0d
   80. ltadd2d
   81. letrd
   82. lelttrd
   83. ltadd2dd
   84. ltletrd
   85. lttrd
   86. lelttrdi
   87. dedekind
   88. 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. addid1
   17. cnegex
   18. cnegex2
   19. addid2
   20. addcan
   21. addcan2
   22. addcom
   23. addid1i
   24. addid2i
   25. mul02i
   26. mul01i
   27. addcomi
   28. addcomli
   29. addcani
   30. addcan2i
   31. mul12i
   32. mul32i
   33. mul4i
   34. mul02d
   35. mul01d
   36. addid1d
   37. addid2d
   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