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	recrecd 11901	A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / (1 / 𝐴)) = 𝐴)
Theorem	dividd 11902	A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
Theorem	div0d 11903	Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (0 / 𝐴) = 0)
Theorem	divcld 11904	Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcan1d 11905	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcan2d 11906	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecd 11907	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrec2d 11908	Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divcan3d 11909	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcan4d 11910	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	diveq0d 11911	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	diveq1d 11912	Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	diveq1ad 11913	The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 11813. Generalization of diveq1d 11912. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	diveq0ad 11914	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 11793. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divne1d 11915	If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 11912. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 1)
Theorem	divne0bd 11916	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0))
Theorem	divnegd 11917	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	divneg2d 11918	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	div2negd 11919	Quotient of two negatives. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divne0d 11920	The ratio of nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 0)
Theorem	recdivd 11921	The reciprocal of a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	recdiv2d 11922	Division into a reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	divcan6d 11923	Cancellation of inverted fractions. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	ddcand 11924	Cancellation in a double division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	rec11d 11925	Reciprocal is one-to-one. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmuld 11926	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	div32d 11927	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13d 11928	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	divdiv32d 11929	Swap denominators in a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcan5d 11930	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divcan5rd 11931	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵))
Theorem	divcan7d 11932	Cancel equal divisors in a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcand 11933	Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶))
Theorem	dmdcan2d 11934	Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶))
Theorem	divdiv1d 11935	Division into a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdiv2d 11936	Division by a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	divmul2d 11937	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmul3d 11938	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divassd 11939	An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div12d 11940	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	div23d 11941	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	divdird 11942	Distribution of division over addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divsubdird 11943	Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	div11d 11944	One-to-one relationship for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    &   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmuldivd 11945	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷)))
Theorem	divmul13d 11946	Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷)))
Theorem	divmul24d 11947	Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 / 𝐷) · (𝐶 / 𝐵)))
Theorem	divadddivd 11948	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷)))
Theorem	divsubdivd 11949	Subtraction of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) − (𝐶 / 𝐷)) = (((𝐴 · 𝐷) − (𝐶 · 𝐵)) / (𝐵 · 𝐷)))
Theorem	divmuleqd 11950	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐶 · 𝐵)))
Theorem	divdivdivd 11951	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐷 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
Theorem	diveq1bd 11952	If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 11813. Converse of diveq1d 11912. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)
Theorem	div2sub 11953	Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷)) → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶)))
Theorem	div2subd 11954	Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 11953. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶)))
Theorem	rereccld 11955	Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	redivcld 11956	Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	subrecd 11957	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵)))
Theorem	subrec 11958	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵)))
Theorem	subreci 11959	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵))
Theorem	mvllmuld 11960	Move the left term in a product on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 / 𝐴))
Theorem	mvllmuli 11961	Move the left term in a product on the LHS to the RHS, inference form. Uses divcan4i 11875. (Contributed by David A. Wheeler, 11-Oct-2018.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ 𝐵 = (𝐶 / 𝐴)
Theorem	ldiv 11962	Left-division. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 / 𝐵)))
Theorem	rdiv 11963	Right-division. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 / 𝐴)))
Theorem	mdiv 11964	A division law. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 = (𝐶 / 𝐵) ↔ 𝐵 = (𝐶 / 𝐴)))
Theorem	lineq 11965	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (((𝐴 · 𝑋) + 𝐵) = 𝑌 ↔ 𝑋 = ((𝑌 − 𝐵) / 𝐴)))
5.3.7  Ordering on reals (cont.)
Theorem	elimgt0 11966	Hypothesis for weak deduction theorem to eliminate 0 < 𝐴. (Contributed by NM, 15-May-1999.)
⊢ 0 < if(0 < 𝐴, 𝐴, 1)
Theorem	elimge0 11967	Hypothesis for weak deduction theorem to eliminate 0 ≤ 𝐴. (Contributed by NM, 30-Jul-1999.)
⊢ 0 ≤ if(0 ≤ 𝐴, 𝐴, 0)
Theorem	ltp1 11968	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
Theorem	lep1 11969	A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1))
Theorem	ltm1 11970	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴)
Theorem	lem1 11971	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≤ 𝐴)
Theorem	letrp1 11972	A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ (𝐵 + 1))
Theorem	p1le 11973	A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + 1) ≤ 𝐵) → 𝐴 ≤ 𝐵)
Theorem	recgt0 11974	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	prodgt0 11975	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 11976	Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐵 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴)
Theorem	ltmul1a 11977	Lemma for ltmul1 11978. Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 15-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) ∧ 𝐴 < 𝐵) → (𝐴 · 𝐶) < (𝐵 · 𝐶))
Theorem	ltmul1 11978	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)))
Theorem	ltmul2 11979	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	lemul1 11980	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))
Theorem	lemul2 11981	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	lemul1a 11982	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))
Theorem	lemul2a 11983	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
Theorem	ltmul12a 11984	Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.)
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (𝐴 · 𝐶) < (𝐵 · 𝐷))
Theorem	lemul12b 11985	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)))
Theorem	lemul12a 11986	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ ((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷)))
Theorem	mulgt1OLD 11987	Obsolete version of mulgt1 11990 as of 29-Jun-2025. (Contributed by NM, 13-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵))
Theorem	ltmulgt11 11988	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐴 · 𝐵)))
Theorem	ltmulgt12 11989	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐵 · 𝐴)))
Theorem	mulgt1 11990	The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) (Proof shortened by SN, 29-Jun-2025.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵))
Theorem	lemulge11 11991	Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐴 · 𝐵))
Theorem	lemulge12 11992	Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐵 · 𝐴))
Theorem	ltdiv1 11993	Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	lediv1 11994	Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶)))
Theorem	gt0div 11995	Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵)))
Theorem	ge0div 11996	Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
Theorem	divgt0 11997	The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 / 𝐵))
Theorem	divge0 11998	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))
Theorem	mulge0b 11999	A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 · 𝐵) ↔ ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))))
Theorem	mulle0b 12000	A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) ≤ 0 ↔ ((𝐴 ≤ 0 ∧ 0 ≤ 𝐵) ∨ (0 ≤ 𝐴 ∧ 𝐵 ≤ 0))))