P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subsubd 8101	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶))
Theorem	subsub2d 8102	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵)))
Theorem	subsub3d 8103	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵))
Theorem	subsub4d 8104	Law for double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶)))
Theorem	sub32d 8105	Swap the second and third terms in a double subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵))
Theorem	nnncand 8106	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵))
Theorem	nnncan1d 8107	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵))
Theorem	nnncan2d 8108	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵))
Theorem	npncan3d 8109	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵))
Theorem	pnpcand 8110	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶))
Theorem	pnpcan2d 8111	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵))
Theorem	pnncand 8112	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶))
Theorem	ppncand 8113	Cancellation law for mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶))
Theorem	subcand 8114	Cancellation law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐴 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = 𝐶)
Theorem	subcan2d 8115	Cancellation law for subtraction. (Contributed by Mario Carneiro, 22-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	subcanad 8116	Cancellation law for subtraction. Deduction form of subcan 8017. Generalization of subcand 8114. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶))
Theorem	subneintrd 8117	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcand 8114. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ≠ (𝐴 − 𝐶))
Theorem	subcan2ad 8118	Cancellation law for subtraction. Deduction form of subcan2 7987. Generalization of subcan2d 8115. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵))
Theorem	subneintr2d 8119	Introducing subtraction on both sides of a statement of inequality. Contrapositive of subcan2d 8115. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶))
Theorem	addsub4d 8120	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷)))
Theorem	subadd4d 8121	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶)))
Theorem	sub4d 8122	Rearrangement of 4 terms in a subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷)))
Theorem	2addsubd 8123	Law for subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵))
Theorem	addsubeq4d 8124	Relation between sums and differences. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷)))
Theorem	subeqxfrd 8125	Transfer two terms of a subtraction in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐷))
Theorem	mvlraddd 8126	Move LHS right addition to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 = (𝐶 − 𝐵))
Theorem	mvlladdd 8127	Move LHS left addition to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 − 𝐴))
Theorem	mvrraddd 8128	Move RHS right addition to LHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵)
Theorem	mvrladdd 8129	Move RHS left addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶)
Theorem	assraddsubd 8130	Associate RHS addition-subtraction. (Contributed by David A. Wheeler, 15-Oct-2018.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = ((𝐵 + 𝐶) − 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 = (𝐵 + (𝐶 − 𝐷)))
Theorem	subaddeqd 8131	Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐷) = (𝐶 − 𝐵))
Theorem	addlsub 8132	Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 − 𝐵)))
Theorem	addrsub 8133	Right-subtraction: Subtraction of the right summand from the result of an addition. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 − 𝐴)))
Theorem	subexsub 8134	A subtraction law: Exchanging the subtrahend and the result of the subtraction. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = (𝐶 − 𝐵) ↔ 𝐵 = (𝐶 − 𝐴)))
Theorem	addid0 8135	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 8136	Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0) → (𝑋 + 𝑌) ≠ 𝑋)
Theorem	pnpncand 8137	Addition/subtraction cancellation law. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐵 − 𝐶)) + (𝐶 − 𝐵)) = 𝐴)
Theorem	subeqrev 8138	Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) = (𝐶 − 𝐷) ↔ (𝐵 − 𝐴) = (𝐷 − 𝐶)))
Theorem	pncan1 8139	Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1) − 1) = 𝐴)
Theorem	npcan1 8140	Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.)
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴)
Theorem	subeq0bd 8141	If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 8083. Converse of subeq0d 8081. Contrapositive of subne0ad 8084. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) = 0)
Theorem	renegcld 8142	Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℝ)
Theorem	resubcld 8143	Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)
Theorem	negf1o 8144*	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→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴})
4.3.3  Multiplication
Theorem	kcnktkm1cn 8145	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 8146	Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	subdi 8147	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
Theorem	subdir 8148	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
Theorem	mul02 8149	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
Theorem	mul02lem2 8150	Zero times a real is zero. Although we prove it as a corollary of mul02 8149, the name is for consistency with the Metamath Proof Explorer which proves it before mul02 8149. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0)
Theorem	mul01 8151	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
Theorem	mul02i 8152	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (0 · 𝐴) = 0
Theorem	mul01i 8153	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 0) = 0
Theorem	mul02d 8154	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (0 · 𝐴) = 0)
Theorem	mul01d 8155	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 0) = 0)
Theorem	ine0 8156	The imaginary unit i is not zero. (Contributed by NM, 6-May-1999.)
⊢ i ≠ 0
Theorem	mulneg1 8157	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 8158	The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · -𝐵) = -(𝐴 · 𝐵))
Theorem	mulneg12 8159	Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = (𝐴 · -𝐵))
Theorem	mul2neg 8160	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 8161	Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 · 𝐶)) = (𝐴 + (𝐵 · -𝐶)))
Theorem	mulm1 8162	Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
Theorem	mulsub 8163	Product of two differences. (Contributed by NM, 14-Jan-2006.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	mulsub2 8164	Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = ((𝐵 − 𝐴) · (𝐷 − 𝐶)))
Theorem	mulm1i 8165	Product with minus one is negative. (Contributed by NM, 31-Jul-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (-1 · 𝐴) = -𝐴
Theorem	mulneg1i 8166	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 8167	Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · -𝐵) = -(𝐴 · 𝐵)
Theorem	mul2negi 8168	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 8169	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))
Theorem	subdiri 8170	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))
Theorem	muladdi 8171	Product of two sums. (Contributed by NM, 17-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))
Theorem	mulm1d 8172	Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-1 · 𝐴) = -𝐴)
Theorem	mulneg1d 8173	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))
Theorem	mulneg2d 8174	Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · -𝐵) = -(𝐴 · 𝐵))
Theorem	mul2negd 8175	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
Theorem	subdid 8176	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)))
Theorem	subdird 8177	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)))
Theorem	muladdd 8178	Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	mulsubd 8179	Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵))))
Theorem	mulsubfacd 8180	Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − 𝐵) = ((𝐴 − 1) · 𝐵))
4.3.4  Ordering on reals (cont.)
Theorem	ltadd2 8181	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	ltadd2i 8182	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))
Theorem	ltadd2d 8183	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
Theorem	ltadd2dd 8184	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵))
Theorem	ltletrd 8185	Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	ltaddneg 8186	Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵))
Theorem	ltaddnegr 8187	Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐴 + 𝐵) < 𝐵))
Theorem	lelttrdi 8188	If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 < 𝐶))
Theorem	gt0ne0 8189	Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
Theorem	lt0ne0 8190	A number which is less than zero is not zero. See also lt0ap0 8410 which is similar but for apartness. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0)
Theorem	ltadd1 8191	Addition to both sides of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 12-Nov-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)))
Theorem	leadd1 8192	Addition to both sides of 'less than or equal to'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 18-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
Theorem	leadd2 8193	Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)))
Theorem	ltsubadd 8194	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵)))
Theorem	ltsubadd2 8195	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶)))
Theorem	lesubadd 8196	'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 8197	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶)))
Theorem	ltaddsub 8198	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵)))
Theorem	ltaddsub2 8199	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴)))
Theorem	leaddsub 8200	'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵)))