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. 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. subeq0d
138. subne0d
139. subeq0ad
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. subeqxfrd
182. mvlraddd
183. mvlladdd
184. mvrraddd
185. mvrladdd
186. assraddsubd
187. subaddeqd
188. addlsub
189. addrsub
190. subexsub
191. addid0
192. addn0nid
193. pnpncand
194. subeqrev
195. addeq0
196. pncan1
197. npcan1
198. subeq0bd
199. renegcld
200. resubcld
201. negn0
202. 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. mulnzcnf
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. 1div0OLD
5. divval
6. divmul
7. divmul2
8. divmul3
9. divcl
10. reccl
11. divcan2
12. divcan1
13. diveq0
14. divne0b
15. divne0
16. recne0
17. recid
18. recid2
19. divrec
20. divrec2
21. divass
22. div23
23. div32
24. div13
25. div12
26. divmulass
27. divmulasscom
28. divdir
29. divcan3
30. divcan4
31. div11
32. div11OLD
33. diveq1
34. divid
35. dividOLD
36. div0
37. div0OLD
38. div1
39. 1div1e1
40. divneg
41. muldivdir
42. divsubdir
43. subdivcomb1
44. subdivcomb2
45. recrec
46. rec11
47. rec11r
48. divmuldiv
49. divdivdiv
50. divcan5
51. divmul13
52. divmul24
53. divmuleq
54. recdiv
55. divcan6
56. divdiv32
57. divcan7
58. dmdcan
59. divdiv1
60. divdiv2
61. recdiv2
62. ddcan
63. divadddiv
64. divsubdiv
65. conjmul
66. rereccl
67. redivcl
68. eqneg
69. eqnegd
70. eqnegad
71. div2neg
72. divneg2
73. recclzi
74. recne0zi
75. recidzi
76. div1i
77. eqnegi
78. reccli
79. recidi
80. recreci
81. dividi
82. div0i
83. divclzi
84. divcan1zi
85. divcan2zi
86. divreczi
87. divcan3zi
88. divcan4zi
89. rec11i
90. divcli
91. divcan2i
92. divcan1i
93. divreci
94. divcan3i
95. divcan4i
96. divne0i
97. rec11ii
98. divasszi
99. divmulzi
100. divdirzi
101. divdiv23zi
102. divmuli
103. divdiv32i
104. divassi
105. divdiri
106. div23i
107. div11i
108. divmuldivi
109. divmul13i
110. divadddivi
111. divdivdivi
112. rerecclzi
113. rereccli
114. redivclzi
115. redivcli
116. div1d
117. reccld
118. recne0d
119. recidd
120. recid2d
121. recrecd
122. dividd
123. div0d
124. divcld
125. divcan1d
126. divcan2d
127. divrecd
128. divrec2d
129. divcan3d
130. divcan4d
131. diveq0d
132. diveq1d
133. diveq1ad
134. diveq0ad
135. divne1d
136. divne0bd
137. divnegd
138. divneg2d
139. div2negd
140. divne0d
141. recdivd
142. recdiv2d
143. divcan6d
144. ddcand
145. rec11d
146. divmuld
147. div32d
148. div13d
149. divdiv32d
150. divcan5d
151. divcan5rd
152. divcan7d
153. dmdcand
154. dmdcan2d
155. divdiv1d
156. divdiv2d
157. divmul2d
158. divmul3d
159. divassd
160. div12d
161. div23d
162. divdird
163. divsubdird
164. div11d
165. divmuldivd
166. divmul13d
167. divmul24d
168. divadddivd
169. divsubdivd
170. divmuleqd
171. divdivdivd
172. diveq1bd
173. div2sub
174. div2subd
175. rereccld
176. redivcld
177. subrecd
178. subrec
179. subreci
180. mvllmuld
181. mvllmuli
182. ldiv
183. rdiv
184. mdiv
185. 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. mulgt1OLD
23. ltmulgt11
24. ltmulgt12
25. mulgt1
26. lemulge11
27. lemulge12
28. ltdiv1
29. lediv1
30. gt0div
31. ge0div
32. divgt0
33. divge0
34. mulge0b
35. mulle0b
36. mulsuble0b
37. ltmuldiv
38. ltmuldiv2
39. ltdivmul
40. ledivmul
41. ltdivmul2
42. lt2mul2div
43. ledivmul2
44. lemuldiv
45. lemuldiv2
46. ltrec
47. lerec
48. lt2msq1
49. lt2msq
50. ltdiv2
51. ltrec1
52. lerec2
53. ledivdiv
54. lediv2
55. ltdiv23
56. lediv23
57. lediv12a
58. lediv2a
59. reclt1
60. recgt1
61. recgt1i
62. recp1lt1
63. recreclt
64. le2msq
65. msq11
66. ledivp1
67. squeeze0
68. ltp1i
69. recgt0i
70. recgt0ii
71. prodgt0i
72. divgt0i
73. divge0i
74. ltreci
75. lereci
76. lt2msqi
77. le2msqi
78. msq11i
79. divgt0i2i
80. ltrecii
81. divgt0ii
82. ltmul1i
83. ltdiv1i
84. ltmuldivi
85. ltmul2i
86. lemul1i
87. lemul2i
88. ltdiv23i
89. ledivp1i
90. ltdivp1i
91. ltdiv23ii
92. ltmul1ii
93. ltdiv1ii
94. ltp1d
95. lep1d
96. ltm1d
97. lem1d
98. recgt0d
99. divgt0d
100. mulgt1d
101. lemulge11d
102. lemulge12d
103. lemul1ad
104. lemul2ad
105. ltmul12ad
106. lemul12ad
107. lemul12bd
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
Imaginary and complex number properties
1. inelr
2. rimul
3. cru
4. crne0
5. creur
6. creui
7. cju
Function operation analogue theorems