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