P. 85 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8401-8500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulgt0d 8401	The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → 0 < (𝐴 · 𝐵))
Theorem	letrd 8402	Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	lelttrd 8403	Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	lttrd 8404	Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	0lt1 8405	0 is less than 1. Theorem I.21 of [Apostol] p. 20. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 17-Jan-1997.)
⊢ 0 < 1
Theorem	ltntri 8406	Negative trichotomy property for real numbers. It is well known that we cannot prove real number trichotomy, 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴. Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no, as shown here. This is another example of distinguishing between being unable to prove something, or being able to refute it. (Contributed by Jim Kingdon, 13-Aug-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴))
4.2.5  Initial properties of the complex numbers
Theorem	mul12 8407	Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Theorem	mul32 8408	Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
Theorem	mul31 8409	Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴))
Theorem	mul4 8410	Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
Theorem	muladd11 8411	A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 𝐴) · (1 + 𝐵)) = ((1 + 𝐴) + (𝐵 + (𝐴 · 𝐵))))
Theorem	1p1times 8412	Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
Theorem	peano2cn 8413	A theorem for complex numbers analogous the second Peano postulate peano2 4719. (Contributed by NM, 17-Aug-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ)
Theorem	peano2re 8414	A theorem for reals analogous the second Peano postulate peano2 4719. (Contributed by NM, 5-Jul-2005.)
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Theorem	addcom 8415	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	addrid 8416	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	addlid 8417	0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
Theorem	readdcan 8418	Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵))
Theorem	00id 8419	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (0 + 0) = 0
Theorem	addridi 8420	0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 + 0) = 𝐴
Theorem	addlidi 8421	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (0 + 𝐴) = 𝐴
Theorem	addcomi 8422	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)
Theorem	addcomli 8423	Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	mul12i 8424	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 8425	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)
Theorem	mul4i 8426	Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))
Theorem	addridd 8427	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 0) = 𝐴)
Theorem	addlidd 8428	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (0 + 𝐴) = 𝐴)
Theorem	addcomd 8429	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	mul12d 8430	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
Theorem	mul32d 8431	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵))
Theorem	mul31d 8432	Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴))
Theorem	mul4d 8433	Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)))
Theorem	muladd11r 8434	A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1))
Theorem	comraddd 8435	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 8436	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)))
Theorem	add32 8437	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵))
Theorem	add32r 8438	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 8439	Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)))
Theorem	add42 8440	Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)))
Theorem	add12i 8441	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))
Theorem	add32i 8442	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)
Theorem	add4i 8443	Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))
Theorem	add42i 8444	Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))
Theorem	add12d 8445	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)))
Theorem	add32d 8446	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵))
Theorem	add4d 8447	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)))
Theorem	add42d 8448	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)))
4.3.2  Subtraction
Syntax	cmin 8449	Extend class notation to include subtraction.
class −
Syntax	cneg 8450	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 8449 (−) to prevent syntax ambiguity. For example, looking at the syntax definition co 6052, 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 8451*	Define subtraction. Theorem subval 8470 shows its value (and describes how this definition works), Theorem subaddi 8565 relates it to addition, and Theorems subcli 8554 and resubcli 8541 prove its closure laws. (Contributed by NM, 26-Nov-1994.)
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
Definition	df-neg 8452	Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 8450 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
⊢ -𝐴 = (0 − 𝐴)
Theorem	cnegexlem1 8453	Addition cancellation of a real number from two complex numbers. Lemma for cnegex 8456. (Contributed by Eric Schmidt, 22-May-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	cnegexlem2 8454	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 8456. (Contributed by Eric Schmidt, 22-May-2007.)
⊢ ∃𝑦 ∈ ℝ (i · 𝑦) ∈ ℝ
Theorem	cnegexlem3 8455*	Existence of real number difference. Lemma for cnegex 8456. (Contributed by Eric Schmidt, 22-May-2007.)
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑐 ∈ ℝ (𝑏 + 𝑐) = 𝑦)
Theorem	cnegex 8456*	Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0)
Theorem	cnegex2 8457*	Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝑥 + 𝐴) = 0)
Theorem	addcan 8458	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 8459	Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	addcani 8460	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 8461	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 8462	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
Theorem	addcan2d 8463	Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
Theorem	addcanad 8464	Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8462. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	addcan2ad 8465	Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8463. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	addneintrd 8466	Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8464. Consequence of addcand 8462. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶))
Theorem	addneintr2d 8467	Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8465. Consequence of addcan2d 8463. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶))
Theorem	0cnALT 8468	Alternate proof of 0cn 8271. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	negeu 8469*	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 8470*	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 8471	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
Theorem	negeqi 8472	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ -𝐴 = -𝐵
Theorem	negeqd 8473	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -𝐴 = -𝐵)
Theorem	nfnegd 8474	Deduction version of nfneg 8475. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥-𝐴)
Theorem	nfneg 8475	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 8476	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 8477	Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	negcl 8478	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
Theorem	negicn 8479	-i is a complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ -i ∈ ℂ
Theorem	subf 8480	Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	subadd 8481	Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	subadd2 8482	Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴))
Theorem	subsub23 8483	Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵))
Theorem	pncan 8484	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Theorem	pncan2 8485	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵)
Theorem	pncan3 8486	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
Theorem	npcan 8487	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)
Theorem	addsubass 8488	Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)))
Theorem	addsub 8489	Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))
Theorem	subadd23 8490	Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵)))
Theorem	addsub12 8491	Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶)))
Theorem	2addsub 8492	Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵))
Theorem	addsubeq4 8493	Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷)))
Theorem	pncan3oi 8494	Subtraction and addition of equals. Almost but not exactly the same as pncan3i 8555 and pncan 8484, 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 8590. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴
Theorem	mvrraddi 8495	Move RHS right addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐴 = (𝐵 + 𝐶)    ⇒   ⊢ (𝐴 − 𝐶) = 𝐵
Theorem	mvlladdi 8496	Move LHS left addition to RHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ 𝐵 = (𝐶 − 𝐴)
Theorem	subid 8497	Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0)
Theorem	subid1 8498	Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
Theorem	npncan 8499	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶))
Theorem	nppcan 8500	Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶))