Home | Metamath
Proof Explorer Theorem List (p. 104 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subid1 10301 | Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) | ||
Theorem | npncan 10302 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) | ||
Theorem | nppcan 10303 | Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) | ||
Theorem | nnpcan 10304 | 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 10305 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) | ||
Theorem | subcan2 10306 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | subeq0 10307 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | npncan2 10308 | Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0) | ||
Theorem | subsub2 10309 | Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) | ||
Theorem | nncan 10310 | Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | ||
Theorem | subsub 10311 | Law for double subtraction. (Contributed by NM, 13-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) | ||
Theorem | nppcan2 10312 | Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) | ||
Theorem | subsub3 10313 | Law for double subtraction. (Contributed by NM, 27-Jul-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) | ||
Theorem | subsub4 10314 | Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) | ||
Theorem | sub32 10315 | Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) | ||
Theorem | nnncan 10316 | Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) | ||
Theorem | nnncan1 10317 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵)) | ||
Theorem | nnncan2 10318 | Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵)) | ||
Theorem | npncan3 10319 | Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵)) | ||
Theorem | pnpcan 10320 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶)) | ||
Theorem | pnpcan2 10321 | Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) | ||
Theorem | pnncan 10322 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)) | ||
Theorem | ppncan 10323 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶)) | ||
Theorem | addsub4 10324 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))) | ||
Theorem | subadd4 10325 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶))) | ||
Theorem | sub4 10326 | Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) | ||
Theorem | neg0 10327 | Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.) |
⊢ -0 = 0 | ||
Theorem | negid 10328 | Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) | ||
Theorem | negsub 10329 | 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 10330 | Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
Theorem | negneg 10331 | 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 10332 | Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | negcon1 10333 | Negative contraposition law. (Contributed by NM, 9-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
Theorem | negcon2 10334 | Negative contraposition law. (Contributed by NM, 14-Nov-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)) | ||
Theorem | negeq0 10335 | 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 10336 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | negsubdi 10337 | Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) | ||
Theorem | negdi 10338 | Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | ||
Theorem | negdi2 10339 | Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) | ||
Theorem | negsubdi2 10340 | Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) | ||
Theorem | neg2sub 10341 | Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) | ||
Theorem | renegcli 10342 | Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 10344 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 10343 | Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℝ | ||
Theorem | renegcl 10344 | Closure law for negative of reals. The weak deduction theorem dedth 4139 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 10342, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
Theorem | resubcl 10345 | Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | negreb 10346 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)) | ||
Theorem | peano2cnm 10347 | "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 10348 | "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.) |
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ) | ||
Theorem | negcli 10349 | Closure law for negative. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ -𝐴 ∈ ℂ | ||
Theorem | negidi 10350 | Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + -𝐴) = 0 | ||
Theorem | negnegi 10351 | 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 10352 | Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐴) = 0 | ||
Theorem | subid1i 10353 | Identity law for subtraction. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 0) = 𝐴 | ||
Theorem | negne0bi 10354 | A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0) | ||
Theorem | negrebi 10355 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ) | ||
Theorem | negne0i 10356 | The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ -𝐴 ≠ 0 | ||
Theorem | subcli 10357 | Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℂ | ||
Theorem | pncan3i 10358 | Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵 | ||
Theorem | negsubi 10359 | 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 10360 | Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵) | ||
Theorem | subeq0i 10361 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵) | ||
Theorem | neg11i 10362 | Negative is one-to-one. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | negcon1i 10363 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴) | ||
Theorem | negcon2i 10364 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴) | ||
Theorem | negdii 10365 | Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by OpenAI, 25-Mar-2011.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 + 𝐵) = (-𝐴 + -𝐵) | ||
Theorem | negsubdii 10366 | Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (-𝐴 + 𝐵) | ||
Theorem | negsubdi2i 10367 | Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴) | ||
Theorem | subaddi 10368 | Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴) | ||
Theorem | subadd2i 10369 | Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴) | ||
Theorem | subaddrii 10370 | Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐵 + 𝐶) = 𝐴 ⇒ ⊢ (𝐴 − 𝐵) = 𝐶 | ||
Theorem | subsub23i 10371 | Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵) | ||
Theorem | addsubassi 10372 | Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)) | ||
Theorem | addsubi 10373 | Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵) | ||
Theorem | subcani 10374 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶) | ||
Theorem | subcan2i 10375 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵) | ||
Theorem | pnncani 10376 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶) | ||
Theorem | addsub4i 10377 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)) | ||
Theorem | 0reALT 10378 | Alternate proof of 0re 10040. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℝ | ||
Theorem | negcld 10379 | Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℂ) | ||
Theorem | subidd 10380 | Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐴) = 0) | ||
Theorem | subid1d 10381 | Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 0) = 𝐴) | ||
Theorem | negidd 10382 | Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + -𝐴) = 0) | ||
Theorem | negnegd 10383 | 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 10384 | A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = 0 ↔ -𝐴 = 0)) | ||
Theorem | negne0bd 10385 | A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) | ||
Theorem | negcon1d 10386 | Contraposition law for unary minus. Deduction form of negcon1 10333. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
Theorem | negcon1ad 10387 | Contraposition law for unary minus. One-way deduction form of negcon1 10333. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐵 = 𝐴) | ||
Theorem | neg11ad 10388 | The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 10332. Generalization of neg11d 10404. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | negned 10389 | If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 10404. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → -𝐴 ≠ -𝐵) | ||
Theorem | negne0d 10390 | The negative of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → -𝐴 ≠ 0) | ||
Theorem | negrebd 10391 | The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | subcld 10392 | Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | pncand 10393 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | pncan2d 10394 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵) | ||
Theorem | pncan3d 10395 | Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) | ||
Theorem | npcand 10396 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
Theorem | nncand 10397 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | ||
Theorem | negsubd 10398 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵)) | ||
Theorem | subnegd 10399 | Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
Theorem | subeq0d 10400 | If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |