Theorem List for Intuitionistic Logic Explorer - 7901-8000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | peano2re 7901 |
A theorem for reals analogous the second Peano postulate peano2 4509.
(Contributed by NM, 5-Jul-2005.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
|
Theorem | addcom 7902 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | addid1 7903 |
0 is an additive identity. (Contributed by Jim
Kingdon,
16-Jan-2020.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2 7904 |
0 is a left identity for addition. (Contributed by
Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
|
Theorem | readdcan 7905 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | 00id 7906 |
0 is its own additive identity. (Contributed by Scott
Fenton,
3-Jan-2013.)
|
⊢ (0 + 0) = 0 |
|
Theorem | addid1i 7907 |
0 is an additive identity. (Contributed by NM,
23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + 0) = 𝐴 |
|
Theorem | addid2i 7908 |
0 is a left identity for addition. (Contributed by NM,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 + 𝐴) = 𝐴 |
|
Theorem | addcomi 7909 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) |
|
Theorem | addcomli 7910 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 |
|
Theorem | mul12i 7911 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew
Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)) |
|
Theorem | mul32i 7912 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵) |
|
Theorem | mul4i 7913 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)) |
|
Theorem | addid1d 7914 |
0 is an additive identity. (Contributed by Mario
Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2d 7915 |
0 is a left identity for addition. (Contributed by
Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐴) |
|
Theorem | addcomd 7916 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | mul12d 7917 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32d 7918 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31d 7919 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4d 7920 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
Theorem | muladd11r 7921 |
A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) |
|
Theorem | comraddd 7922 |
Commute RHS addition, in deduction form. (Contributed by David A.
Wheeler, 11-Oct-2018.)
|
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐵)) |
|
4.3 Real and complex numbers - basic
operations
|
|
4.3.1 Addition
|
|
Theorem | add12 7923 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32 7924 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add32r 7925 |
Commutative/associative law that swaps the last two terms in a triple sum,
rearranging the parentheses. (Contributed by Paul Chapman,
18-May-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add4 7926 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42 7927 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
Theorem | add12i 7928 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)) |
|
Theorem | add32i 7929 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵) |
|
Theorem | add4i 7930 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)) |
|
Theorem | add42i 7931 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)) |
|
Theorem | add12d 7932 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32d 7933 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add4d 7934 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42d 7935 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
4.3.2 Subtraction
|
|
Syntax | cmin 7936 |
Extend class notation to include subtraction.
|
class − |
|
Syntax | cneg 7937 |
Extend class notation to include unary minus. The symbol - is not a
class by itself but part of a compound class definition. We do this
rather than making it a formal function since it is so commonly used.
Note: We use different symbols for unary minus (-) and subtraction
cmin 7936 (−) to prevent
syntax ambiguity. For example, looking at the
syntax definition co 5774, if we used the same symbol
then "( − 𝐴 − 𝐵) " could mean either
"− 𝐴 " minus "𝐵",
or
it could represent the (meaningless) operation of
classes "− " and "− 𝐵
" connected with "operation" "𝐴".
On the other hand, "(-𝐴 − 𝐵) " is unambiguous.
|
class -𝐴 |
|
Definition | df-sub 7938* |
Define subtraction. Theorem subval 7957 shows its value (and describes how
this definition works), theorem subaddi 8052 relates it to addition, and
theorems subcli 8041 and resubcli 8028 prove its closure laws. (Contributed
by NM, 26-Nov-1994.)
|
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
|
Definition | df-neg 7939 |
Define the negative of a number (unary minus). We use different symbols
for unary minus (-) and subtraction (−) to prevent syntax
ambiguity. See cneg 7937 for a discussion of this. (Contributed by
NM,
10-Feb-1995.)
|
⊢ -𝐴 = (0 − 𝐴) |
|
Theorem | cnegexlem1 7940 |
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 7943. (Contributed by Eric Schmidt, 22-May-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | cnegexlem2 7941 |
Existence of a real number which produces a real number when multiplied
by i. (Hint: zero is such a number, although we
don't need to
prove that yet). Lemma for cnegex 7943. (Contributed by Eric Schmidt,
22-May-2007.)
|
⊢ ∃𝑦 ∈ ℝ (i · 𝑦) ∈
ℝ |
|
Theorem | cnegexlem3 7942* |
Existence of real number difference. Lemma for cnegex 7943. (Contributed
by Eric Schmidt, 22-May-2007.)
|
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑐 ∈ ℝ (𝑏 + 𝑐) = 𝑦) |
|
Theorem | cnegex 7943* |
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21-May-2007.)
|
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) |
|
Theorem | cnegex2 7944* |
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝑥 + 𝐴) = 0) |
|
Theorem | addcan 7945 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addcan2 7946 |
Cancellation law for addition. (Contributed by NM, 30-Jul-2004.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcani 7947 |
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 7948 |
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 7949 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addcan2d 7950 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcanad 7951 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 7949. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) |
|
Theorem | addcan2ad 7952 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 7950. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | addneintrd 7953 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 7951. Consequence of addcand 7949.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶)) |
|
Theorem | addneintr2d 7954 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 7952. Consequence of
addcan2d 7950. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶)) |
|
Theorem | 0cnALT 7955 |
Alternate proof of 0cn 7761. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 0 ∈ ℂ |
|
Theorem | negeu 7956* |
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 7957* |
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 7958 |
Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
|
⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
|
Theorem | negeqi 7959 |
Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝐴 = -𝐵 |
|
Theorem | negeqd 7960 |
Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐴 = -𝐵) |
|
Theorem | nfnegd 7961 |
Deduction version of nfneg 7962. (Contributed by NM, 29-Feb-2008.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝐴) |
|
Theorem | nfneg 7962 |
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 7963 |
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 7964 |
Closure law for subtraction. (Contributed by NM, 10-May-1999.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) |
|
Theorem | negcl 7965 |
Closure law for negative. (Contributed by NM, 6-Aug-2003.)
|
⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) |
|
Theorem | negicn 7966 |
-i is a complex number (common case). (Contributed by
David A.
Wheeler, 7-Dec-2018.)
|
⊢ -i ∈ ℂ |
|
Theorem | subf 7967 |
Subtraction is an operation on the complex numbers. (Contributed by NM,
4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
⊢ − :(ℂ ×
ℂ)⟶ℂ |
|
Theorem | subadd 7968 |
Relationship between subtraction and addition. (Contributed by NM,
20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) |
|
Theorem | subadd2 7969 |
Relationship between subtraction and addition. (Contributed by Scott
Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) |
|
Theorem | subsub23 7970 |
Swap subtrahend and result of subtraction. (Contributed by NM,
14-Dec-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) |
|
Theorem | pncan 7971 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) |
|
Theorem | pncan2 7972 |
Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵) |
|
Theorem | pncan3 7973 |
Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
|
Theorem | npcan 7974 |
Cancellation law for subtraction. (Contributed by NM, 10-May-2004.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) |
|
Theorem | addsubass 7975 |
Associative-type law for addition and subtraction. (Contributed by NM,
6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) |
|
Theorem | addsub 7976 |
Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) |
|
Theorem | subadd23 7977 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 1-Feb-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | addsub12 7978 |
Commutative/associative law for addition and subtraction. (Contributed by
NM, 8-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) |
|
Theorem | 2addsub 7979 |
Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) |
|
Theorem | addsubeq4 7980 |
Relation between sums and differences. (Contributed by Jeff Madsen,
17-Jun-2010.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷))) |
|
Theorem | pncan3oi 7981 |
Subtraction and addition of equals. Almost but not exactly the same as
pncan3i 8042 and pncan 7971, 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 8077. (Contributed by
David A. Wheeler, 11-Oct-2018.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴 |
|
Theorem | mvrraddi 7982 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐴 = (𝐵 + 𝐶) ⇒ ⊢ (𝐴 − 𝐶) = 𝐵 |
|
Theorem | mvlladdi 7983 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ 𝐵 = (𝐶 − 𝐴) |
|
Theorem | subid 7984 |
Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.)
(Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) |
|
Theorem | subid1 7985 |
Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
|
Theorem | npncan 7986 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) |
|
Theorem | nppcan 7987 |
Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) |
|
Theorem | nnpcan 7988 |
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 7989 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | subcan2 7990 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | subeq0 7991 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 16-Nov-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
|
Theorem | npncan2 7992 |
Cancellation law for subtraction. (Contributed by Scott Fenton,
21-Jun-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0) |
|
Theorem | subsub2 7993 |
Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | nncan 7994 |
Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵) |
|
Theorem | subsub 7995 |
Law for double subtraction. (Contributed by NM, 13-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) |
|
Theorem | nppcan2 7996 |
Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | subsub3 7997 |
Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) |
|
Theorem | subsub4 7998 |
Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) |
|
Theorem | sub32 7999 |
Swap the second and third terms in a double subtraction. (Contributed by
NM, 19-Aug-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) |
|
Theorem | nnncan 8000 |
Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) |