| Metamath
Proof Explorer Theorem List (p. 116 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | negeqi 11501 | Equality inference for negatives. (Contributed by NM, 14-Feb-1995.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝐴 = -𝐵 | ||
| Theorem | negeqd 11502 | Equality deduction for negatives. (Contributed by NM, 14-May-1999.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐴 = -𝐵) | ||
| Theorem | nfnegd 11503 | Deduction version of nfneg 11504. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝐴) | ||
| Theorem | nfneg 11504 | 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 11505 | 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 11506 | A negative is a set. (Contributed by NM, 4-Apr-2005.) |
| ⊢ -𝐴 ∈ V | ||
| Theorem | subcl 11507 | Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
| Theorem | negcl 11508 | Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
| ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) | ||
| Theorem | negicn 11509 | -i is a complex number. (Contributed by David A. Wheeler, 7-Dec-2018.) |
| ⊢ -i ∈ ℂ | ||
| Theorem | subf 11510 | Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
| ⊢ − :(ℂ × ℂ)⟶ℂ | ||
| Theorem | subadd 11511 | Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
| Theorem | subadd2 11512 | Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) | ||
| Theorem | subsub23 11513 | Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
| Theorem | pncan 11514 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
| Theorem | pncan2 11515 | Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵) | ||
| Theorem | pncan3 11516 | Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Steven Nguyen, 8-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) | ||
| Theorem | npcan 11517 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
| Theorem | addsubass 11518 | Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) | ||
| Theorem | addsub 11519 | Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) | ||
| Theorem | subadd23 11520 | Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) | ||
| Theorem | addsub12 11521 | Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) | ||
| Theorem | 2addsub 11522 | Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) | ||
| Theorem | addsubeq4 11523 | Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷))) | ||
| Theorem | pncan3oi 11524 | Subtraction and addition of equals. Almost but not exactly the same as pncan3i 11586 and pncan 11514, 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 11621. (Contributed by David A. Wheeler, 11-Oct-2018.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴 | ||
| Theorem | mvrraddi 11525 | Move the right term in a sum on the RHS to the LHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
| ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐴 = (𝐵 + 𝐶) ⇒ ⊢ (𝐴 − 𝐶) = 𝐵 | ||
| Theorem | mvrladdi 11526 | Move the left term in a sum on the RHS to the LHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
| ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐴 = (𝐵 + 𝐶) ⇒ ⊢ (𝐴 − 𝐵) = 𝐶 | ||
| Theorem | mvlladdi 11527 | Move the left term in a sum on the LHS to the RHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ 𝐵 = (𝐶 − 𝐴) | ||
| Theorem | subid 11528 | Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) | ||
| Theorem | subid1 11529 | Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) | ||
| Theorem | npncan 11530 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) | ||
| Theorem | nppcan 11531 | Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) | ||
| Theorem | nnpcan 11532 | Cancellation law for subtraction: ((a-b)-c)+b = a-c holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 24-Mar-2018.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) − 𝐶) + 𝐵) = (𝐴 − 𝐶)) | ||
| Theorem | nppcan3 11533 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) | ||
| Theorem | subcan2 11534 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | subeq0 11535 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
| Theorem | npncan2 11536 | Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0) | ||
| Theorem | subsub2 11537 | Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) | ||
| Theorem | nncan 11538 | Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | ||
| Theorem | subsub 11539 | Law for double subtraction. (Contributed by NM, 13-May-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) | ||
| Theorem | nppcan2 11540 | Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) | ||
| Theorem | subsub3 11541 | Law for double subtraction. (Contributed by NM, 27-Jul-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) | ||
| Theorem | subsub4 11542 | Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) | ||
| Theorem | sub32 11543 | Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) | ||
| Theorem | nnncan 11544 | Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) | ||
| Theorem | nnncan1 11545 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵)) | ||
| Theorem | nnncan2 11546 | Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵)) | ||
| Theorem | npncan3 11547 | Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵)) | ||
| Theorem | pnpcan 11548 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by SN, 13-Nov-2023.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶)) | ||
| Theorem | pnpcan2 11549 | Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) | ||
| Theorem | pnncan 11550 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)) | ||
| Theorem | ppncan 11551 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶)) | ||
| Theorem | addsub4 11552 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))) | ||
| Theorem | subadd4 11553 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶))) | ||
| Theorem | sub4 11554 | Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) | ||
| Theorem | neg0 11555 | Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.) |
| ⊢ -0 = 0 | ||
| Theorem | negid 11556 | Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) | ||
| Theorem | negsub 11557 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵)) | ||
| Theorem | subneg 11558 | Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
| Theorem | negneg 11559 | A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by NM, 12-Jan-2002.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝐴 ∈ ℂ → --𝐴 = 𝐴) | ||
| Theorem | neg11 11560 | Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | negcon1 11561 | Negative contraposition law. (Contributed by NM, 9-May-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
| Theorem | negcon2 11562 | Negative contraposition law. (Contributed by NM, 14-Nov-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)) | ||
| Theorem | negeq0 11563 | A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 = 0 ↔ -𝐴 = 0)) | ||
| Theorem | subcan 11564 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) | ||
| Theorem | negsubdi 11565 | Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) | ||
| Theorem | negdi 11566 | Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | ||
| Theorem | negdi2 11567 | Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) | ||
| Theorem | negsubdi2 11568 | Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) | ||
| Theorem | neg2sub 11569 | Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) | ||
| Theorem | renegcli 11570 | Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11572 is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ -𝐴 ∈ ℝ | ||
| Theorem | resubcli 11571 | Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℝ | ||
| Theorem | renegcl 11572 | Closure law for negative of reals. The weak deduction theorem dedth 4584 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11570, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
| Theorem | resubcl 11573 | Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) | ||
| Theorem | negreb 11574 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| ⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)) | ||
| Theorem | peano2cnm 11575 | "Reverse" second Peano postulate analogue for complex numbers: A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
| ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ) | ||
| Theorem | peano2rem 11576 | "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.) |
| ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ) | ||
| Theorem | negcli 11577 | Closure law for negative. (Contributed by NM, 26-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ -𝐴 ∈ ℂ | ||
| Theorem | negidi 11578 | Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + -𝐴) = 0 | ||
| Theorem | negnegi 11579 | A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by NM, 8-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ --𝐴 = 𝐴 | ||
| Theorem | subidi 11580 | Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐴) = 0 | ||
| Theorem | subid1i 11581 | Identity law for subtraction. (Contributed by NM, 29-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 0) = 𝐴 | ||
| Theorem | negne0bi 11582 | A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0) | ||
| Theorem | negrebi 11583 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ) | ||
| Theorem | negne0i 11584 | The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ -𝐴 ≠ 0 | ||
| Theorem | subcli 11585 | Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℂ | ||
| Theorem | pncan3i 11586 | Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵 | ||
| Theorem | negsubi 11587 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + -𝐵) = (𝐴 − 𝐵) | ||
| Theorem | subnegi 11588 | Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵) | ||
| Theorem | subeq0i 11589 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵) | ||
| Theorem | neg11i 11590 | Negative is one-to-one. (Contributed by NM, 1-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵) | ||
| Theorem | negcon1i 11591 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴) | ||
| Theorem | negcon2i 11592 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴) | ||
| Theorem | negdii 11593 | Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by OpenAI, 25-Mar-2011.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 + 𝐵) = (-𝐴 + -𝐵) | ||
| Theorem | negsubdii 11594 | Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (-𝐴 + 𝐵) | ||
| Theorem | negsubdi2i 11595 | Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴) | ||
| Theorem | subaddi 11596 | Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴) | ||
| Theorem | subadd2i 11597 | Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴) | ||
| Theorem | subaddrii 11598 | Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐵 + 𝐶) = 𝐴 ⇒ ⊢ (𝐴 − 𝐵) = 𝐶 | ||
| Theorem | subsub23i 11599 | Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵) | ||
| Theorem | addsubassi 11600 | Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |