P. 117 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11601-11700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mvrraddi 11601	Move the right term in a sum on the RHS to the LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐴 = (𝐵 + 𝐶)    ⇒   ⊢ (𝐴 − 𝐶) = 𝐵
Theorem	mvrladdi 11602	Move the left term in a sum on the RHS to the LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐴 = (𝐵 + 𝐶)    ⇒   ⊢ (𝐴 − 𝐵) = 𝐶
Theorem	mvlladdi 11603	Move the left term in a sum on the LHS to the RHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ 𝐵 = (𝐶 − 𝐴)
Theorem	subid 11604	Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0)
Theorem	subid1 11605	Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
Theorem	npncan 11606	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶))
Theorem	nppcan 11607	Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶))
Theorem	nnpcan 11608	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 11609	Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶))
Theorem	subcan2 11610	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subeq0 11611	If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	npncan2 11612	Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐴)) = 0)
Theorem	subsub2 11613	Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵)))
Theorem	nncan 11614	Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − (𝐴 − 𝐵)) = 𝐵)
Theorem	subsub 11615	Law for double subtraction. (Contributed by NM, 13-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))
Theorem	nppcan2 11616	Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵))
Theorem	subsub3 11617	Law for double subtraction. (Contributed by NM, 27-Jul-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵))
Theorem	subsub4 11618	Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
Theorem	sub32 11619	Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵))
Theorem	nnncan 11620	Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵))
Theorem	nnncan1 11621	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵))
Theorem	nnncan2 11622	Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵))
Theorem	npncan3 11623	Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵))
Theorem	pnpcan 11624	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 11625	Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵))
Theorem	pnncan 11626	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶))
Theorem	ppncan 11627	Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶))
Theorem	addsub4 11628	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)))
Theorem	subadd4 11629	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶)))
Theorem	sub4 11630	Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷)))
Theorem	neg0 11631	Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.)
⊢ -0 = 0
Theorem	negid 11632	Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (𝐴 + -𝐴) = 0)
Theorem	negsub 11633	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 11634	Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − -𝐵) = (𝐴 + 𝐵))
Theorem	negneg 11635	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 11636	Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ( -𝐴 = -𝐵 ↔ 𝐴 = 𝐵))
Theorem	negcon1 11637	Negative contraposition law. (Contributed by NM, 9-May-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ( -𝐴 = 𝐵 ↔ -𝐵 = 𝐴))
Theorem	negcon2 11638	Negative contraposition law. (Contributed by NM, 14-Nov-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = -𝐵 ↔ 𝐵 = -𝐴))
Theorem	negeq0 11639	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 11640	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶))
Theorem	negsubdi 11641	Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = ( -𝐴 + 𝐵))
Theorem	negdi 11642	Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = ( -𝐴 + -𝐵))
Theorem	negdi2 11643	Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = ( -𝐴 − 𝐵))
Theorem	negsubdi2 11644	Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 − 𝐵) = (𝐵 − 𝐴))
Theorem	neg2sub 11645	Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ( -𝐴 − -𝐵) = (𝐵 − 𝐴))
Theorem	renegcli 11646	Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11648 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 11647	Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 − 𝐵) ∈ ℝ
Theorem	renegcl 11648	Closure law for negative of reals. The weak deduction theorem dedth 4544 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11646, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
Theorem	resubcl 11649	Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
Theorem	negreb 11650	The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℂ → ( -𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ))
Theorem	peano2cnm 11651	"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 11652	"Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.)
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
Theorem	negcli 11653	Closure law for negative. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ -𝐴 ∈ ℂ
Theorem	negidi 11654	Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 + -𝐴) = 0
Theorem	negnegi 11655	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 11656	Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 − 𝐴) = 0
Theorem	subid1i 11657	Identity law for subtraction. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 − 0) = 𝐴
Theorem	negne0bi 11658	A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 ↔ -𝐴 ≠ 0)
Theorem	negrebi 11659	The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ( -𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ)
Theorem	negne0i 11660	The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ -𝐴 ≠ 0
Theorem	subcli 11661	Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 − 𝐵) ∈ ℂ
Theorem	pncan3i 11662	Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + (𝐵 − 𝐴)) = 𝐵
Theorem	negsubi 11663	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 11664	Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 − -𝐵) = (𝐴 + 𝐵)
Theorem	subeq0i 11665	If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)
Theorem	neg11i 11666	Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ( -𝐴 = -𝐵 ↔ 𝐴 = 𝐵)
Theorem	negcon1i 11667	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ( -𝐴 = 𝐵 ↔ -𝐵 = 𝐴)
Theorem	negcon2i 11668	Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐵 ↔ 𝐵 = -𝐴)
Theorem	negdii 11669	Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by OpenAI, 25-Mar-2011.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ -(𝐴 + 𝐵) = ( -𝐴 + -𝐵)
Theorem	negsubdii 11670	Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ -(𝐴 − 𝐵) = ( -𝐴 + 𝐵)
Theorem	negsubdi2i 11671	Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ -(𝐴 − 𝐵) = (𝐵 − 𝐴)
Theorem	subaddi 11672	Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)
Theorem	subadd2i 11673	Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)
Theorem	subaddrii 11674	Relationship between subtraction and addition. (Contributed by NM, 16-Dec-2006.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ (𝐵 + 𝐶) = 𝐴    ⇒   ⊢ (𝐴 − 𝐵) = 𝐶
Theorem	subsub23i 11675	Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)
Theorem	addsubassi 11676	Associative-type law for subtraction and addition. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))
Theorem	addsubi 11677	Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)
Theorem	subcani 11678	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)
Theorem	subcan2i 11679	Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)
Theorem	pnncani 11680	Cancellation law for mixed addition and subtraction. (Contributed by NM, 14-Jan-2006.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)
Theorem	addsub4i 11681	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 17-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))
Theorem	0reALT 11682	Alternate proof of 0re 11337. (Contributed by NM, 19-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℝ
Theorem	negcld 11683	Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℂ)
Theorem	subidd 11684	Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
Theorem	subid1d 11685	Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − 0) = 𝐴)
Theorem	negidd 11686	Addition of a number and its negative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + -𝐴) = 0)
Theorem	negnegd 11687	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 11688	A number is zero iff its negative is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = 0 ↔ -𝐴 = 0))
Theorem	negne0bd 11689	A number is nonzero iff its negative is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ -𝐴 ≠ 0))
Theorem	negcon1d 11690	Contraposition law for unary minus. Deduction form of negcon1 11637. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ( -𝐴 = 𝐵 ↔ -𝐵 = 𝐴))
Theorem	negcon1ad 11691	Contraposition law for unary minus. One-way deduction form of negcon1 11637. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → -𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → -𝐵 = 𝐴)
Theorem	neg11ad 11692	The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 11636. Generalization of neg11d 11708. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ( -𝐴 = -𝐵 ↔ 𝐴 = 𝐵))
Theorem	negned 11693	If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 11708. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → -𝐴 ≠ -𝐵)
Theorem	negne0d 11694	The negative of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → -𝐴 ≠ 0)
Theorem	negrebd 11695	The negative of a real is real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → -𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	subcld 11696	Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)
Theorem	pncand 11697	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐵) = 𝐴)
Theorem	pncan2d 11698	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − 𝐴) = 𝐵)
Theorem	pncan3d 11699	Subtraction and addition of equals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
Theorem	npcand 11700	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) + 𝐵) = 𝐴)