Home | Metamath
Proof Explorer Theorem List (p. 110 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subeq0 10901 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | npncan2 10902 | Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0) | ||
Theorem | subsub2 10903 | Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) | ||
Theorem | nncan 10904 | Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | ||
Theorem | subsub 10905 | Law for double subtraction. (Contributed by NM, 13-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) | ||
Theorem | nppcan2 10906 | Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) | ||
Theorem | subsub3 10907 | Law for double subtraction. (Contributed by NM, 27-Jul-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) | ||
Theorem | subsub4 10908 | Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) | ||
Theorem | sub32 10909 | Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) | ||
Theorem | nnncan 10910 | Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) | ||
Theorem | nnncan1 10911 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵)) | ||
Theorem | nnncan2 10912 | Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵)) | ||
Theorem | npncan3 10913 | Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵)) | ||
Theorem | pnpcan 10914 | 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 10915 | Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) | ||
Theorem | pnncan 10916 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)) | ||
Theorem | ppncan 10917 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶)) | ||
Theorem | addsub4 10918 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))) | ||
Theorem | subadd4 10919 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶))) | ||
Theorem | sub4 10920 | Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) | ||
Theorem | neg0 10921 | Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.) |
⊢ -0 = 0 | ||
Theorem | negid 10922 | Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) | ||
Theorem | negsub 10923 | 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 10924 | Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
Theorem | negneg 10925 | 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 10926 | Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | negcon1 10927 | Negative contraposition law. (Contributed by NM, 9-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
Theorem | negcon2 10928 | Negative contraposition law. (Contributed by NM, 14-Nov-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)) | ||
Theorem | negeq0 10929 | 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 10930 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | negsubdi 10931 | Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) | ||
Theorem | negdi 10932 | Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | ||
Theorem | negdi2 10933 | Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) | ||
Theorem | negsubdi2 10934 | Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) | ||
Theorem | neg2sub 10935 | Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) | ||
Theorem | renegcli 10936 | Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 10938 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 10937 | Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℝ | ||
Theorem | renegcl 10938 | Closure law for negative of reals. The weak deduction theorem dedth 4521 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 10936, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
Theorem | resubcl 10939 | Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | negreb 10940 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)) | ||
Theorem | peano2cnm 10941 | "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 10942 | "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.) |
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ) | ||
Theorem | negcli 10943 | Closure law for negative. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ -𝐴 ∈ ℂ | ||
Theorem | negidi 10944 | Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + -𝐴) = 0 | ||
Theorem | negnegi 10945 | 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 10946 | Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐴) = 0 | ||
Theorem | subid1i 10947 | Identity law for subtraction. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 − 0) = 𝐴 | ||
Theorem | negne0bi 10948 | A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0) | ||
Theorem | negrebi 10949 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ) | ||
Theorem | negne0i 10950 | The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ -𝐴 ≠ 0 | ||
Theorem | subcli 10951 | Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℂ | ||
Theorem | pncan3i 10952 | Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵 | ||
Theorem | negsubi 10953 | 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 10954 | Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵) | ||
Theorem | subeq0i 10955 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵) | ||
Theorem | neg11i 10956 | Negative is one-to-one. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | negcon1i 10957 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴) | ||
Theorem | negcon2i 10958 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴) | ||
Theorem | negdii 10959 | Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by OpenAI, 25-Mar-2011.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 + 𝐵) = (-𝐴 + -𝐵) | ||
Theorem | negsubdii 10960 | Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (-𝐴 + 𝐵) | ||
Theorem | negsubdi2i 10961 | Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴) | ||
Theorem | subaddi 10962 | Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴) | ||
Theorem | subadd2i 10963 | Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴) | ||
Theorem | subaddrii 10964 | Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐵 + 𝐶) = 𝐴 ⇒ ⊢ (𝐴 − 𝐵) = 𝐶 | ||
Theorem | subsub23i 10965 | Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵) | ||
Theorem | addsubassi 10966 | Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)) | ||
Theorem | addsubi 10967 | Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵) | ||
Theorem | subcani 10968 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶) | ||
Theorem | subcan2i 10969 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵) | ||
Theorem | pnncani 10970 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶) | ||
Theorem | addsub4i 10971 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)) | ||
Theorem | 0reALT 10972 | Alternate proof of 0re 10632. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℝ | ||
Theorem | negcld 10973 | Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℂ) | ||
Theorem | subidd 10974 | Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐴) = 0) | ||
Theorem | subid1d 10975 | Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 0) = 𝐴) | ||
Theorem | negidd 10976 | Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + -𝐴) = 0) | ||
Theorem | negnegd 10977 | 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 10978 | A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = 0 ↔ -𝐴 = 0)) | ||
Theorem | negne0bd 10979 | A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) | ||
Theorem | negcon1d 10980 | Contraposition law for unary minus. Deduction form of negcon1 10927. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) | ||
Theorem | negcon1ad 10981 | Contraposition law for unary minus. One-way deduction form of negcon1 10927. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐵 = 𝐴) | ||
Theorem | neg11ad 10982 | The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 10926. Generalization of neg11d 10998. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | negned 10983 | If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 10998. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → -𝐴 ≠ -𝐵) | ||
Theorem | negne0d 10984 | The negative of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → -𝐴 ≠ 0) | ||
Theorem | negrebd 10985 | The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | subcld 10986 | Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | pncand 10987 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | pncan2d 10988 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵) | ||
Theorem | pncan3d 10989 | Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) | ||
Theorem | npcand 10990 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
Theorem | nncand 10991 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵) | ||
Theorem | negsubd 10992 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵)) | ||
Theorem | subnegd 10993 | Relationship between subtraction and negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 − -𝐵) = (𝐴 + 𝐵)) | ||
Theorem | subeq0d 10994 | If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | subne0d 10995 | Two unequal numbers have nonzero difference. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) | ||
Theorem | subeq0ad 10996 | The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 10901. Generalization of subeq0d 10994. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
Theorem | subne0ad 10997 | If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 10995. Contrapositive of subeq0bd 11055. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | neg11d 10998 | If the difference between two numbers is zero, they are equal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = -𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | negdid 10999 | Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | ||
Theorem | negdi2d 11000 | Distribution of negative over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |