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	mvlladdi 11401	Move the left term in a sum on the LHS to the RHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ 𝐵 = (𝐶 − 𝐴)
Theorem	subid 11402	Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0)
Theorem	subid1 11403	Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
Theorem	npncan 11404	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶))
Theorem	nppcan 11405	Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶))
Theorem	nnpcan 11406	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 11407	Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶))
Theorem	subcan2 11408	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subeq0 11409	If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	npncan2 11410	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0)
Theorem	subsub2 11411	Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵)))
Theorem	nncan 11412	Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵)
Theorem	subsub 11413	Law for double subtraction. (Contributed by NM, 13-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))
Theorem	nppcan2 11414	Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵))
Theorem	subsub3 11415	Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵))
Theorem	subsub4 11416	Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
Theorem	sub32 11417	Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵))
Theorem	nnncan 11418	Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵))
Theorem	nnncan1 11419	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵))
Theorem	nnncan2 11420	Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵))
Theorem	npncan3 11421	Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵))
Theorem	pnpcan 11422	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 11423	Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵))
Theorem	pnncan 11424	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶))
Theorem	ppncan 11425	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶))
Theorem	addsub4 11426	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)))
Theorem	subadd4 11427	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶)))
Theorem	sub4 11428	Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷)))
Theorem	neg0 11429	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
⊢ -0 = 0
Theorem	negid 11430	Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0)
Theorem	negsub 11431	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 11432	Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵))
Theorem	negneg 11433	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 11434	Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵))
Theorem	negcon1 11435	Negative contraposition law. (Contributed by NM, 9-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴))
Theorem	negcon2 11436	Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴))
Theorem	negeq0 11437	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 11438	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶))
Theorem	negsubdi 11439	Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (-𝐴 + 𝐵))
Theorem	negdi 11440	Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
Theorem	negdi2 11441	Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 − 𝐵))
Theorem	negsubdi2 11442	Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴))
Theorem	neg2sub 11443	Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 − -𝐵) = (𝐵 − 𝐴))
Theorem	renegcli 11444	Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11446 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 11445	Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 − 𝐵) ∈ ℝ
Theorem	renegcl 11446	Closure law for negative of reals. The weak deduction theorem dedth 4526 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11444, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
Theorem	resubcl 11447	Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
Theorem	negreb 11448	The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
Theorem	peano2cnm 11449	"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 11450	"Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.)
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
Theorem	negcli 11451	Closure law for negative. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ -𝐴 ∈ ℂ
Theorem	negidi 11452	Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 + -𝐴) = 0
Theorem	negnegi 11453	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 11454	Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 − 𝐴) = 0
Theorem	subid1i 11455	Identity law for subtraction. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 − 0) = 𝐴
Theorem	negne0bi 11456	A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)
Theorem	negrebi 11457	The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (-𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)
Theorem	negne0i 11458	The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ -𝐴 ≠ 0
Theorem	subcli 11459	Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 − 𝐵) ∈ ℂ
Theorem	pncan3i 11460	Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵
Theorem	negsubi 11461	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 11462	Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵)
Theorem	subeq0i 11463	If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)
Theorem	neg11i 11464	Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵)
Theorem	negcon1i 11465	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴)
Theorem	negcon2i 11466	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)
Theorem	negdii 11467	Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by OpenAI, 25-Mar-2011.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ -(𝐴 + 𝐵) = (-𝐴 + -𝐵)
Theorem	negsubdii 11468	Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ -(𝐴 − 𝐵) = (-𝐴 + 𝐵)
Theorem	negsubdi2i 11469	Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴)
Theorem	subaddi 11470	Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)
Theorem	subadd2i 11471	Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)
Theorem	subaddrii 11472	Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ (𝐵 + 𝐶) = 𝐴    ⇒   ⊢ (𝐴 − 𝐵) = 𝐶
Theorem	subsub23i 11473	Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)
Theorem	addsubassi 11474	Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))
Theorem	addsubi 11475	Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)
Theorem	subcani 11476	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)
Theorem	subcan2i 11477	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)
Theorem	pnncani 11478	Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)
Theorem	addsub4i 11479	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))
Theorem	0reALT 11480	Alternate proof of 0re 11135. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℝ
Theorem	negcld 11481	Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℂ)
Theorem	subidd 11482	Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
Theorem	subid1d 11483	Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − 0) = 𝐴)
Theorem	negidd 11484	Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + -𝐴) = 0)
Theorem	negnegd 11485	A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → --𝐴 = 𝐴)
Theorem	negeq0d 11486	A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = 0 ↔ -𝐴 = 0))
Theorem	negne0bd 11487	A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0))
Theorem	negcon1d 11488	Contraposition law for unary minus. Deduction form of negcon1 11435. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴 = 𝐵 ↔ -𝐵 = 𝐴))
Theorem	negcon1ad 11489	Contraposition law for unary minus. One-way deduction form of negcon1 11435. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → -𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -𝐵 = 𝐴)
Theorem	neg11ad 11490	The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 11434. Generalization of neg11d 11506. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴 = -𝐵 ↔ 𝐴 = 𝐵))
Theorem	negned 11491	If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 11506. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → -𝐴 ≠ -𝐵)
Theorem	negne0d 11492	The negative of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → -𝐴 ≠ 0)
Theorem	negrebd 11493	The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → -𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	subcld 11494	Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
Theorem	pncand 11495	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Theorem	pncan2d 11496	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵)
Theorem	pncan3d 11497	Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
Theorem	npcand 11498	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴)
Theorem	nncand 11499	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − (𝐴 − 𝐵)) = 𝐵)
Theorem	negsubd 11500	Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵))