Metamath Proof Explorer

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

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
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. mvlladdi
36. subid
37. subid1
38. npncan
39. nppcan
40. nnpcan
41. nppcan3
42. subcan2
43. subeq0
44. npncan2
45. subsub2
46. nncan
47. subsub
48. nppcan2
49. subsub3
50. subsub4
51. sub32
52. nnncan
53. nnncan1
54. nnncan2
55. npncan3
56. pnpcan
57. pnpcan2
58. pnncan
59. ppncan
60. addsub4
61. subadd4
62. sub4
63. neg0
64. negid
65. negsub
66. subneg
67. negneg
68. neg11
69. negcon1
70. negcon2
71. negeq0
72. subcan
73. negsubdi
74. negdi
75. negdi2
76. negsubdi2
77. neg2sub
78. renegcli
79. resubcli
80. renegcl
81. resubcl
82. negreb
83. peano2cnm
84. peano2rem
85. negcli
86. negidi
87. negnegi
88. subidi
89. subid1i
90. negne0bi
91. negrebi
92. negne0i
93. subcli
94. pncan3i
95. negsubi
96. subnegi
97. subeq0i
98. neg11i
99. negcon1i
100. negcon2i
101. negdii
102. negsubdii
103. negsubdi2i
104. subaddi
105. subadd2i
106. subaddrii
107. subsub23i
108. addsubassi
109. addsubi
110. subcani
111. subcan2i
112. pnncani
113. addsub4i
114. 0reALT
115. negcld
116. subidd
117. subid1d
118. negidd
119. negnegd
120. negeq0d
121. negne0bd
122. negcon1d
123. negcon1ad
124. neg11ad
125. negned
126. negne0d
127. negrebd
128. subcld
129. pncand
130. pncan2d
131. pncan3d
132. npcand
133. nncand
134. negsubd
135. subnegd
136. subeq0d
137. subne0d
138. subeq0ad
139. subne0ad
140. neg11d
141. negdid
142. negdi2d
143. negsubdid
144. negsubdi2d
145. neg2subd
146. subaddd
147. subadd2d
148. addsubassd
149. addsubd
150. subadd23d
151. addsub12d
152. npncand
153. nppcand
154. nppcan2d
155. nppcan3d
156. subsubd
157. subsub2d
158. subsub3d
159. subsub4d
160. sub32d
161. nnncand
162. nnncan1d
163. nnncan2d
164. npncan3d
165. pnpcand
166. pnpcan2d
167. pnncand
168. ppncand
169. subcand
170. subcan2d
171. subcanad
172. subneintrd
173. subcan2ad
174. subneintr2d
175. addsub4d
176. subadd4d
177. sub4d
178. 2addsubd
179. addsubeq4d
180. subeqxfrd
181. mvlraddd
182. mvlladdd
183. mvrraddd
184. mvrladdd
185. assraddsubd
186. subaddeqd
187. addlsub
188. addrsub
189. subexsub
190. addid0
191. addn0nid
192. pnpncand
193. subeqrev
194. addeq0
195. pncan1
196. npcan1
197. subeq0bd
198. renegcld
199. resubcld
200. negn0
201. negf1o
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
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
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. mulnzcnopr
19. msq0i
20. mul0ori
21. msq0d
22. mul0ord
23. mulne0bd
24. mulne0d
25. mulcan1g
26. mulcan2g
27. mulne0bad
28. mulne0bbd
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. divid
32. div0
33. div1
34. 1div1e1
35. diveq1
36. divneg
37. muldivdir
38. divsubdir
39. subdivcomb1
40. subdivcomb2
41. recrec
42. rec11
43. rec11r
44. divmuldiv
45. divdivdiv
46. divcan5
47. divmul13
48. divmul24
49. divmuleq
50. recdiv
51. divcan6
52. divdiv32
53. divcan7
54. dmdcan
55. divdiv1
56. divdiv2
57. recdiv2
58. ddcan
59. divadddiv
60. divsubdiv
61. conjmul
62. rereccl
63. redivcl
64. eqneg
65. eqnegd
66. eqnegad
67. div2neg
68. divneg2
69. recclzi
70. recne0zi
71. recidzi
72. div1i
73. eqnegi
74. reccli
75. recidi
76. recreci
77. dividi
78. div0i
79. divclzi
80. divcan1zi
81. divcan2zi
82. divreczi
83. divcan3zi
84. divcan4zi
85. rec11i
86. divcli
87. divcan2i
88. divcan1i
89. divreci
90. divcan3i
91. divcan4i
92. divne0i
93. rec11ii
94. divasszi
95. divmulzi
96. divdirzi
97. divdiv23zi
98. divmuli
99. divdiv32i
100. divassi
101. divdiri
102. div23i
103. div11i
104. divmuldivi
105. divmul13i
106. divadddivi
107. divdivdivi
108. rerecclzi
109. rereccli
110. redivclzi
111. redivcli
112. div1d
113. reccld
114. recne0d
115. recidd
116. recid2d
117. recrecd
118. dividd
119. div0d
120. divcld
121. divcan1d
122. divcan2d
123. divrecd
124. divrec2d
125. divcan3d
126. divcan4d
127. diveq0d
128. diveq1d
129. diveq1ad
130. diveq0ad
131. divne1d
132. divne0bd
133. divnegd
134. divneg2d
135. div2negd
136. divne0d
137. recdivd
138. recdiv2d
139. divcan6d
140. ddcand
141. rec11d
142. divmuld
143. div32d
144. div13d
145. divdiv32d
146. divcan5d
147. divcan5rd
148. divcan7d
149. dmdcand
150. dmdcan2d
151. divdiv1d
152. divdiv2d
153. divmul2d
154. divmul3d
155. divassd
156. div12d
157. div23d
158. divdird
159. divsubdird
160. div11d
161. divmuldivd
162. divmul13d
163. divmul24d
164. divadddivd
165. divsubdivd
166. divmuleqd
167. divdivdivd
168. diveq1bd
169. div2sub
170. div2subd
171. rereccld
172. redivcld
173. subrec
174. subreci
175. subrecd
176. mvllmuld
177. mvllmuli
178. ldiv
179. rdiv
180. mdiv
181. lineq
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. mulgt1
23. ltmulgt11
24. ltmulgt12
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
Completeness Axiom and Suprema
1. fimaxre
2. fimaxreOLD
3. fimaxre2
4. fimaxre3
5. fiminre
6. negfi
7. fiminreOLD
8. lbreu
9. lbcl
10. lble
11. lbinf
12. lbinfcl
13. lbinfle
14. sup2
15. sup3
16. infm3lem
17. infm3
18. suprcl
19. suprub
20. suprubd
21. suprcld
22. suprlub
23. suprnub
24. suprleub
25. supaddc
26. supadd
27. supmul1
28. supmullem1
29. supmullem2
30. supmul
31. sup3ii
32. suprclii
33. suprubii
34. suprlubii
35. suprnubii
36. suprleubii
37. riotaneg
38. negiso
39. dfinfre
40. infrecl
41. infrenegsup
42. infregelb
43. infrelb
44. supfirege
Imaginary and complex number properties
1. inelr
2. rimul
3. cru
4. crne0
5. creur
6. creui
7. cju
Function operation analogue theorems