P. 78 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7701-7800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divcanap2zi 7701	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapzi 7702	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divcanap3zi 7703	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4zi 7704	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	rec11api 7705	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 # 0 ∧ 𝐵 # 0) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divclapi 7706	Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℂ
Theorem	divcanap2i 7707	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐵 · (𝐴 / 𝐵)) = 𝐴
Theorem	divcanap1i 7708	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · 𝐵) = 𝐴
Theorem	divrecapi 7709	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))
Theorem	divcanap3i 7710	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐵 · 𝐴) / 𝐵) = 𝐴
Theorem	divcanap4i 7711	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐵) = 𝐴
Theorem	divap0i 7712	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) # 0
Theorem	rec11apii 7713	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)
Theorem	divassapzi 7714	An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	divmulapzi 7715	Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	divdirapzi 7716	Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divdiv23apzi 7717	Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐵 # 0 ∧ 𝐶 # 0) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divmulapi 7718	Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)
Theorem	divdiv32api 7719	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)
Theorem	divassapi 7720	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))
Theorem	divdirapi 7721	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))
Theorem	div23api 7722	A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)
Theorem	div11api 7723	One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)
Theorem	divmuldivapi 7724	Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷))
Theorem	divmul13api 7725	Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷))
Theorem	divadddivapi 7726	Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷))
Theorem	divdivdivapi 7727	Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))
Theorem	rerecclapzi 7728	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) ∈ ℝ)
Theorem	rerecclapi 7729	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (1 / 𝐴) ∈ ℝ
Theorem	redivclapzi 7730	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	redivclapi 7731	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℝ
Theorem	div1d 7732	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 / 1) = 𝐴)
Theorem	recclapd 7733	Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ)
Theorem	recap0d 7734	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) # 0)
Theorem	recidapd 7735	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recidap2d 7736	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) · 𝐴) = 1)
Theorem	recrecapd 7737	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / (1 / 𝐴)) = 𝐴)
Theorem	dividapd 7738	A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
Theorem	div0apd 7739	Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (0 / 𝐴) = 0)
Theorem	apmul1 7740	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 # 𝐵 ↔ (𝐴 · 𝐶) # (𝐵 · 𝐶)))
Theorem	divclapd 7741	Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcanap1d 7742	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcanap2d 7743	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapd 7744	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrecap2d 7745	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divcanap3d 7746	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4d 7747	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	diveqap0d 7748	If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	diveqap1d 7749	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	diveqap1ad 7750	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7658. Generalization of diveqap1d 7749. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	diveqap0ad 7751	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7637. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divap1d 7752	If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐴 # 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) # 1)
Theorem	divap0bd 7753	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0))
Theorem	divnegapd 7754	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	divneg2apd 7755	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	div2negapd 7756	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divap0d 7757	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) # 0)
Theorem	recdivapd 7758	The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	recdivap2d 7759	Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	divcanap6d 7760	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	ddcanapd 7761	Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	rec11apd 7762	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmulapd 7763	Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	div32apd 7764	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13apd 7765	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	divdiv32apd 7766	Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcanap5d 7767	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divcanap5rd 7768	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵))
Theorem	divcanap7d 7769	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcanapd 7770	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶))
Theorem	dmdcanap2d 7771	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶))
Theorem	divdivap1d 7772	Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdivap2d 7773	Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	divmulap2d 7774	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmulap3d 7775	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divassapd 7776	An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div12apd 7777	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	div23apd 7778	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	divdirapd 7779	Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divsubdirapd 7780	Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	div11apd 7781	One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmuldivapd 7782	Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐷 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷)))
Theorem	rerecclapd 7783	Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	redivclapd 7784	Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	mvllmulapd 7785	Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 / 𝐴))
3.3.9  Ordering on reals (cont.)
Theorem	ltp1 7786	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	lep1 7787	A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1))
Theorem	ltm1 7788	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
Theorem	lem1 7789	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≤ 𝐴)
Theorem	letrp1 7790	A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ (𝐵 + 1))
Theorem	p1le 7791	A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + 1) ≤ 𝐵) → 𝐴 ≤ 𝐵)
Theorem	recgt0 7792	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 25-Aug-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (1 / 𝐴))
Theorem	prodgt0gt0 7793	Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7794 for the same theorem with 0 < 𝐴 replaced by the weaker condition 0 ≤ 𝐴. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵)
Theorem	prodgt0 7794	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵)
Theorem	prodgt02 7795	Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐵 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴)
Theorem	prodge0 7796	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ (𝐴 · 𝐵))) → 0 ≤ 𝐵)
Theorem	prodge02 7797	Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐵 ∧ 0 ≤ (𝐴 · 𝐵))) → 0 ≤ 𝐴)
Theorem	ltmul2 7798	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵)))
Theorem	lemul2 7799	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	lemul1a 7800	Multiplication of both sides of 'less than or equal to' by a nonnegative number. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 21-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))