P. 120 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulne0b 11901	The product of two nonzero numbers is nonzero. (Contributed by NM, 1-Aug-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0))
Theorem	mulne0 11902	The product of two nonzero numbers is nonzero. (Contributed by NM, 30-Dec-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ≠ 0)
Theorem	mulne0i 11903	The product of two nonzero numbers is nonzero. (Contributed by NM, 15-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐴 · 𝐵) ≠ 0
Theorem	muleqadd 11904	Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 13-Nov-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 + 𝐵) ↔ ((𝐴 − 1) · (𝐵 − 1)) = 1))
Theorem	receu 11905*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)
Theorem	mulnzcnf 11906	Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.)
⊢ ( · ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0})
Theorem	msq0i 11907	A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0)
Theorem	mul0ori 11908	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 7-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0))
Theorem	msq0d 11909	A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0))
Theorem	mul0ord 11910	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	mulne0bd 11911	The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0))
Theorem	mulne0d 11912	The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)
Theorem	mulcan1g 11913	A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 · 𝐶) ↔ (𝐴 = 0 ∨ 𝐵 = 𝐶)))
Theorem	mulcan2g 11914	A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐶 = 0)))
Theorem	mulne0bad 11915	A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11912 and consequence of mulne0bd 11911. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	mulne0bbd 11916	A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11912 and consequence of mulne0bd 11911. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 0)
5.3.6  Division
Syntax	cdiv 11917	Extend class notation to include division.
class /
Definition	df-div 11918*	Define division. Theorem divmuli 12018 relates it to multiplication, and divcli 12006 and redivcli 12031 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divval 11921 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
Theorem	1div0 11919	You can't divide by zero, because division explicitly excludes zero from the domain of the function. Thus, by the definition of function value, it evaluates to the empty set. (This theorem is for information only and normally is not referenced by other proofs. To be meaningful, it assumes that ∅ is not a complex number, which depends on the particular complex number construction that is used.) (Contributed by Mario Carneiro, 1-Apr-2014.) (Proof shortened by SN, 5-Jun-2025.) (New usage is discouraged.)
⊢ (1 / 0) = ∅
Theorem	1div0OLD 11920	Obsolete version of 1div0 11919 as of 5-Jun-2025. (Contributed by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (1 / 0) = ∅
Theorem	divval 11921*	Value of division: if 𝐴 and 𝐵 are complex numbers with 𝐵 nonzero, then (𝐴 / 𝐵) is the (unique) complex number such that (𝐵 · 𝑥) = 𝐴. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
Theorem	divmul 11922	Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	divmul2 11923	Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmul3 11924	Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divcl 11925	Closure law for division. (Contributed by NM, 21-Jul-2001.) (Proof shortened by Mario Carneiro, 17-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
Theorem	reccl 11926	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ)
Theorem	divcan2 11927	A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divcan1 11928	A cancellation law for division. (Contributed by NM, 5-Jun-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	diveq0 11929	A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divne0b 11930	The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0))
Theorem	divne0 11931	The ratio of nonzero numbers is nonzero. (Contributed by NM, 28-Dec-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ≠ 0)
Theorem	recne0 11932	The reciprocal of a nonzero number is nonzero. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ≠ 0)
Theorem	recid 11933	Multiplication of a number and its reciprocal. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recid2 11934	Multiplication of a number and its reciprocal. (Contributed by NM, 22-Jun-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 𝐴) · 𝐴) = 1)
Theorem	divrec 11935	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrec2 11936	Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divass 11937	An associative law for division. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div23 11938	A commutative/associative law for division. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	div32 11939	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13 11940	A commutative/associative law for division. (Contributed by NM, 22-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	div12 11941	A commutative/associative law for division. (Contributed by NM, 30-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	divmulass 11942	An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷)))
Theorem	divmulasscom 11943	An associative/commutative law for division and multiplication. (Contributed by AV, 10-Jul-2021.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷)))
Theorem	divdir 11944	Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divcan3 11945	A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcan4 11946	A cancellation law for division. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	div11 11947	One-to-one relationship for division. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) (Proof shortened by SN, 9-Jul-2025.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵))
Theorem	div11OLD 11948	Obsolete version of div11 11947 as of 9-Jul-2025. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵))
Theorem	diveq1 11949	Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	divid 11950	A number divided by itself is one. (Contributed by NM, 1-Aug-2004.) (Proof shortened by SN, 9-Jul-2025.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1)
Theorem	dividOLD 11951	Obsolete version of divid 11950 as of 9-Jul-2025. (Contributed by NM, 1-Aug-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1)
Theorem	div0 11952	Division into zero is zero. (Contributed by NM, 14-Mar-2005.) (Proof shortened by SN, 9-Jul-2025.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0 / 𝐴) = 0)
Theorem	div0OLD 11953	Obsolete version of div0 11952 as of 9-Jul-2025. (Contributed by NM, 14-Mar-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0 / 𝐴) = 0)
Theorem	div1 11954	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
Theorem	1div1e1 11955	1 divided by 1 is 1. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ (1 / 1) = 1
Theorem	divneg 11956	Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	muldivdir 11957	Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) + 𝐵) / 𝐶) = (𝐴 + (𝐵 / 𝐶)))
Theorem	divsubdir 11958	Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	subdivcomb1 11959	Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) − 𝐵) / 𝐶) = (𝐴 − (𝐵 / 𝐶)))
Theorem	subdivcomb2 11960	Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − (𝐶 · 𝐵)) / 𝐶) = ((𝐴 / 𝐶) − 𝐵))
Theorem	recrec 11961	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 26-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / (1 / 𝐴)) = 𝐴)
Theorem	rec11 11962	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	rec11r 11963	Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) = 𝐵 ↔ (1 / 𝐵) = 𝐴))
Theorem	divmuldiv 11964	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 · 𝐵) / (𝐶 · 𝐷)))
Theorem	divdivdiv 11965	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.)
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
Theorem	divcan5 11966	Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divmul13 11967	Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐵 / 𝐶) · (𝐴 / 𝐷)))
Theorem	divmul24 11968	Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 / 𝐷) · (𝐵 / 𝐶)))
Theorem	divmuleq 11969	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) = (𝐵 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐵 · 𝐶)))
Theorem	recdiv 11970	The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	divcan6 11971	Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	divdiv32 11972	Swap denominators in a division. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcan7 11973	Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcan 11974	Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Fan Zheng, 3-Jul-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · (𝐶 / 𝐴)) = (𝐶 / 𝐵))
Theorem	divdiv1 11975	Division into a fraction. (Contributed by NM, 31-Dec-2007.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdiv2 11976	Division by a fraction. (Contributed by NM, 27-Dec-2008.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	recdiv2 11977	Division into a reciprocal. (Contributed by NM, 19-Oct-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	ddcan 11978	Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	divadddiv 11979	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) + (𝐵 / 𝐷)) = (((𝐴 · 𝐷) + (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	divsubdiv 11980	Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) − (𝐵 / 𝐷)) = (((𝐴 · 𝐷) − (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	conjmul 11981	Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 12-Nov-2006.)
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 ≠ 0) ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → (((1 / 𝑃) + (1 / 𝑄)) = 1 ↔ ((𝑃 − 1) · (𝑄 − 1)) = 1))
Theorem	rereccl 11982	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℝ)
Theorem	redivcl 11983	Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	eqneg 11984	A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegd 11985	A complex number equals its negative iff it is zero. Deduction form of eqneg 11984. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegad 11986	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 11984. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = -𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	div2neg 11987	Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divneg2 11988	Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	recclzi 11989	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℂ)
Theorem	recne0zi 11990	The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ≠ 0)
Theorem	recidzi 11991	Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	div1i 11992	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 / 1) = 𝐴
Theorem	eqnegi 11993	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0)
Theorem	reccli 11994	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (1 / 𝐴) ∈ ℂ
Theorem	recidi 11995	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (𝐴 · (1 / 𝐴)) = 1
Theorem	recreci 11996	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (1 / (1 / 𝐴)) = 𝐴
Theorem	dividi 11997	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (𝐴 / 𝐴) = 1
Theorem	div0i 11998	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (0 / 𝐴) = 0
Theorem	divclzi 11999	Closure law for division. (Contributed by NM, 7-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcan1zi 12000	A cancellation law for division. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)