P. 87 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8601-8700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rpreap0 8601	A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 # 0))
Theorem	rpcnne0 8602	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
Theorem	rpcnap0 8603	A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 # 0))
Theorem	ralrp 8604	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑))
Theorem	rexrp 8605	Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑))
Theorem	rpaddcl 8606	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℝ+)
Theorem	rpmulcl 8607	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)
Theorem	rpdivcl 8608	Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
Theorem	rpreccl 8609	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+)
Theorem	rphalfcl 8610	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+)
Theorem	rpgecl 8611	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ+)
Theorem	rphalflt 8612	Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴)
Theorem	rerpdivcl 8613	Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	ge0p1rp 8614	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈ ℝ+)
Theorem	rpnegap 8615	Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (𝐴 ∈ ℝ+ ⊻ -𝐴 ∈ ℝ+))
Theorem	0nrp 8616	Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
⊢ ¬ 0 ∈ ℝ+
Theorem	ltsubrp 8617	Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 − 𝐵) < 𝐴)
Theorem	ltaddrp 8618	Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵))
Theorem	difrp 8619	Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℝ+))
Theorem	elrpd 8620	Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ+)
Theorem	nnrpd 8621	A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ+)
Theorem	rpred 8622	A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	rpxrd 8623	A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	rpcnd 8624	A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	rpgt0d 8625	A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	rpge0d 8626	A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 ≤ 𝐴)
Theorem	rpne0d 8627	A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	rpap0d 8628	A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
Theorem	rpregt0d 8629	A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	rprege0d 8630	A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	rprene0d 8631	A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0))
Theorem	rpcnne0d 8632	A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
Theorem	rpreccld 8633	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ+)
Theorem	rprecred 8634	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	rphalfcld 8635	Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ+)
Theorem	reclt1d 8636	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 1 ↔ 1 < (1 / 𝐴)))
Theorem	recgt1d 8637	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ (1 / 𝐴) < 1))
Theorem	rpaddcld 8638	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ+)
Theorem	rpmulcld 8639	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ+)
Theorem	rpdivcld 8640	Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)
Theorem	ltrecd 8641	The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)))
Theorem	lerecd 8642	The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴)))
Theorem	ltrec1d 8643	Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → (1 / 𝐴) < 𝐵)    ⇒   ⊢ (𝜑 → (1 / 𝐵) < 𝐴)
Theorem	lerec2d 8644	Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≤ (1 / 𝐵))    ⇒   ⊢ (𝜑 → 𝐵 ≤ (1 / 𝐴))
Theorem	lediv2ad 8645	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))
Theorem	ltdiv2d 8646	Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴)))
Theorem	lediv2d 8647	Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)))
Theorem	ledivdivd 8648	Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) ≤ (𝐶 / 𝐷))    ⇒   ⊢ (𝜑 → (𝐷 / 𝐶) ≤ (𝐵 / 𝐴))
Theorem	divge1 8649	The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 1 ≤ (𝐵 / 𝐴))
Theorem	divlt1lt 8650	A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < 𝐵))
Theorem	divle1le 8651	A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) ≤ 1 ↔ 𝐴 ≤ 𝐵))
Theorem	ledivge1le 8652	If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 / 𝐶) ≤ 𝐵))
Theorem	ge0p1rpd 8653	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 + 1) ∈ ℝ+)
Theorem	rerpdivcld 8654	Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	ltsubrpd 8655	Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) < 𝐴)
Theorem	ltaddrpd 8656	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵))
Theorem	ltaddrp2d 8657	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐴))
Theorem	ltmulgt11d 8658	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴)))
Theorem	ltmulgt12d 8659	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐴 · 𝐵)))
Theorem	gt0divd 8660	Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵)))
Theorem	ge0divd 8661	Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
Theorem	rpgecld 8662	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ+)
Theorem	divge0d 8663	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵))
Theorem	ltmul1d 8664	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)))
Theorem	ltmul2d 8665	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵)))
Theorem	lemul1d 8666	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))
Theorem	lemul2d 8667	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	ltdiv1d 8668	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	lediv1d 8669	Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶)))
Theorem	ltmuldivd 8670	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmuldiv2d 8671	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	lemuldivd 8672	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	lemuldiv2d 8673	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	ltdivmuld 8674	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵)))
Theorem	ltdivmul2d 8675	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶)))
Theorem	ledivmuld 8676	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵)))
Theorem	ledivmul2d 8677	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶)))
Theorem	ltmul1dd 8678	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶))
Theorem	ltmul2dd 8679	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · 𝐴) < (𝐶 · 𝐵))
Theorem	ltdiv1dd 8680	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶))
Theorem	lediv1dd 8681	Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))
Theorem	lediv12ad 8682	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))
Theorem	ltdiv23d 8683	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵)
Theorem	lediv23d 8684	Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵)
Theorem	lt2mul2divd 8685	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))
3.5.2  Infinity and the extended real number system (cont.)
Syntax	cxne 8686	Extend class notation to include the negative of an extended real.
class -𝑒𝐴
Syntax	cxad 8687	Extend class notation to include addition of extended reals.
class +𝑒
Syntax	cxmu 8688	Extend class notation to include multiplication of extended reals.
class ·e
Definition	df-xneg 8689	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
Definition	df-xadd 8690*	Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
Definition	df-xmul 8691*	Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦 ∧ 𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦 ∧ 𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥 ∧ 𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))
Theorem	pnfxr 8692	Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
⊢ +∞ ∈ ℝ*
Theorem	pnfex 8693	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ +∞ ∈ V
Theorem	mnfxr 8694	Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ -∞ ∈ ℝ*
Theorem	ltxr 8695	The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ)))))
Theorem	elxr 8696	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Theorem	pnfnemnf 8697	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 8698	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	xrnemnf 8699	An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))
Theorem	xrnepnf 8700	An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞))