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	mulcan2 11901	Cancellation law for multiplication. (Contributed by NM, 21-Jan-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulcani 11902	Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 26-Jan-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)
Theorem	mul0or 11903	If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
Theorem	mulne0b 11904	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 11905	The product of two nonzero numbers is nonzero. (Contributed by NM, 30-Dec-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ≠ 0)
Theorem	mulne0i 11906	The product of two nonzero numbers is nonzero. (Contributed by NM, 15-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐴 · 𝐵) ≠ 0
Theorem	muleqadd 11907	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 11908*	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 11909	Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.)
⊢ ( · ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0})
Theorem	msq0i 11910	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 11911	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 11912	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 11913	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 11914	The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0))
Theorem	mulne0d 11915	The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)
Theorem	mulcan1g 11916	A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 · 𝐶) ↔ (𝐴 = 0 ∨ 𝐵 = 𝐶)))
Theorem	mulcan2g 11917	A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐶 = 0)))
Theorem	mulne0bad 11918	A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11915 and consequence of mulne0bd 11914. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	mulne0bbd 11919	A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11915 and consequence of mulne0bd 11914. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0)    ⇒   ⊢ (𝜑 → 𝐵 ≠ 0)
5.3.6  Division
Syntax	cdiv 11920	Extend class notation to include division.
class /
Definition	df-div 11921*	Define division. Theorem divmuli 12021 relates it to multiplication, and divcli 12009 and redivcli 12034 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divval 11924 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
Theorem	1div0 11922	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 11923	Obsolete version of 1div0 11922 as of 5-Jun-2025. (Contributed by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (1 / 0) = ∅
Theorem	divval 11924*	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 11925	Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	divmul2 11926	Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmul3 11927	Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divcl 11928	Closure law for division. (Contributed by NM, 21-Jul-2001.) (Proof shortened by Mario Carneiro, 17-Feb-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
Theorem	reccl 11929	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ)
Theorem	divcan2 11930	A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divcan1 11931	A cancellation law for division. (Contributed by NM, 5-Jun-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	diveq0 11932	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 11933	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 11934	The ratio of nonzero numbers is nonzero. (Contributed by NM, 28-Dec-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ≠ 0)
Theorem	recne0 11935	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 11936	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 11937	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 11938	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 11939	Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divass 11940	An associative law for division. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div23 11941	A commutative/associative law for division. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	div32 11942	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13 11943	A commutative/associative law for division. (Contributed by NM, 22-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	div12 11944	A commutative/associative law for division. (Contributed by NM, 30-Apr-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	divmulass 11945	An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷)))
Theorem	divmulasscom 11946	An associative/commutative law for division and multiplication. (Contributed by AV, 10-Jul-2021.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷)))
Theorem	divdir 11947	Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divcan3 11948	A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcan4 11949	A cancellation law for division. (Contributed by NM, 8-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	div11 11950	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 11951	Obsolete version of div11 11950 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 11952	Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	divid 11953	A number divided by itself is one. (Contributed by NM, 1-Aug-2004.) (Proof shortened by SN, 9-Jul-2025.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1)
Theorem	dividOLD 11954	Obsolete version of divid 11953 as of 9-Jul-2025. (Contributed by NM, 1-Aug-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1)
Theorem	div0 11955	Division into zero is zero. (Contributed by NM, 14-Mar-2005.) (Proof shortened by SN, 9-Jul-2025.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0 / 𝐴) = 0)
Theorem	div0OLD 11956	Obsolete version of div0 11955 as of 9-Jul-2025. (Contributed by NM, 14-Mar-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0 / 𝐴) = 0)
Theorem	div1 11957	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
Theorem	1div1e1 11958	1 divided by 1 is 1. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ (1 / 1) = 1
Theorem	divneg 11959	Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	muldivdir 11960	Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) + 𝐵) / 𝐶) = (𝐴 + (𝐵 / 𝐶)))
Theorem	divsubdir 11961	Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	subdivcomb1 11962	Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) − 𝐵) / 𝐶) = (𝐴 − (𝐵 / 𝐶)))
Theorem	subdivcomb2 11963	Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − (𝐶 · 𝐵)) / 𝐶) = ((𝐴 / 𝐶) − 𝐵))
Theorem	recrec 11964	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 11965	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	rec11r 11966	Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) = 𝐵 ↔ (1 / 𝐵) = 𝐴))
Theorem	divmuldiv 11967	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 · 𝐵) / (𝐶 · 𝐷)))
Theorem	divdivdiv 11968	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.)
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
Theorem	divcan5 11969	Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divmul13 11970	Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐵 / 𝐶) · (𝐴 / 𝐷)))
Theorem	divmul24 11971	Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 / 𝐷) · (𝐵 / 𝐶)))
Theorem	divmuleq 11972	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) = (𝐵 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐵 · 𝐶)))
Theorem	recdiv 11973	The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	divcan6 11974	Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	divdiv32 11975	Swap denominators in a division. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcan7 11976	Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcan 11977	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 11978	Division into a fraction. (Contributed by NM, 31-Dec-2007.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdiv2 11979	Division by a fraction. (Contributed by NM, 27-Dec-2008.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	recdiv2 11980	Division into a reciprocal. (Contributed by NM, 19-Oct-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	ddcan 11981	Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	divadddiv 11982	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 11983	Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) − (𝐵 / 𝐷)) = (((𝐴 · 𝐷) − (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	conjmul 11984	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 11985	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℝ)
Theorem	redivcl 11986	Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	eqneg 11987	A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegd 11988	A complex number equals its negative iff it is zero. Deduction form of eqneg 11987. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegad 11989	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 11987. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = -𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	div2neg 11990	Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divneg2 11991	Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	recclzi 11992	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℂ)
Theorem	recne0zi 11993	The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ≠ 0)
Theorem	recidzi 11994	Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	div1i 11995	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 / 1) = 𝐴
Theorem	eqnegi 11996	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0)
Theorem	reccli 11997	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (1 / 𝐴) ∈ ℂ
Theorem	recidi 11998	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (𝐴 · (1 / 𝐴)) = 1
Theorem	recreci 11999	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 12000	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (𝐴 / 𝐴) = 1