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	subsub3d 11601	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵))
Theorem	subsub4d 11602	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
Theorem	sub32d 11603	Swap the second and third terms in a double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵))
Theorem	nnncand 11604	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵))
Theorem	nnncan1d 11605	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵))
Theorem	nnncan2d 11606	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵))
Theorem	npncan3d 11607	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵))
Theorem	pnpcand 11608	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶))
Theorem	pnpcan2d 11609	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵))
Theorem	pnncand 11610	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶))
Theorem	ppncand 11611	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶))
Theorem	subcand 11612	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐴 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	subcan2d 11613	Cancellation law for subtraction. (Contributed by Mario Carneiro, 22-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	subcanad 11614	Cancellation law for subtraction. Deduction form of subcan 11515. Generalization of subcand 11612. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶))
Theorem	subneintrd 11615	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcand 11612. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≠ (𝐴 − 𝐶))
Theorem	subcan2ad 11616	Cancellation law for subtraction. Deduction form of subcan2 11485. Generalization of subcan2d 11613. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subneintr2d 11617	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 11613. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶))
Theorem	addsub4d 11618	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)))
Theorem	subadd4d 11619	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶)))
Theorem	sub4d 11620	Rearrangement of 4 terms in a subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷)))
Theorem	2addsubd 11621	Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵))
Theorem	addsubeq4d 11622	Relation between sums and differences. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷)))
Theorem	subeqxfrd 11623	Transfer two terms of a subtraction in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐷))
Theorem	mvlraddd 11624	Move the right term in a sum on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = (𝐶 − 𝐵))
Theorem	mvlladdd 11625	Move the left term in a sum on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 − 𝐴))
Theorem	mvrraddd 11626	Move the right term in a sum on the RHS to the LHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵)
Theorem	mvrladdd 11627	Move the left term in a sum on the RHS to the LHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶)
Theorem	assraddsubd 11628	Associate RHS addition-subtraction. (Contributed by David A. Wheeler, 15-Oct-2018.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = ((𝐵 + 𝐶) − 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 = (𝐵 + (𝐶 − 𝐷)))
Theorem	subaddeqd 11629	Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐷) = (𝐶 − 𝐵))
Theorem	addlsub 11630	Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 − 𝐵)))
Theorem	addrsub 11631	Right-subtraction: Subtraction of the right summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 − 𝐴)))
Theorem	subexsub 11632	A subtraction law: Exchanging the subtrahend and the result of the subtraction. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = (𝐶 − 𝐵) ↔ 𝐵 = (𝐶 − 𝐴)))
Theorem	addid0 11633	If adding a number to a another number yields the other number, the added number must be 0. This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑋 + 𝑌) = 𝑋 ↔ 𝑌 = 0))
Theorem	addn0nid 11634	Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0) → (𝑋 + 𝑌) ≠ 𝑋)
Theorem	pnpncand 11635	Addition/subtraction cancellation law. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐵 − 𝐶)) + (𝐶 − 𝐵)) = 𝐴)
Theorem	subeqrev 11636	Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) = (𝐶 − 𝐷) ↔ (𝐵 − 𝐴) = (𝐷 − 𝐶)))
Theorem	addeq0 11637	Two complex numbers add up to zero iff they are each other's opposites. (Contributed by Thierry Arnoux, 2-May-2017.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) = 0 ↔ 𝐴 = -𝐵))
Theorem	pncan1 11638	Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1) − 1) = 𝐴)
Theorem	npcan1 11639	Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.)
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴)
Theorem	subeq0bd 11640	If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 11581. Converse of subeq0d 11579. Contrapositive of subne0ad 11582. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = 0)
Theorem	renegcld 11641	Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℝ)
Theorem	resubcld 11642	Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)
Theorem	negn0 11643*	The image under negation of a nonempty set of reals is nonempty. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅)
Theorem	negf1o 11644*	Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℝ → 𝐹:𝐴–1-1-onto→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴})
5.3.3  Multiplication
Theorem	kcnktkm1cn 11645	k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈ ℂ)
Theorem	muladd 11646	Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	subdi 11647	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
Theorem	subdir 11648	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
Theorem	ine0 11649	The imaginary unit i is not zero. (Contributed by NM, 6-May-1999.)
⊢ i ≠ 0
Theorem	mulneg1 11650	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))
Theorem	mulneg2 11651	The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · -𝐵) = -(𝐴 · 𝐵))
Theorem	mulneg12 11652	Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = (𝐴 · -𝐵))
Theorem	mul2neg 11653	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 30-Jul-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
Theorem	submul2 11654	Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 · 𝐶)) = (𝐴 + (𝐵 · -𝐶)))
Theorem	mulm1 11655	Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
Theorem	addneg1mul 11656	Addition with product with minus one is a subtraction. (Contributed by AV, 18-Oct-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (-1 · 𝐵)) = (𝐴 − 𝐵))
Theorem	mulsub 11657	Product of two differences. (Contributed by NM, 14-Jan-2006.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	mulsub2 11658	Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = ((𝐵 − 𝐴) · (𝐷 − 𝐶)))
Theorem	mulm1i 11659	Product with minus one is negative. (Contributed by NM, 31-Jul-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (-1 · 𝐴) = -𝐴
Theorem	mulneg1i 11660	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 10-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (-𝐴 · 𝐵) = -(𝐴 · 𝐵)
Theorem	mulneg2i 11661	Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · -𝐵) = -(𝐴 · 𝐵)
Theorem	mul2negi 11662	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (-𝐴 · -𝐵) = (𝐴 · 𝐵)
Theorem	subdii 11663	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))
Theorem	subdiri 11664	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))
Theorem	muladdi 11665	Product of two sums. (Contributed by NM, 17-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))
Theorem	mulm1d 11666	Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-1 · 𝐴) = -𝐴)
Theorem	mulneg1d 11667	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))
Theorem	mulneg2d 11668	Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · -𝐵) = -(𝐴 · 𝐵))
Theorem	mul2negd 11669	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
Theorem	subdid 11670	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
Theorem	subdird 11671	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
Theorem	muladdd 11672	Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	mulsubd 11673	Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	muls1d 11674	Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 − 1)) = ((𝐴 · 𝐵) − 𝐴))
Theorem	mulsubfacd 11675	Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − 𝐵) = ((𝐴 − 1) · 𝐵))
Theorem	addmulsub 11676	The product of a sum and a difference. (Contributed by AV, 5-Mar-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐵 · 𝐶)) − ((𝐴 · 𝐷) + (𝐵 · 𝐷))))
Theorem	subaddmulsub 11677	The difference with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ 𝐸 ∈ ℂ) → (𝐸 − ((𝐴 + 𝐵) · (𝐶 − 𝐷))) = (((𝐸 − (𝐴 · 𝐶)) − (𝐵 · 𝐶)) + ((𝐴 · 𝐷) + (𝐵 · 𝐷))))
Theorem	mulsubaddmulsub 11678	A special difference of a product with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐵 · 𝐶) − ((𝐴 + 𝐵) · (𝐶 − 𝐷))) = (((𝐴 · 𝐷) + (𝐵 · 𝐷)) − (𝐴 · 𝐶)))
5.3.4  Ordering on reals (cont.)
Theorem	gt0ne0 11679	Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
Theorem	lt0ne0 11680	A number which is less than zero is not zero. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0)
Theorem	ltadd1 11681	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)))
Theorem	leadd1 11682	Addition to both sides of 'less than or equal to'. (Contributed by NM, 18-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
Theorem	leadd2 11683	Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)))
Theorem	ltsubadd 11684	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵)))
Theorem	ltsubadd2 11685	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	lesubadd 11686	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵)))
Theorem	lesubadd2 11687	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶)))
Theorem	ltaddsub 11688	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵)))
Theorem	ltaddsub2 11689	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴)))
Theorem	leaddsub 11690	'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵)))
Theorem	leaddsub2 11691	'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴)))
Theorem	suble 11692	Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵))
Theorem	lesub 11693	Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴)))
Theorem	ltsub23 11694	'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵))
Theorem	ltsub13 11695	'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴)))
Theorem	le2add 11696	Adding both sides of two 'less than or equal to' relations. (Contributed by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)))
Theorem	ltleadd 11697	Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	leltadd 11698	Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	lt2add 11699	Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷)))
Theorem	addgt0 11700	The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵))