Theorem List for Intuitionistic Logic Explorer - 8001-8100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | neg0 8001 |
Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|
⊢ -0 = 0 |
|
Theorem | negid 8002 |
Addition of a number and its negative. (Contributed by NM,
14-Mar-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) |
|
Theorem | negsub 8003 |
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 8004 |
Relationship between subtraction and negative. (Contributed by NM,
10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵)) |
|
Theorem | negneg 8005 |
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 8006 |
Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by
Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | negcon1 8007 |
Negative contraposition law. (Contributed by NM, 9-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) |
|
Theorem | negcon2 8008 |
Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)) |
|
Theorem | negeq0 8009 |
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 8010 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | negsubdi 8011 |
Distribution of negative over subtraction. (Contributed by NM,
15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) |
|
Theorem | negdi 8012 |
Distribution of negative over addition. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) |
|
Theorem | negdi2 8013 |
Distribution of negative over addition. (Contributed by NM,
1-Jan-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) |
|
Theorem | negsubdi2 8014 |
Distribution of negative over subtraction. (Contributed by NM,
4-Oct-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) |
|
Theorem | neg2sub 8015 |
Relationship between subtraction and negative. (Contributed by Paul
Chapman, 8-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) |
|
Theorem | renegcl 8016 |
Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) |
|
Theorem | renegcli 8017 |
Closure law for negative of reals. (Note: this inference proof style
and the deduction theorem usage in renegcl 8016 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 8018 |
Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℝ |
|
Theorem | resubcl 8019 |
Closure law for subtraction of reals. (Contributed by NM,
20-Jan-1997.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) |
|
Theorem | negreb 8020 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)) |
|
Theorem | peano2cnm 8021 |
"Reverse" second Peano postulate analog for complex numbers: A
complex
number minus 1 is a complex number. (Contributed by Alexander van der
Vekens, 18-Mar-2018.)
|
⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈
ℂ) |
|
Theorem | peano2rem 8022 |
"Reverse" second Peano postulate analog for reals. (Contributed by
NM,
6-Feb-2007.)
|
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
|
Theorem | negcli 8023 |
Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ -𝐴 ∈ ℂ |
|
Theorem | negidi 8024 |
Addition of a number and its negative. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + -𝐴) = 0 |
|
Theorem | negnegi 8025 |
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 8026 |
Subtraction of a number from itself. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 − 𝐴) = 0 |
|
Theorem | subid1i 8027 |
Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 − 0) = 𝐴 |
|
Theorem | negne0bi 8028 |
A number is nonzero iff its negative is nonzero. (Contributed by NM,
10-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0) |
|
Theorem | negrebi 8029 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ) |
|
Theorem | negne0i 8030 |
The negative of a nonzero number is nonzero. (Contributed by NM,
30-Jul-2004.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠
0 ⇒ ⊢ -𝐴 ≠ 0 |
|
Theorem | subcli 8031 |
Closure law for subtraction. (Contributed by NM, 26-Nov-1994.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℂ |
|
Theorem | pncan3i 8032 |
Subtraction and addition of equals. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵 |
|
Theorem | negsubi 8033 |
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 8034 |
Relationship between subtraction and negative. (Contributed by NM,
1-Dec-2005.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵) |
|
Theorem | subeq0i 8035 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵) |
|
Theorem | neg11i 8036 |
Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵) |
|
Theorem | negcon1i 8037 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴) |
|
Theorem | negcon2i 8038 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴) |
|
Theorem | negdii 8039 |
Distribution of negative over addition. (Contributed by NM,
28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ -(𝐴 + 𝐵) = (-𝐴 + -𝐵) |
|
Theorem | negsubdii 8040 |
Distribution of negative over subtraction. (Contributed by NM,
6-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (-𝐴 + 𝐵) |
|
Theorem | negsubdi2i 8041 |
Distribution of negative over subtraction. (Contributed by NM,
1-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴) |
|
Theorem | subaddi 8042 |
Relationship between subtraction and addition. (Contributed by NM,
26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴) |
|
Theorem | subadd2i 8043 |
Relationship between subtraction and addition. (Contributed by NM,
15-Dec-2006.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴) |
|
Theorem | subaddrii 8044 |
Relationship between subtraction and addition. (Contributed by NM,
16-Dec-2006.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐵 + 𝐶) = 𝐴 ⇒ ⊢ (𝐴 − 𝐵) = 𝐶 |
|
Theorem | subsub23i 8045 |
Swap subtrahend and result of subtraction. (Contributed by NM,
7-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵) |
|
Theorem | addsubassi 8046 |
Associative-type law for subtraction and addition. (Contributed by NM,
16-Sep-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)) |
|
Theorem | addsubi 8047 |
Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵) |
|
Theorem | subcani 8048 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶) |
|
Theorem | subcan2i 8049 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵) |
|
Theorem | pnncani 8050 |
Cancellation law for mixed addition and subtraction. (Contributed by
NM, 14-Jan-2006.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶) |
|
Theorem | addsub4i 8051 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 17-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)) |
|
Theorem | 0reALT 8052 |
Alternate proof of 0re 7759. (Contributed by NM, 19-Feb-2005.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ 0 ∈ ℝ |
|
Theorem | negcld 8053 |
Closure law for negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → -𝐴 ∈ ℂ) |
|
Theorem | subidd 8054 |
Subtraction of a number from itself. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − 𝐴) = 0) |
|
Theorem | subid1d 8055 |
Identity law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − 0) = 𝐴) |
|
Theorem | negidd 8056 |
Addition of a number and its negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + -𝐴) = 0) |
|
Theorem | negnegd 8057 |
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 8058 |
A number is zero iff its negative is zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 = 0 ↔ -𝐴 = 0)) |
|
Theorem | negne0bd 8059 |
A number is nonzero iff its negative is nonzero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)) |
|
Theorem | negcon1d 8060 |
Contraposition law for unary minus. Deduction form of negcon1 8007.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) |
|
Theorem | negcon1ad 8061 |
Contraposition law for unary minus. One-way deduction form of
negcon1 8007. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐵 = 𝐴) |
|
Theorem | neg11ad 8062 |
The negatives of two complex numbers are equal iff they are equal.
Deduction form of neg11 8006. Generalization of neg11d 8078.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | negned 8063 |
If two complex numbers are unequal, so are their negatives.
Contrapositive of neg11d 8078. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → -𝐴 ≠ -𝐵) |
|
Theorem | negne0d 8064 |
The negative of a nonzero number is nonzero. See also negap0d 8386 which
is similar but for apart from zero rather than not equal to zero.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → -𝐴 ≠ 0) |
|
Theorem | negrebd 8065 |
The negative of a real is real. (Contributed by Mario Carneiro,
28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → -𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) |
|
Theorem | subcld 8066 |
Closure law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ) |
|
Theorem | pncand 8067 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
|
Theorem | pncan2d 8068 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵) |
|
Theorem | pncan3d 8069 |
Subtraction and addition of equals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
|
Theorem | npcand 8070 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
|
Theorem | nncand 8071 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵) |
|
Theorem | negsubd 8072 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
|
Theorem | subnegd 8073 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − -𝐵) = (𝐴 + 𝐵)) |
|
Theorem | subeq0d 8074 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | subne0d 8075 |
Two unequal numbers have nonzero difference. See also subap0d 8399 which
is the same thing for apartness rather than negated equality.
(Contributed by Mario Carneiro, 1-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) |
|
Theorem | subeq0ad 8076 |
The difference of two complex numbers is zero iff they are equal.
Deduction form of subeq0 7981. Generalization of subeq0d 8074.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
|
Theorem | subne0ad 8077 |
If the difference of two complex numbers is nonzero, they are unequal.
Converse of subne0d 8075. Contrapositive of subeq0bd 8134. (Contributed
by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | neg11d 8078 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → -𝐴 = -𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | negdid 8079 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) |
|
Theorem | negdi2d 8080 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) |
|
Theorem | negsubdid 8081 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) |
|
Theorem | negsubdi2d 8082 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) |
|
Theorem | neg2subd 8083 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) |
|
Theorem | subaddd 8084 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) |
|
Theorem | subadd2d 8085 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) |
|
Theorem | addsubassd 8086 |
Associative-type law for subtraction and addition. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) |
|
Theorem | addsubd 8087 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) |
|
Theorem | subadd23d 8088 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | addsub12d 8089 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) |
|
Theorem | npncand 8090 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) |
|
Theorem | nppcand 8091 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) |
|
Theorem | nppcan2d 8092 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | nppcan3d 8093 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | subsubd 8094 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) |
|
Theorem | subsub2d 8095 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | subsub3d 8096 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) |
|
Theorem | subsub4d 8097 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) |
|
Theorem | sub32d 8098 |
Swap the second and third terms in a double subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) |
|
Theorem | nnncand 8099 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | nnncan1d 8100 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵)) |