| Metamath Proof Explorer | < Previous Next > | |
| Browser slow? Try the
Unicode version. |
| Color key: | (1-11257) |
(11258-12844) |
(12845-19026) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mulge0 7201 | The product of two nonnegative numbers is nonnegative. |
| Theorem | mulge0OLD 7202 | The product of two nonnegative numbers is nonnegative. |
| Theorem | mullt0 7203 | The product of two negative numbers is positive. (Contributed by Jeffrey Hankins, 8-Jun-2009.) |
| Theorem | lt01 7204 | 0 is less than 1. Theorem I.21 of [Apostol] p. 20. |
| Reciprocals | ||
| Theorem | ixi 7205 |
|
| Theorem | recextlem1 7206 | Lemma for recex 7208. [Auxiliary lemma - not displayed.] |
| Theorem | recextlem2 7207 | Lemma for recex 7208. [Auxiliary lemma - not displayed.] |
| Theorem | recex 7208 | Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007.) |
| Theorem | recexi 7209 | Existence of reciprocals. |
| Theorem | mulcani 7210 | Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. |
| Theorem | mulcant2i 7211 | Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. Illustrates use of keephyp 3221. |
| Theorem | mulcan 7212 | Cancellation law for multiplication (full theorem form). Theorem I.7 of [Apostol] p. 18. Illustrates use of dedth 3208 and elimne0 6820. |
| Theorem | mulcan2 7213 | Cancellation law for multiplication. |
| Theorem | mul0ori 7214 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. |
| Theorem | msq0i 7215 | A number is zero iff its square is zero (where square is represented using multiplication). |
| Theorem | mul0or 7216 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. |
| Theorem | mulne0b 7217 | The product of two nonzero numbers is nonzero. (The proof was shortened by Andrew Salmon, 19-Nov-2011.) |
| Theorem | mulne0 7218 | The product of two nonzero numbers is nonzero. |
| Theorem | mulne0i 7219 | The product of two nonzero numbers is nonzero. |
| Theorem | muleqadd 7220 | Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12. |
| Theorem | receui 7221 | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. |
| Theorem | mulnzcnopr 7222 | Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.) |
| Division | ||
| Definition | df-div 7223 | Define division. Theorem divmuli 7225 relates it to multiplication, and divcli 7230 and redivcli 7307 prove its closure laws. |
| Theorem | divvali 7224 |
Value of division: the (unique) element |
| Theorem | divmuli 7225 | Relationship between division and multiplication. |
| Theorem | divmulzi 7226 | Relationship between division and multiplication. |
| Theorem | divmul 7227 | Relationship between division and multiplication. |
| Theorem | divmul2 7228 | Relationship between division and multiplication. |
| Theorem | divmul3 7229 | Relationship between division and multiplication. |
| Theorem | divcli 7230 | Closure law for division. |
| Theorem | divclzi 7231 | Closure law for division. |
| Theorem | divcl 7232 | Closure law for division. |
| Theorem | reccli 7233 | Closure law for reciprocal. |
| Theorem | recclzi 7234 | Closure law for reciprocal. |
| Theorem | reccl 7235 | Closure law for reciprocal. |
| Theorem | divcan2i 7236 | A cancellation law for division. |
| Theorem | divcan1i 7237 | A cancellation law for division. |
| Theorem | divcan1zi 7238 | A cancellation law for division. |
| Theorem | divcan2zi 7239 |
A cancellation law for division. We eliminate the third hypothesis of
divcan2i 7236 using the weak deduction theorem dedth 3208 and keep the other
two. Because the first hypothesis shares the class variable |
| Theorem | divcan1 7240 | A cancellation law for division. |
| Theorem | divcan2 7241 | A cancellation law for division. |
| Theorem | divne0b 7242 | The ratio of nonzero numbers is nonzero. |
| Theorem | divne0 7243 | The ratio of nonzero numbers is nonzero. |
| Theorem | divne0i 7244 | The ratio of nonzero numbers is nonzero. |
| Theorem | recne0zi 7245 | The reciprocal of a nonzero number is nonzero. |
| Theorem | recne0 7246 | The reciprocal of a nonzero number is nonzero. |
| Theorem | recidi 7247 | Multiplication of a number and its reciprocal. |
| Theorem | recidzi 7248 | Multiplication of a number and its reciprocal. |
| Theorem | recid 7249 | Multiplication of a number and its reciprocal. |
| Theorem | recid2 7250 | Multiplication of a number and its reciprocal. |
| Theorem | divreci 7251 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. |
| Theorem | divreczi 7252 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. |
| Theorem | divrec 7253 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. |
| Theorem | divrec2 7254 | Relationship between division and reciprocal. |
| Theorem | divass 7255 | An associative law for division. |
| Theorem | div23 7256 | A commutative/associative law for division. |
| Theorem | div13 7257 | A commutative/associative law for division. |
| Theorem | div12 7258 | A commutative/associative law for division. |
| Theorem | divasszi 7259 | An associative law for division. |
| Theorem | divassi 7260 | An associative law for division. |
| Theorem | divdiri 7261 | Distribution of division over addition. |
| Theorem | div23i 7262 | A commutative/associative law for division. |
| Theorem | divdirzi 7263 | Distribution of division over addition. |
| Theorem | divdir 7264 | Distribution of division over addition. |
| Theorem | divcan3i 7265 | A cancellation law for division. |
| Theorem | divcan4i 7266 | A cancellation law for division. |
| Theorem | divcan3zi 7267 | A cancellation law for division. (Eliminates a hypothesis of divcan3i 7265 with the weak deduction theorem.) |
| Theorem | divcan4zi 7268 | A cancellation law for division. |
| Theorem | divcan3 7269 | A cancellation law for division. |
| Theorem | divcan4 7270 | A cancellation law for division. |
| Theorem | div11i 7271 | One-to-one relationship for division. |
| Theorem | div11 7272 | One-to-one relationship for division. |
| Theorem | divid 7273 | A number divided by itself is one. |
| Theorem | div0 7274 | Division into zero is zero. |
| Theorem | diveq0 7275 | A ratio is zero iff the numerator is zero. |
| Theorem | recreci 7276 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. |
| Theorem | dividi 7277 | A number divided by itself is one. |
| Theorem | div0i 7278 | Division into zero is zero. |
| Theorem | div1i 7279 | A number divided by 1 is itself. |
| Theorem | div1 7280 | A number divided by 1 is itself. |
| Theorem | divneg 7281 | Move negative sign inside of a division. |
| Theorem | divsubdir 7282 | Distribution of division over subtraction. |
| Theorem | recrec 7283 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. |
| Theorem | rec11ii 7284 | Reciprocal is one-to-one. |
| Theorem | rec11i 7285 | Reciprocal is one-to-one. |
| Theorem | rec11r 7286 | Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.) |
| Theorem | divmuldiv 7287 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. |
| Theorem | divcan5 7288 | Cancellation of common factor in a ratio. |
| Theorem | divmul13 7289 | Swap the denominators in the product of two ratios. |
| Theorem | divmul24 7290 | Swap the numerators in the product of two ratios. |
| Theorem | divadddiv 7291 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. |
| Theorem | divdivdiv 7292 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. |
| Theorem | divdivdivOLD 7293 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. |
| Theorem | divmuldivi 7294 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. |
| Theorem | divmul13i 7295 | Swap denominators of two ratios. |
| Theorem | divadddivi 7296 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. |
| Theorem | divdivdivi 7297 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. |
| Theorem | recdiv 7298 | The reciprocal of a ratio. |
| Theorem | divcan6 7299 | Cancellation of inverted fractions. |
| Theorem | divdiv23 7300 | Swap denominators in a division. |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |