Theorem List for Intuitionistic Logic Explorer - 7401-7500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | subcani 7401 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | subcan2i 7402 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | pnncani 7403 |
Cancellation law for mixed addition and subtraction. (Contributed by
NM, 14-Jan-2006.)
|
|
|
Theorem | addsub4i 7404 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 17-Oct-1999.)
|
|
|
Theorem | 0reALT 7405 |
Alternate proof of 0re 7119. (Contributed by NM, 19-Feb-2005.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | negcld 7406 |
Closure law for negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subidd 7407 |
Subtraction of a number from itself. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subid1d 7408 |
Identity law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negidd 7409 |
Addition of a number and its negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negnegd 7410 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negeq0d 7411 |
A number is zero iff its negative is zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negne0bd 7412 |
A number is nonzero iff its negative is nonzero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negcon1d 7413 |
Contraposition law for unary minus. Deduction form of negcon1 7360.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | negcon1ad 7414 |
Contraposition law for unary minus. One-way deduction form of
negcon1 7360. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | neg11ad 7415 |
The negatives of two complex numbers are equal iff they are equal.
Deduction form of neg11 7359. Generalization of neg11d 7431.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | negned 7416 |
If two complex numbers are unequal, so are their negatives.
Contrapositive of neg11d 7431. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | negne0d 7417 |
The negative of a nonzero number is nonzero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negrebd 7418 |
The negative of a real is real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | subcld 7419 |
Closure law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pncand 7420 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pncan2d 7421 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pncan3d 7422 |
Subtraction and addition of equals. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | npcand 7423 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nncand 7424 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negsubd 7425 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subnegd 7426 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subeq0d 7427 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subne0d 7428 |
Two unequal numbers have nonzero difference. See also subap0d 7740 which
is the same thing for apartness rather than negated equality.
(Contributed by Mario Carneiro, 1-Jan-2017.)
|
|
|
Theorem | subeq0ad 7429 |
The difference of two complex numbers is zero iff they are equal.
Deduction form of subeq0 7334. Generalization of subeq0d 7427.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | subne0ad 7430 |
If the difference of two complex numbers is nonzero, they are unequal.
Converse of subne0d 7428. Contrapositive of subeq0bd 7483. (Contributed
by David Moews, 28-Feb-2017.)
|
|
|
Theorem | neg11d 7431 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negdid 7432 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negdi2d 7433 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negsubdid 7434 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negsubdi2d 7435 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | neg2subd 7436 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subaddd 7437 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subadd2d 7438 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | addsubassd 7439 |
Associative-type law for subtraction and addition. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsubd 7440 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subadd23d 7441 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsub12d 7442 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | npncand 7443 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nppcand 7444 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nppcan2d 7445 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nppcan3d 7446 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsubd 7447 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsub2d 7448 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsub3d 7449 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsub4d 7450 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | sub32d 7451 |
Swap the second and third terms in a double subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nnncand 7452 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nnncan1d 7453 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nnncan2d 7454 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | npncan3d 7455 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pnpcand 7456 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pnpcan2d 7457 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pnncand 7458 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ppncand 7459 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subcand 7460 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subcan2d 7461 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
22-Sep-2016.)
|
|
|
Theorem | subcanad 7462 |
Cancellation law for subtraction. Deduction form of subcan 7363.
Generalization of subcand 7460. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | subneintrd 7463 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcand 7460. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | subcan2ad 7464 |
Cancellation law for subtraction. Deduction form of subcan2 7333.
Generalization of subcan2d 7461. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | subneintr2d 7465 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcan2d 7461. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | addsub4d 7466 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subadd4d 7467 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | sub4d 7468 |
Rearrangement of 4 terms in a subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | 2addsubd 7469 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addsubeq4d 7470 |
Relation between sums and differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mvlraddd 7471 |
Move LHS right addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
|
|
Theorem | mvrraddd 7472 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
|
|
Theorem | subaddeqd 7473 |
Transfer two terms of a subtraction to an addition in an equality.
(Contributed by Thierry Arnoux, 2-Feb-2020.)
|
|
|
Theorem | addlsub 7474 |
Left-subtraction: Subtraction of the left summand from the result of an
addition. (Contributed by BJ, 6-Jun-2019.)
|
|
|
Theorem | addrsub 7475 |
Right-subtraction: Subtraction of the right summand from the result of
an addition. (Contributed by BJ, 6-Jun-2019.)
|
|
|
Theorem | subexsub 7476 |
A subtraction law: Exchanging the subtrahend and the result of the
subtraction. (Contributed by BJ, 6-Jun-2019.)
|
|
|
Theorem | addid0 7477 |
If adding a number to a another number yields the other number, the added
number must be .
This shows that is the
unique (right)
identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
|
|
|
Theorem | addn0nid 7478 |
Adding a nonzero number to a complex number does not yield the complex
number. (Contributed by AV, 17-Jan-2021.)
|
|
|
Theorem | pnpncand 7479 |
Addition/subtraction cancellation law. (Contributed by Scott Fenton,
14-Dec-2017.)
|
|
|
Theorem | subeqrev 7480 |
Reverse the order of subtraction in an equality. (Contributed by Scott
Fenton, 8-Jul-2013.)
|
|
|
Theorem | pncan1 7481 |
Cancellation law for addition and subtraction with 1. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
|
|
Theorem | npcan1 7482 |
Cancellation law for subtraction and addition with 1. (Contributed by
Alexander van der Vekens, 5-Oct-2018.)
|
|
|
Theorem | subeq0bd 7483 |
If two complex numbers are equal, their difference is zero. Consequence
of subeq0ad 7429. Converse of subeq0d 7427. Contrapositive of subne0ad 7430.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | renegcld 7484 |
Closure law for negative of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | resubcld 7485 |
Closure law for subtraction of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negf1o 7486* |
Negation is an isomorphism of a subset of the real numbers to the
negated elements of the subset. (Contributed by AV, 9-Aug-2020.)
|
|
|
3.3.3 Multiplication
|
|
Theorem | kcnktkm1cn 7487 |
k times k minus 1 is a complex number if k is a complex number.
(Contributed by Alexander van der Vekens, 11-Mar-2018.)
|
|
|
Theorem | muladd 7488 |
Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened
by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | subdi 7489 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 18-Nov-2004.)
|
|
|
Theorem | subdir 7490 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 30-Dec-2005.)
|
|
|
Theorem | mul02 7491 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 10-Aug-1999.)
|
|
|
Theorem | mul02lem2 7492 |
Zero times a real is zero. Although we prove it as a corollary of
mul02 7491, the name is for consistency with the
Metamath Proof Explorer
which proves it before mul02 7491. (Contributed by Scott Fenton,
3-Jan-2013.)
|
|
|
Theorem | mul01 7493 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | mul02i 7494 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
NM, 23-Nov-1994.)
|
|
|
Theorem | mul01i 7495 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|
|
|
Theorem | mul02d 7496 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mul01d 7497 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ine0 7498 |
The imaginary unit
is not zero. (Contributed by NM,
6-May-1999.)
|
|
|
Theorem | mulneg1 7499 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | mulneg2 7500 |
The product with a negative is the negative of the product. (Contributed
by NM, 30-Jul-2004.)
|
|