P. 115 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11401-11500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	add12d 11401	Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)))
Theorem	add32d 11402	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵))
Theorem	add4d 11403	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)))
Theorem	add42d 11404	Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)))
5.3.2  Subtraction
Syntax	cmin 11405	Extend class notation to include subtraction.
class −
Syntax	cneg 11406	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 11405 (−) to prevent syntax ambiguity. For example, looking at the syntax definition co 7387, 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 11407*	Define subtraction. Theorem subval 11412 shows its value (and describes how this definition works), Theorem subaddi 11509 relates it to addition, and Theorems subcli 11498 and resubcli 11484 prove its closure laws. (Contributed by NM, 26-Nov-1994.)
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥))
Definition	df-neg 11408	Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 11406 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
⊢ -𝐴 = (0 − 𝐴)
Theorem	0cnALT 11409	Alternate proof of 0cn 11166 which does not reference ax-1cn 11126. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	0cnALT2 11410	Alternate proof of 0cnALT 11409 which is shorter, but depends on ax-8 2111, ax-13 2370, ax-sep 5251, ax-nul 5261, ax-pow 5320, ax-pr 5387, ax-un 7711, and every complex number axiom except ax-pre-mulgt0 11145 and ax-pre-sup 11146. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	negeu 11411*	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 11412*	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 11413	Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
Theorem	negeqi 11414	Equality inference for negatives. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ -𝐴 = -𝐵
Theorem	negeqd 11415	Equality deduction for negatives. (Contributed by NM, 14-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -𝐴 = -𝐵)
Theorem	nfnegd 11416	Deduction version of nfneg 11417. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥-𝐴)
Theorem	nfneg 11417	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 11418	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	negex 11419	A negative is a set. (Contributed by NM, 4-Apr-2005.)
⊢ -𝐴 ∈ V
Theorem	subcl 11420	Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
Theorem	negcl 11421	Closure law for negative. (Contributed by NM, 6-Aug-2003.)
⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)
Theorem	negicn 11422	-i is a complex number. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ -i ∈ ℂ
Theorem	subf 11423	Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
⊢ − :(ℂ × ℂ)⟶ℂ
Theorem	subadd 11424	Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴))
Theorem	subadd2 11425	Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴))
Theorem	subsub23 11426	Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵))
Theorem	pncan 11427	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Theorem	pncan2 11428	Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵)
Theorem	pncan3 11429	Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Steven Nguyen, 8-Jan-2023.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
Theorem	npcan 11430	Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴)
Theorem	addsubass 11431	Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶)))
Theorem	addsub 11432	Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵))
Theorem	subadd23 11433	Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵)))
Theorem	addsub12 11434	Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶)))
Theorem	2addsub 11435	Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵))
Theorem	addsubeq4 11436	Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷)))
Theorem	pncan3oi 11437	Subtraction and addition of equals. Almost but not exactly the same as pncan3i 11499 and pncan 11427, 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 11534. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴
Theorem	mvrraddi 11438	Move the right term in a sum on the RHS to the LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐴 = (𝐵 + 𝐶)    ⇒   ⊢ (𝐴 − 𝐶) = 𝐵
Theorem	mvrladdi 11439	Move the left term in a sum on the RHS to the LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐴 = (𝐵 + 𝐶)    ⇒   ⊢ (𝐴 − 𝐵) = 𝐶
Theorem	mvlladdi 11440	Move the left term in a sum on the LHS to the RHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ 𝐵 = (𝐶 − 𝐴)
Theorem	subid 11441	Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0)
Theorem	subid1 11442	Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
Theorem	npncan 11443	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶))
Theorem	nppcan 11444	Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶))
Theorem	nnpcan 11445	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 11446	Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶))
Theorem	subcan2 11447	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subeq0 11448	If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	npncan2 11449	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0)
Theorem	subsub2 11450	Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵)))
Theorem	nncan 11451	Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵)
Theorem	subsub 11452	Law for double subtraction. (Contributed by NM, 13-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))
Theorem	nppcan2 11453	Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵))
Theorem	subsub3 11454	Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵))
Theorem	subsub4 11455	Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
Theorem	sub32 11456	Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵))
Theorem	nnncan 11457	Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵))
Theorem	nnncan1 11458	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵))
Theorem	nnncan2 11459	Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵))
Theorem	npncan3 11460	Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵))
Theorem	pnpcan 11461	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 11462	Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵))
Theorem	pnncan 11463	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶))
Theorem	ppncan 11464	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶))
Theorem	addsub4 11465	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)))
Theorem	subadd4 11466	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶)))
Theorem	sub4 11467	Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷)))
Theorem	neg0 11468	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
⊢ -0 = 0
Theorem	negid 11469	Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0)
Theorem	negsub 11470	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 11471	Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵))
Theorem	negneg 11472	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 11473	Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵))
Theorem	negcon1 11474	Negative contraposition law. (Contributed by NM, 9-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴))
Theorem	negcon2 11475	Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴))
Theorem	negeq0 11476	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 11477	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶))
Theorem	negsubdi 11478	Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵))
Theorem	negdi 11479	Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
Theorem	negdi2 11480	Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵))
Theorem	negsubdi2 11481	Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴))
Theorem	neg2sub 11482	Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴))
Theorem	renegcli 11483	Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11485 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 11484	Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 − 𝐵) ∈ ℝ
Theorem	renegcl 11485	Closure law for negative of reals. The weak deduction theorem dedth 4547 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11483, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
Theorem	resubcl 11486	Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
Theorem	negreb 11487	The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
Theorem	peano2cnm 11488	"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 11489	"Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.)
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
Theorem	negcli 11490	Closure law for negative. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ -𝐴 ∈ ℂ
Theorem	negidi 11491	Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 + -𝐴) = 0
Theorem	negnegi 11492	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 11493	Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 − 𝐴) = 0
Theorem	subid1i 11494	Identity law for subtraction. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 − 0) = 𝐴
Theorem	negne0bi 11495	A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)
Theorem	negrebi 11496	The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)
Theorem	negne0i 11497	The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ -𝐴 ≠ 0
Theorem	subcli 11498	Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 − 𝐵) ∈ ℂ
Theorem	pncan3i 11499	Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵
Theorem	negsubi 11500	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.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + -𝐵) = (𝐴 − 𝐵)