![]() |
Metamath
Proof Explorer Theorem List (p. 116 of 478) | < 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-30149) |
![]() (30150-31672) |
![]() (31673-47754) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sub4 11501 | Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) | ||
Theorem | neg0 11502 | Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.) |
⊢ -0 = 0 | ||
Theorem | negid 11503 | Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) | ||
Theorem | negsub 11504 | 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 11505 | Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
Theorem | negneg 11506 | 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 11507 | Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | negcon1 11508 | Negative contraposition law. (Contributed by NM, 9-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
Theorem | negcon2 11509 | Negative contraposition law. (Contributed by NM, 14-Nov-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)) | ||
Theorem | negeq0 11510 | 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 11511 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | negsubdi 11512 | Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) | ||
Theorem | negdi 11513 | Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | ||
Theorem | negdi2 11514 | Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) | ||
Theorem | negsubdi2 11515 | Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) | ||
Theorem | neg2sub 11516 | Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) | ||
Theorem | renegcli 11517 | Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11519 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 11518 | Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℝ | ||
Theorem | renegcl 11519 | Closure law for negative of reals. The weak deduction theorem dedth 4585 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11517, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
Theorem | resubcl 11520 | Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | negreb 11521 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)) | ||
Theorem | peano2cnm 11522 | "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 11523 | "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.) |
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ) | ||
Theorem | negcli 11524 | Closure law for negative. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ -𝐴 ∈ ℂ | ||
Theorem | negidi 11525 | Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + -𝐴) = 0 | ||
Theorem | negnegi 11526 | 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 11527 | Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐴) = 0 | ||
Theorem | subid1i 11528 | Identity law for subtraction. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 0) = 𝐴 | ||
Theorem | negne0bi 11529 | A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0) | ||
Theorem | negrebi 11530 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ) | ||
Theorem | negne0i 11531 | The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ -𝐴 ≠ 0 | ||
Theorem | subcli 11532 | Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℂ | ||
Theorem | pncan3i 11533 | Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵 | ||
Theorem | negsubi 11534 | 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 11535 | Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵) | ||
Theorem | subeq0i 11536 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵) | ||
Theorem | neg11i 11537 | Negative is one-to-one. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | negcon1i 11538 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴) | ||
Theorem | negcon2i 11539 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴) | ||
Theorem | negdii 11540 | Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by OpenAI, 25-Mar-2011.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 + 𝐵) = (-𝐴 + -𝐵) | ||
Theorem | negsubdii 11541 | Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (-𝐴 + 𝐵) | ||
Theorem | negsubdi2i 11542 | Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴) | ||
Theorem | subaddi 11543 | Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴) | ||
Theorem | subadd2i 11544 | Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴) | ||
Theorem | subaddrii 11545 | Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐵 + 𝐶) = 𝐴 ⇒ ⊢ (𝐴 − 𝐵) = 𝐶 | ||
Theorem | subsub23i 11546 | Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵) | ||
Theorem | addsubassi 11547 | Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)) | ||
Theorem | addsubi 11548 | Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵) | ||
Theorem | subcani 11549 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶) | ||
Theorem | subcan2i 11550 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵) | ||
Theorem | pnncani 11551 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶) | ||
Theorem | addsub4i 11552 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)) | ||
Theorem | 0reALT 11553 | Alternate proof of 0re 11212. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℝ | ||
Theorem | negcld 11554 | Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℂ) | ||
Theorem | subidd 11555 | Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐴) = 0) | ||
Theorem | subid1d 11556 | Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 0) = 𝐴) | ||
Theorem | negidd 11557 | Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + -𝐴) = 0) | ||
Theorem | negnegd 11558 | 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 11559 | A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = 0 ↔ -𝐴 = 0)) | ||
Theorem | negne0bd 11560 | A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) | ||
Theorem | negcon1d 11561 | Contraposition law for unary minus. Deduction form of negcon1 11508. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
Theorem | negcon1ad 11562 | Contraposition law for unary minus. One-way deduction form of negcon1 11508. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐵 = 𝐴) | ||
Theorem | neg11ad 11563 | The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 11507. Generalization of neg11d 11579. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | negned 11564 | If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 11579. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → -𝐴 ≠ -𝐵) | ||
Theorem | negne0d 11565 | The negative of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → -𝐴 ≠ 0) | ||
Theorem | negrebd 11566 | The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | subcld 11567 | Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | pncand 11568 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | pncan2d 11569 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵) | ||
Theorem | pncan3d 11570 | Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) | ||
Theorem | npcand 11571 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
Theorem | nncand 11572 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | ||
Theorem | negsubd 11573 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵)) | ||
Theorem | subnegd 11574 | Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
Theorem | subeq0d 11575 | If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | subne0d 11576 | Two unequal numbers have nonzero difference. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) | ||
Theorem | subeq0ad 11577 | The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 11482. Generalization of subeq0d 11575. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | subne0ad 11578 | If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 11576. Contrapositive of subeq0bd 11636. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | neg11d 11579 | If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = -𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | negdid 11580 | Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | ||
Theorem | negdi2d 11581 | Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) | ||
Theorem | negsubdid 11582 | Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) | ||
Theorem | negsubdi2d 11583 | Distribution of negative over subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) | ||
Theorem | neg2subd 11584 | Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) | ||
Theorem | subaddd 11585 | Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | subadd2d 11586 | Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) | ||
Theorem | addsubassd 11587 | Associative-type law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) | ||
Theorem | addsubd 11588 | Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) | ||
Theorem | subadd23d 11589 | Commutative/associative law for addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) | ||
Theorem | addsub12d 11590 | Commutative/associative law for addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) | ||
Theorem | npncand 11591 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) | ||
Theorem | nppcand 11592 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) | ||
Theorem | nppcan2d 11593 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) | ||
Theorem | nppcan3d 11594 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) | ||
Theorem | subsubd 11595 | Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) | ||
Theorem | subsub2d 11596 | Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) | ||
Theorem | subsub3d 11597 | Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) | ||
Theorem | subsub4d 11598 | Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) | ||
Theorem | sub32d 11599 | Swap the second and third terms in a double subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) | ||
Theorem | nnncand 11600 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |