Home | Metamath
Proof Explorer Theorem List (p. 103 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dedekindle 10201* | The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013.) |
Theorem | mul12 10202 | Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.) |
Theorem | mul32 10203 | Commutative/associative law. (Contributed by NM, 8-Oct-1999.) |
Theorem | mul31 10204 | Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mul4 10205 | Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.) |
Theorem | muladd11 10206 | A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.) |
Theorem | 1p1times 10207 | Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | peano2cn 10208 | A theorem for complex numbers analogous the second Peano postulate peano2nn 11032. (Contributed by NM, 17-Aug-2005.) |
Theorem | peano2re 10209 | A theorem for reals analogous the second Peano postulate peano2nn 11032. (Contributed by NM, 5-Jul-2005.) |
Theorem | readdcan 10210 | Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | 00id 10211 | is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mul02lem1 10212 | Lemma for mul02 10214. If any real does not produce when multiplied by , then any complex is equal to double itself. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mul02lem2 10213 | Lemma for mul02 10214. Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mul02 10214 | Multiplication by . Theorem I.6 of [Apostol] p. 18. Based on ideas by Eric Schmidt. (Contributed by NM, 10-Aug-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | mul01 10215 | Multiplication by . Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | addid1 10216 | is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | cnegex 10217* | Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | cnegex2 10218* | Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | addid2 10219 | is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | addcan 10220 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | addcan2 10221 | Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | addcom 10222 | Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | addid1i 10223 | is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | addid2i 10224 | is a left identity for addition. (Contributed by NM, 3-Jan-2013.) |
Theorem | mul02i 10225 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) |
Theorem | mul01i 10226 | Multiplication by . Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | addcomi 10227 | Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | addcomli 10228 | Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Theorem | addcani 10229 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | addcan2i 10230 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 14-May-2003.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | mul12i 10231 | Commutative/associative law that swaps the first two factors in a triple product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | mul32i 10232 | Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.) |
Theorem | mul4i 10233 | Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.) |
Theorem | mul02d 10234 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mul01d 10235 | Multiplication by . Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addid1d 10236 | is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addid2d 10237 | is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcomd 10238 | Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | addcand 10239 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcan2d 10240 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcanad 10241 | Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 10239. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | addcan2ad 10242 | Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 10240. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | addneintrd 10243 | Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 10241. Consequence of addcand 10239. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | addneintr2d 10244 | Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 10242. Consequence of addcan2d 10240. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | mul12d 10245 | Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mul32d 10246 | Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mul31d 10247 | Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mul4d 10248 | Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | muladd11r 10249 | A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.) |
Theorem | comraddd 10250 | Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
Theorem | ltaddneg 10251 | Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | ltaddnegr 10252 | Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021.) |
Theorem | add12 10253 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004.) |
Theorem | add32 10254 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999.) |
Theorem | add32r 10255 | Commutative/associative law that swaps the last two terms in a triple sum, rearranging the parentheses. (Contributed by Paul Chapman, 18-May-2007.) |
Theorem | add4 10256 | Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | add42 10257 | Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.) |
Theorem | add12i 10258 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997.) |
Theorem | add32i 10259 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 21-Jan-1997.) |
Theorem | add4i 10260 | Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.) |
Theorem | add42i 10261 | Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | add12d 10262 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | add32d 10263 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | add4d 10264 | Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | add42d 10265 | Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.) |
Syntax | cmin 10266 | Extend class notation to include subtraction. |
Syntax | cneg 10267 | Extend class notation to include unary minus. The symbol is not a class by itself but part of a compound class definition. We do this rather than making it a formal function since it is so commonly used. Note: We use different symbols for unary minus () and subtraction cmin 10266 () to prevent syntax ambiguity. For example, looking at the syntax definition co 6650, if we used the same symbol then " " could mean either " " minus "", or it could represent the (meaningless) operation of classes " " and " " connected with "operation" "". On the other hand, " " is unambiguous. |
Definition | df-sub 10268* | Define subtraction. Theorem subval 10272 shows its value (and describes how this definition works), theorem subaddi 10368 relates it to addition, and theorems subcli 10357 and resubcli 10343 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
Definition | df-neg 10269 | Define the negative of a number (unary minus). We use different symbols for unary minus () and subtraction () to prevent syntax ambiguity. See cneg 10267 for a discussion of this. (Contributed by NM, 10-Feb-1995.) |
Theorem | 0cnALT 10270 | Alternate proof of 0cn 10032 which does not reference ax-1cn 9994. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | negeu 10271* | Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | subval 10272* | Value of subtraction, which is the (unique) element such that . (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 2-Nov-2013.) |
Theorem | negeq 10273 | Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
Theorem | negeqi 10274 | Equality inference for negatives. (Contributed by NM, 14-Feb-1995.) |
Theorem | negeqd 10275 | Equality deduction for negatives. (Contributed by NM, 14-May-1999.) |
Theorem | nfnegd 10276 | Deduction version of nfneg 10277. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nfneg 10277 | Bound-variable hypothesis builder for the negative of a complex number. (Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | csbnegg 10278 | Move class substitution in and out of the negative of a number. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | negex 10279 | A negative is a set. (Contributed by NM, 4-Apr-2005.) |
Theorem | subcl 10280 | Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.) |
Theorem | negcl 10281 | Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
Theorem | negicn 10282 | is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) |
Theorem | subf 10283 | Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Theorem | subadd 10284 | Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.) |
Theorem | subadd2 10285 | Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Theorem | subsub23 10286 | Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.) |
Theorem | pncan 10287 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | pncan2 10288 | Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.) |
Theorem | pncan3 10289 | Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.) |
Theorem | npcan 10290 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | addsubass 10291 | Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | addsub 10292 | Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | subadd23 10293 | Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.) |
Theorem | addsub12 10294 | Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.) |
Theorem | 2addsub 10295 | Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.) |
Theorem | addsubeq4 10296 | Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.) |
Theorem | pncan3oi 10297 | Subtraction and addition of equals. Almost but not exactly the same as pncan3i 10358 and pncan 10287, this order happens often when applying "operations to both sides" so create a theorem specifically for it. A deduction version of this is available as pncand 10393. (Contributed by David A. Wheeler, 11-Oct-2018.) |
Theorem | mvrraddi 10298 | Move RHS right addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
Theorem | mvlladdi 10299 | Move LHS left addition to RHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
Theorem | subid 10300 | Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |