Theorem List for Intuitionistic Logic Explorer - 8101-8200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | addcani 8101 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶) |
|
Theorem | addcan2i 8102 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 14-May-2003.) (Revised by Scott Fenton,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵) |
|
Theorem | addcand 8103 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addcan2d 8104 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcanad 8105 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 8103. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) |
|
Theorem | addcan2ad 8106 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 8104. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | addneintrd 8107 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 8105. Consequence of addcand 8103.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶)) |
|
Theorem | addneintr2d 8108 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 8106. Consequence of
addcan2d 8104. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶)) |
|
Theorem | 0cnALT 8109 |
Alternate proof of 0cn 7912. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 0 ∈ ℂ |
|
Theorem | negeu 8110* |
Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) |
|
Theorem | subval 8111* |
Value of subtraction, which is the (unique) element 𝑥 such that
𝐵 +
𝑥 = 𝐴. (Contributed by NM, 4-Aug-2007.)
(Revised by Mario
Carneiro, 2-Nov-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)) |
|
Theorem | negeq 8112 |
Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|
⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
|
Theorem | negeqi 8113 |
Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝐴 = -𝐵 |
|
Theorem | negeqd 8114 |
Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐴 = -𝐵) |
|
Theorem | nfnegd 8115 |
Deduction version of nfneg 8116. (Contributed by NM, 29-Feb-2008.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝐴) |
|
Theorem | nfneg 8116 |
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 8117 |
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 | subcl 8118 |
Closure law for subtraction. (Contributed by NM, 10-May-1999.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) |
|
Theorem | negcl 8119 |
Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|
⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) |
|
Theorem | negicn 8120 |
-i is a complex number (common case). (Contributed by
David A.
Wheeler, 7-Dec-2018.)
|
⊢ -i ∈ ℂ |
|
Theorem | subf 8121 |
Subtraction is an operation on the complex numbers. (Contributed by NM,
4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
⊢ − :(ℂ ×
ℂ)⟶ℂ |
|
Theorem | subadd 8122 |
Relationship between subtraction and addition. (Contributed by NM,
20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) |
|
Theorem | subadd2 8123 |
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) |
|
Theorem | subsub23 8124 |
Swap subtrahend and result of subtraction. (Contributed by NM,
14-Dec-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) |
|
Theorem | pncan 8125 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
|
Theorem | pncan2 8126 |
Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵) |
|
Theorem | pncan3 8127 |
Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
|
Theorem | npcan 8128 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
|
Theorem | addsubass 8129 |
Associative-type law for addition and subtraction. (Contributed by NM,
6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) |
|
Theorem | addsub 8130 |
Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) |
|
Theorem | subadd23 8131 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 1-Feb-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | addsub12 8132 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 8-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) |
|
Theorem | 2addsub 8133 |
Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) |
|
Theorem | addsubeq4 8134 |
Relation between sums and differences. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷))) |
|
Theorem | pncan3oi 8135 |
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 8196 and pncan 8125, 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 8231. (Contributed by
David A. Wheeler, 11-Oct-2018.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴 |
|
Theorem | mvrraddi 8136 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐴 = (𝐵 + 𝐶) ⇒ ⊢ (𝐴 − 𝐶) = 𝐵 |
|
Theorem | mvlladdi 8137 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ 𝐵 = (𝐶 − 𝐴) |
|
Theorem | subid 8138 |
Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) |
|
Theorem | subid1 8139 |
Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
|
Theorem | npncan 8140 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) |
|
Theorem | nppcan 8141 |
Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) |
|
Theorem | nnpcan 8142 |
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 8143 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | subcan2 8144 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | subeq0 8145 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16-Nov-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
|
Theorem | npncan2 8146 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
21-Jun-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0) |
|
Theorem | subsub2 8147 |
Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | nncan 8148 |
Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵) |
|
Theorem | subsub 8149 |
Law for double subtraction. (Contributed by NM, 13-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) |
|
Theorem | nppcan2 8150 |
Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | subsub3 8151 |
Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) |
|
Theorem | subsub4 8152 |
Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) |
|
Theorem | sub32 8153 |
Swap the second and third terms in a double subtraction. (Contributed by
NM, 19-Aug-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) |
|
Theorem | nnncan 8154 |
Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | nnncan1 8155 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵)) |
|
Theorem | nnncan2 8156 |
Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵)) |
|
Theorem | npncan3 8157 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵)) |
|
Theorem | pnpcan 8158 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶)) |
|
Theorem | pnpcan2 8159 |
Cancellation law for mixed addition and subtraction. (Contributed by
Scott Fenton, 9-Jun-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) |
|
Theorem | pnncan 8160 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)) |
|
Theorem | ppncan 8161 |
Cancellation law for mixed addition and subtraction. (Contributed by NM,
30-Jun-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | addsub4 8162 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 4-Mar-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))) |
|
Theorem | subadd4 8163 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 24-Aug-2006.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶))) |
|
Theorem | sub4 8164 |
Rearrangement of 4 terms in a subtraction. (Contributed by NM,
23-Nov-2007.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) |
|
Theorem | neg0 8165 |
Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
|
⊢ -0 = 0 |
|
Theorem | negid 8166 |
Addition of a number and its negative. (Contributed by NM,
14-Mar-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0) |
|
Theorem | negsub 8167 |
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 8168 |
Relationship between subtraction and negative. (Contributed by NM,
10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵)) |
|
Theorem | negneg 8169 |
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 8170 |
Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by
Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | negcon1 8171 |
Negative contraposition law. (Contributed by NM, 9-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)) |
|
Theorem | negcon2 8172 |
Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)) |
|
Theorem | negeq0 8173 |
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 8174 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | negsubdi 8175 |
Distribution of negative over subtraction. (Contributed by NM,
15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵)) |
|
Theorem | negdi 8176 |
Distribution of negative over addition. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) |
|
Theorem | negdi2 8177 |
Distribution of negative over addition. (Contributed by NM,
1-Jan-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵)) |
|
Theorem | negsubdi2 8178 |
Distribution of negative over subtraction. (Contributed by NM,
4-Oct-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴)) |
|
Theorem | neg2sub 8179 |
Relationship between subtraction and negative. (Contributed by Paul
Chapman, 8-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴)) |
|
Theorem | renegcl 8180 |
Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.)
|
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) |
|
Theorem | renegcli 8181 |
Closure law for negative of reals. (Note: this inference proof style
and the deduction theorem usage in renegcl 8180 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 8182 |
Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℝ |
|
Theorem | resubcl 8183 |
Closure law for subtraction of reals. (Contributed by NM,
20-Jan-1997.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) |
|
Theorem | negreb 8184 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
(Revised by Mario Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)) |
|
Theorem | peano2cnm 8185 |
"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 8186 |
"Reverse" second Peano postulate analog for reals. (Contributed by
NM,
6-Feb-2007.)
|
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
|
Theorem | negcli 8187 |
Closure law for negative. (Contributed by NM, 26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ -𝐴 ∈ ℂ |
|
Theorem | negidi 8188 |
Addition of a number and its negative. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + -𝐴) = 0 |
|
Theorem | negnegi 8189 |
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 8190 |
Subtraction of a number from itself. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 − 𝐴) = 0 |
|
Theorem | subid1i 8191 |
Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 − 0) = 𝐴 |
|
Theorem | negne0bi 8192 |
A number is nonzero iff its negative is nonzero. (Contributed by NM,
10-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0) |
|
Theorem | negrebi 8193 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ) |
|
Theorem | negne0i 8194 |
The negative of a nonzero number is nonzero. (Contributed by NM,
30-Jul-2004.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠
0 ⇒ ⊢ -𝐴 ≠ 0 |
|
Theorem | subcli 8195 |
Closure law for subtraction. (Contributed by NM, 26-Nov-1994.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 − 𝐵) ∈ ℂ |
|
Theorem | pncan3i 8196 |
Subtraction and addition of equals. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵 |
|
Theorem | negsubi 8197 |
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 8198 |
Relationship between subtraction and negative. (Contributed by NM,
1-Dec-2005.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵) |
|
Theorem | subeq0i 8199 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵) |
|
Theorem | neg11i 8200 |
Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵) |