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