Metamath Proof Explorer

Table of Contents - 5.3. Real and complex numbers - basic operations

1. Addition
   1. add12
   2. add32
   3. add32r
   4. add4
   5. add42
   6. add12i
   7. add32i
   8. add4i
   9. add42i
   10. add12d
   11. add32d
   12. add4d
   13. add42d
2. Subtraction
   1. cmin
   2. cneg
   3. df-sub
   4. df-neg
   5. 0cnALT
   6. 0cnALT2
   7. negeu
   8. subval
   9. negeq
   10. negeqi
   11. negeqd
   12. nfnegd
   13. nfneg
   14. csbnegg
   15. negex
   16. subcl
   17. negcl
   18. negicn
   19. subf
   20. subadd
   21. subadd2
   22. subsub23
   23. pncan
   24. pncan2
   25. pncan3
   26. npcan
   27. addsubass
   28. addsub
   29. subadd23
   30. addsub12
   31. 2addsub
   32. addsubeq4
   33. pncan3oi
   34. mvrraddi
   35. mvrladdi
   36. mvlladdi
   37. subid
   38. subid1
   39. npncan
   40. nppcan
   41. nnpcan
   42. nppcan3
   43. subcan2
   44. subeq0
   45. npncan2
   46. subsub2
   47. nncan
   48. subsub
   49. nppcan2
   50. subsub3
   51. subsub4
   52. sub32
   53. nnncan
   54. nnncan1
   55. nnncan2
   56. npncan3
   57. pnpcan
   58. pnpcan2
   59. pnncan
   60. ppncan
   61. addsub4
   62. subadd4
   63. sub4
   64. neg0
   65. negid
   66. negsub
   67. subneg
   68. negneg
   69. neg11
   70. negcon1
   71. negcon2
   72. negeq0
   73. subcan
   74. negsubdi
   75. negdi
   76. negdi2
   77. negsubdi2
   78. neg2sub
   79. renegcli
   80. resubcli
   81. renegcl
   82. resubcl
   83. negreb
   84. peano2cnm
   85. peano2rem
   86. negcli
   87. negidi
   88. negnegi
   89. subidi
   90. subid1i
   91. negne0bi
   92. negrebi
   93. negne0i
   94. subcli
   95. pncan3i
   96. negsubi
   97. subnegi
   98. subeq0i
   99. neg11i
   100. negcon1i
   101. negcon2i
   102. negdii
   103. negsubdii
   104. negsubdi2i
   105. subaddi
   106. subadd2i
   107. subaddrii
   108. subsub23i
   109. addsubassi
   110. addsubi
   111. subcani
   112. subcan2i
   113. pnncani
   114. addsub4i
   115. 0reALT
   116. negcld
   117. subidd
   118. subid1d
   119. negidd
   120. negnegd
   121. negeq0d
   122. negne0bd
   123. negcon1d
   124. negcon1ad
   125. neg11ad
   126. negned
   127. negne0d
   128. negrebd
   129. subcld
   130. pncand
   131. pncan2d
   132. pncan3d
   133. npcand
   134. nncand
   135. negsubd
   136. subnegd
   137. subeq0ad
   138. subeq0d
   139. subne0d
   140. subne0ad
   141. neg11d
   142. negdid
   143. negdi2d
   144. negsubdid
   145. negsubdi2d
   146. neg2subd
   147. subaddd
   148. subadd2d
   149. addsubassd
   150. addsubd
   151. subadd23d
   152. addsub12d
   153. npncand
   154. nppcand
   155. nppcan2d
   156. nppcan3d
   157. subsubd
   158. subsub2d
   159. subsub3d
   160. subsub4d
   161. sub32d
   162. nnncand
   163. nnncan1d
   164. nnncan2d
   165. npncan3d
   166. pnpcand
   167. pnpcan2d
   168. pnncand
   169. ppncand
   170. subcand
   171. subcan2d
   172. subcanad
   173. subneintrd
   174. subcan2ad
   175. subneintr2d
   176. addsub4d
   177. subadd4d
   178. sub4d
   179. 2addsubd
   180. addsubeq4d
   181. subsubadd23
   182. addsubsub23
   183. subeqxfrd
   184. mvlraddd
   185. mvlladdd
   186. mvrraddd
   187. mvrladdd
   188. assraddsubd
   189. subaddeqd
   190. addlsub
   191. addrsub
   192. subexsub
   193. addid0
   194. addn0nid
   195. pnpncand
   196. subeqrev
   197. addeq0
   198. pncan1
   199. npcan1
   200. subeq0bd
   201. renegcld
   202. resubcld
   203. negn0
   204. negf1o
3. Multiplication
   1. kcnktkm1cn
   2. muladd
   3. subdi
   4. subdir
   5. ine0
   6. mulneg1
   7. mulneg2
   8. mulneg12
   9. mul2neg
   10. submul2
   11. mulm1
   12. addneg1mul
   13. mulsub
   14. mulsub2
   15. mulm1i
   16. mulneg1i
   17. mulneg2i
   18. mul2negi
   19. subdii
   20. subdiri
   21. muladdi
   22. mulm1d
   23. mulneg1d
   24. mulneg2d
   25. mul2negd
   26. subdid
   27. subdird
   28. muladdd
   29. mulsubd
   30. muls1d
   31. mulsubfacd
   32. addmulsub
   33. subaddmulsub
   34. mulsubaddmulsub
4. Ordering on reals (cont.)
   1. gt0ne0
   2. lt0ne0
   3. ltadd1
   4. leadd1
   5. leadd2
   6. ltsubadd
   7. ltsubadd2
   8. lesubadd
   9. lesubadd2
   10. ltaddsub
   11. ltaddsub2
   12. leaddsub
   13. leaddsub2
   14. suble
   15. lesub
   16. ltsub23
   17. ltsub13
   18. le2add
   19. ltleadd
   20. leltadd
   21. lt2add
   22. addgt0
   23. addgegt0
   24. addgtge0
   25. addge0
   26. ltaddpos
   27. ltaddpos2
   28. ltsubpos
   29. posdif
   30. lesub1
   31. lesub2
   32. ltsub1
   33. ltsub2
   34. lt2sub
   35. le2sub
   36. ltneg
   37. ltnegcon1
   38. ltnegcon2
   39. leneg
   40. lenegcon1
   41. lenegcon2
   42. lt0neg1
   43. lt0neg2
   44. le0neg1
   45. le0neg2
   46. addge01
   47. addge02
   48. add20
   49. subge0
   50. suble0
   51. leaddle0
   52. subge02
   53. lesub0
   54. mulge0
   55. mullt0
   56. msqgt0
   57. msqge0
   58. 0lt1
   59. 0le1
   60. relin01
   61. ltordlem
   62. ltord1
   63. leord1
   64. eqord1
   65. ltord2
   66. leord2
   67. eqord2
   68. wloglei
   69. wlogle
   70. leidi
   71. gt0ne0i
   72. gt0ne0ii
   73. msqgt0i
   74. msqge0i
   75. addgt0i
   76. addge0i
   77. addgegt0i
   78. addgt0ii
   79. add20i
   80. ltnegi
   81. lenegi
   82. ltnegcon2i
   83. mulge0i
   84. lesub0i
   85. ltaddposi
   86. posdifi
   87. ltnegcon1i
   88. lenegcon1i
   89. subge0i
   90. ltadd1i
   91. leadd1i
   92. leadd2i
   93. ltsubaddi
   94. lesubaddi
   95. ltsubadd2i
   96. lesubadd2i
   97. ltaddsubi
   98. lt2addi
   99. le2addi
   100. gt0ne0d
   101. lt0ne0d
   102. leidd
   103. msqgt0d
   104. msqge0d
   105. lt0neg1d
   106. lt0neg2d
   107. le0neg1d
   108. le0neg2d
   109. addgegt0d
   110. addgtge0d
   111. addgt0d
   112. addge0d
   113. mulge0d
   114. ltnegd
   115. lenegd
   116. ltnegcon1d
   117. ltnegcon2d
   118. lenegcon1d
   119. lenegcon2d
   120. ltaddposd
   121. ltaddpos2d
   122. ltsubposd
   123. posdifd
   124. addge01d
   125. addge02d
   126. subge0d
   127. suble0d
   128. subge02d
   129. ltadd1d
   130. leadd1d
   131. leadd2d
   132. ltsubaddd
   133. lesubaddd
   134. ltsubadd2d
   135. lesubadd2d
   136. ltaddsubd
   137. ltaddsub2d
   138. leaddsub2d
   139. subled
   140. lesubd
   141. ltsub23d
   142. ltsub13d
   143. lesub1d
   144. lesub2d
   145. ltsub1d
   146. ltsub2d
   147. ltadd1dd
   148. ltsub1dd
   149. ltsub2dd
   150. leadd1dd
   151. leadd2dd
   152. lesub1dd
   153. lesub2dd
   154. lesub3d
   155. le2addd
   156. le2subd
   157. ltleaddd
   158. leltaddd
   159. lt2addd
   160. lt2subd
   161. possumd
   162. sublt0d
   163. ltaddsublt
   164. 1le1
5. Reciprocals
   1. ixi
   2. recextlem1
   3. recextlem2
   4. recex
   5. mulcand
   6. mulcan2d
   7. mulcanad
   8. mulcan2ad
   9. mulcan
   10. mulcan2
   11. mulcani
   12. mul0or
   13. mulne0b
   14. mulne0
   15. mulne0i
   16. muleqadd
   17. receu
   18. mulnzcnf
   19. mul0ori
   20. mul0ord
   21. msq0i
   22. msq0d
   23. mulne0bd
   24. mulne0d
   25. mulcan1g
   26. mulcan2g
   27. mulne0bad
   28. mulne0bbd
6. Division
   1. cdiv
   2. df-div
   3. 1div0
   4. divval
   5. divmul
   6. divmul2
   7. divmul3
   8. divcl
   9. reccl
   10. divcan2
   11. divcan1
   12. diveq0
   13. divne0b
   14. divne0
   15. recne0
   16. recid
   17. recid2
   18. divrec
   19. divrec2
   20. divass
   21. div23
   22. div32
   23. div13
   24. div12
   25. divmulass
   26. divmulasscom
   27. divdir
   28. divcan3
   29. divcan4
   30. div11
   31. diveq1
   32. divid
   33. div0
   34. div1
   35. 1div1e1
   36. divneg
   37. muldivdir
   38. divsubdir
   39. muldivdid
   40. subdivcomb1
   41. subdivcomb2
   42. recrec
   43. rec11
   44. rec11r
   45. divmuldiv
   46. divdivdiv
   47. divcan5
   48. divmul13
   49. divmul24
   50. divmuleq
   51. recdiv
   52. divcan6
   53. divdiv32
   54. divcan7
   55. dmdcan
   56. divdiv1
   57. divdiv2
   58. recdiv2
   59. ddcan
   60. divadddiv
   61. divsubdiv
   62. conjmul
   63. rereccl
   64. redivcl
   65. eqneg
   66. eqnegd
   67. eqnegad
   68. div2neg
   69. divneg2
   70. recclzi
   71. recne0zi
   72. recidzi
   73. div1i
   74. eqnegi
   75. reccli
   76. recidi
   77. recreci
   78. dividi
   79. div0i
   80. divclzi
   81. divcan1zi
   82. divcan2zi
   83. divreczi
   84. divcan3zi
   85. divcan4zi
   86. rec11i
   87. divcli
   88. divcan2i
   89. divcan1i
   90. divreci
   91. divcan3i
   92. divcan4i
   93. divne0i
   94. rec11ii
   95. divasszi
   96. divmulzi
   97. divdirzi
   98. divdiv23zi
   99. divmuli
   100. divdiv32i
   101. divassi
   102. divdiri
   103. div23i
   104. div11i
   105. divmuldivi
   106. divmul13i
   107. divadddivi
   108. divdivdivi
   109. rerecclzi
   110. rereccli
   111. redivclzi
   112. redivcli
   113. div1d
   114. reccld
   115. recne0d
   116. recidd
   117. recid2d
   118. recrecd
   119. dividd
   120. div0d
   121. divcld
   122. divcan1d
   123. divcan2d
   124. divrecd
   125. divrec2d
   126. divcan3d
   127. divcan4d
   128. diveq0d
   129. diveq1d
   130. diveq1ad
   131. diveq0ad
   132. divne1d
   133. divne0bd
   134. divnegd
   135. divneg2d
   136. div2negd
   137. divne0d
   138. recdivd
   139. recdiv2d
   140. divcan6d
   141. ddcand
   142. rec11d
   143. divmuld
   144. div32d
   145. div13d
   146. divdiv32d
   147. divcan5d
   148. divcan5rd
   149. divcan7d
   150. dmdcand
   151. dmdcan2d
   152. divdiv1d
   153. divdiv2d
   154. divmul2d
   155. divmul3d
   156. divassd
   157. div12d
   158. div23d
   159. divdird
   160. divsubdird
   161. div11d
   162. divmuldivd
   163. divmul13d
   164. divmul24d
   165. divadddivd
   166. divsubdivd
   167. divmuleqd
   168. divdivdivd
   169. diveq1bd
   170. div2sub
   171. div2subd
   172. rereccld
   173. redivcld
   174. subrecd
   175. subrec
   176. subreci
   177. mvllmuld
   178. mvllmuli
   179. ldiv
   180. rdiv
   181. mdiv
   182. lineq
7. Ordering on reals (cont.)
   1. elimgt0
   2. elimge0
   3. ltp1
   4. lep1
   5. ltm1
   6. lem1
   7. letrp1
   8. p1le
   9. recgt0
   10. prodgt0
   11. prodgt02
   12. ltmul1a
   13. ltmul1
   14. ltmul2
   15. lemul1
   16. lemul2
   17. lemul1a
   18. lemul2a
   19. ltmul12a
   20. lemul12b
   21. lemul12a
   22. ltmulgt11
   23. ltmulgt12
   24. mulgt1
   25. lemulge11
   26. lemulge12
   27. ltdiv1
   28. lediv1
   29. gt0div
   30. ge0div
   31. divgt0
   32. divge0
   33. mulge0b
   34. mulle0b
   35. mulsuble0b
   36. ltmuldiv
   37. ltmuldiv2
   38. ltdivmul
   39. ledivmul
   40. ltdivmul2
   41. lt2mul2div
   42. ledivmul2
   43. lemuldiv
   44. lemuldiv2
   45. ltrec
   46. lerec
   47. lt2msq1
   48. lt2msq
   49. ltdiv2
   50. ltrec1
   51. lerec2
   52. ledivdiv
   53. lediv2
   54. ltdiv23
   55. lediv23
   56. lediv12a
   57. lediv2a
   58. reclt1
   59. recgt1
   60. recgt1i
   61. recp1lt1
   62. recreclt
   63. le2msq
   64. msq11
   65. ledivp1
   66. squeeze0
   67. ltp1i
   68. recgt0i
   69. recgt0ii
   70. prodgt0i
   71. divgt0i
   72. divge0i
   73. ltreci
   74. lereci
   75. lt2msqi
   76. le2msqi
   77. msq11i
   78. divgt0i2i
   79. ltrecii
   80. divgt0ii
   81. ltmul1i
   82. ltdiv1i
   83. ltmuldivi
   84. ltmul2i
   85. lemul1i
   86. lemul2i
   87. ltdiv23i
   88. ledivp1i
   89. ltdivp1i
   90. ltdiv23ii
   91. ltmul1ii
   92. ltdiv1ii
   93. ltp1d
   94. lep1d
   95. ltm1d
   96. lem1d
   97. recgt0d
   98. divgt0d
   99. mulgt1d
   100. lemulge11d
   101. lemulge12d
   102. lemul1ad
   103. lemul2ad
   104. ltmul12ad
   105. lemul12ad
   106. lemul12bd
8. Completeness Axiom and Suprema
   1. fimaxre
   2. fimaxre2
   3. fimaxre3
   4. fiminre
   5. fiminre2
   6. negfi
   7. lbreu
   8. lbcl
   9. lble
   10. lbinf
   11. lbinfcl
   12. lbinfle
   13. sup2
   14. sup3
   15. infm3lem
   16. infm3
   17. suprcl
   18. suprub
   19. suprubd
   20. suprcld
   21. suprlub
   22. suprnub
   23. suprleub
   24. supaddc
   25. supadd
   26. supmul1
   27. supmullem1
   28. supmullem2
   29. supmul
   30. sup3ii
   31. suprclii
   32. suprubii
   33. suprlubii
   34. suprnubii
   35. suprleubii
   36. riotaneg
   37. negiso
   38. dfinfre
   39. infrecl
   40. infrenegsup
   41. infregelb
   42. infrelb
   43. infrefilb
   44. supfirege
9. Imaginary and complex number properties
   1. neg1cn
   2. neg1rr
   3. neg1ne0
   4. neg1lt0
   5. negneg1e1
   6. inelr
   7. rimul
   8. cru
   9. crne0
   10. creur
   11. creui
   12. cju
10. Function operation analogue theorems
    1. ofsubeq0
    2. ofnegsub
    3. ofsubge0
11. Indicator Functions
    1. cind
    2. df-ind
    3. indv
    4. indval
    5. indval0
    6. indval2
    7. indf
    8. indfval
    9. fvindre
    10. ind1
    11. ind0
    12. ind1a
    13. indconst0
    14. indconst1
    15. indpi1