P. 91 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mul0eqap 9001	If two numbers are apart from each other and their product is zero, one of them must be zero. (Contributed by Jim Kingdon, 31-Jul-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐴 = 0 ∨ 𝐵 = 0))
Theorem	recapb 9002*	A complex number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies), generalized from real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.)
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))
4.3.8  Division
Syntax	cdiv 9003	Extend class notation to include division.
class /
Definition	df-div 9004*	Define division. Theorem divmulap 9006 relates it to multiplication, and divclap 9009 and redivclap 9062 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divvalap 9005 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
Theorem	divvalap 9005*	Value of division: the (unique) element 𝑥 such that (𝐵 · 𝑥) = 𝐴. This is meaningful only when 𝐵 is apart from zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
Theorem	divmulap 9006	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	divmulap2 9007	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmulap3 9008	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divclap 9009	Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) ∈ ℂ)
Theorem	recclap 9010	Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) ∈ ℂ)
Theorem	divcanap2 9011	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divcanap1 9012	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	diveqap0 9013	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divap0b 9014	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0))
Theorem	divap0 9015	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 / 𝐵) # 0)
Theorem	recap0 9016	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) # 0)
Theorem	recidap 9017	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recidap2 9018	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((1 / 𝐴) · 𝐴) = 1)
Theorem	divrecap 9019	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrecap2 9020	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divassap 9021	An associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div23ap 9022	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	div32ap 9023	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13ap 9024	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	div12ap 9025	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	divmulassap 9026	An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷)))
Theorem	divmulasscomap 9027	An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷)))
Theorem	divdirap 9028	Distribution of division over addition. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divcanap3 9029	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4 9030	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	div11ap 9031	One-to-one relationship for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵))
Theorem	dividap 9032	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 / 𝐴) = 1)
Theorem	div0ap 9033	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (0 / 𝐴) = 0)
Theorem	div1 9034	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
Theorem	1div1e1 9035	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ (1 / 1) = 1
Theorem	diveqap1 9036	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	divnegap 9037	Move negative sign inside of a division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	muldivdirap 9038	Distribution of division over addition with a multiplication. (Contributed by Jim Kingdon, 11-Nov-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (((𝐶 · 𝐴) + 𝐵) / 𝐶) = (𝐴 + (𝐵 / 𝐶)))
Theorem	divsubdirap 9039	Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	recrecap 9040	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / (1 / 𝐴)) = 𝐴)
Theorem	rec11ap 9041	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	rec11rap 9042	Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) = 𝐵 ↔ (1 / 𝐵) = 𝐴))
Theorem	divmuldivap 9043	Multiplication of two ratios. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 · 𝐵) / (𝐶 · 𝐷)))
Theorem	divdivdivap 9044	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
Theorem	divcanap5 9045	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divmul13ap 9046	Swap the denominators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐵 / 𝐶) · (𝐴 / 𝐷)))
Theorem	divmul24ap 9047	Swap the numerators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 / 𝐷) · (𝐵 / 𝐶)))
Theorem	divmuleqap 9048	Cross-multiply in an equality of ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) = (𝐵 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐵 · 𝐶)))
Theorem	recdivap 9049	The reciprocal of a ratio. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	divcanap6 9050	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	divdiv32ap 9051	Swap denominators in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcanap7 9052	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcanap 9053	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · (𝐶 / 𝐴)) = (𝐶 / 𝐵))
Theorem	divdivap1 9054	Division into a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdivap2 9055	Division by a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	recdivap2 9056	Division into a reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	ddcanap 9057	Cancellation in a double division. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	divadddivap 9058	Addition of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) + (𝐵 / 𝐷)) = (((𝐴 · 𝐷) + (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	divsubdivap 9059	Subtraction of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) − (𝐵 / 𝐷)) = (((𝐴 · 𝐷) − (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	conjmulap 9060	Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 # 0) ∧ (𝑄 ∈ ℂ ∧ 𝑄 # 0)) → (((1 / 𝑃) + (1 / 𝑄)) = 1 ↔ ((𝑃 − 1) · (𝑄 − 1)) = 1))
Theorem	rerecclap 9061	Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (1 / 𝐴) ∈ ℝ)
Theorem	redivclap 9062	Closure law for division of reals. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	eqneg 9063	A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegd 9064	A complex number equals its negative iff it is zero. Deduction form of eqneg 9063. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegad 9065	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 9063. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = -𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	div2negap 9066	Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divneg2ap 9067	Move negative sign inside of a division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	recclapzi 9068	Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) ∈ ℂ)
Theorem	recap0apzi 9069	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) # 0)
Theorem	recidapzi 9070	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	div1i 9071	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 / 1) = 𝐴
Theorem	eqnegi 9072	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0)
Theorem	recclapi 9073	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (1 / 𝐴) ∈ ℂ
Theorem	recidapi 9074	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (𝐴 · (1 / 𝐴)) = 1
Theorem	recrecapi 9075	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	dividapi 9076	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (𝐴 / 𝐴) = 1
Theorem	div0api 9077	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (0 / 𝐴) = 0
Theorem	divclapzi 9078	Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcanap1zi 9079	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcanap2zi 9080	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapzi 9081	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divcanap3zi 9082	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4zi 9083	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	rec11api 9084	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 # 0 ∧ 𝐵 # 0) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divclapi 9085	Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℂ
Theorem	divcanap2i 9086	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐵 · (𝐴 / 𝐵)) = 𝐴
Theorem	divcanap1i 9087	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · 𝐵) = 𝐴
Theorem	divrecapi 9088	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))
Theorem	divcanap3i 9089	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐵 · 𝐴) / 𝐵) = 𝐴
Theorem	divcanap4i 9090	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐵) = 𝐴
Theorem	divap0i 9091	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) # 0
Theorem	rec11apii 9092	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)
Theorem	divassapzi 9093	An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	divmulapzi 9094	Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	divdirapzi 9095	Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divdiv23apzi 9096	Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐵 # 0 ∧ 𝐶 # 0) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divmulapi 9097	Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)
Theorem	divdiv32api 9098	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)
Theorem	divassapi 9099	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))
Theorem	divdirapi 9100	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))