P. 99 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9801-9900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ledivge1le 9801	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 9802	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 + 1) ∈ ℝ+)
Theorem	rerpdivcld 9803	Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	ltsubrpd 9804	Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) < 𝐴)
Theorem	ltaddrpd 9805	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵))
Theorem	ltaddrp2d 9806	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐴))
Theorem	ltmulgt11d 9807	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴)))
Theorem	ltmulgt12d 9808	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐴 · 𝐵)))
Theorem	gt0divd 9809	Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵)))
Theorem	ge0divd 9810	Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
Theorem	rpgecld 9811	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ+)
Theorem	divge0d 9812	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵))
Theorem	ltmul1d 9813	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)))
Theorem	ltmul2d 9814	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 9815	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))
Theorem	lemul2d 9816	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))
Theorem	ltdiv1d 9817	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	lediv1d 9818	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 9819	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmuldiv2d 9820	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	lemuldivd 9821	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	lemuldiv2d 9822	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	ltdivmuld 9823	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵)))
Theorem	ltdivmul2d 9824	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶)))
Theorem	ledivmuld 9825	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵)))
Theorem	ledivmul2d 9826	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶)))
Theorem	ltmul1dd 9827	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶))
Theorem	ltmul2dd 9828	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 9829	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶))
Theorem	lediv1dd 9830	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 9831	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))
Theorem	ltdiv23d 9832	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵)
Theorem	lediv23d 9833	Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵)
Theorem	mul2lt0rlt0 9834	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ ((𝜑 ∧ 𝐵 < 0) → 0 < 𝐴)
Theorem	mul2lt0rgt0 9835	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 < 0)
Theorem	mul2lt0llt0 9836	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ ((𝜑 ∧ 𝐴 < 0) → 0 < 𝐵)
Theorem	mul2lt0lgt0 9837	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)    ⇒   ⊢ ((𝜑 ∧ 0 < 𝐴) → 𝐵 < 0)
Theorem	mul2lt0np 9838	The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) < 0)
Theorem	mul2lt0pn 9839	The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 0 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐵 · 𝐴) < 0)
Theorem	lt2mul2divd 9840	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))
Theorem	nnledivrp 9841	Division of a positive integer by a positive number is less than or equal to the integer iff the number is greater than or equal to 1. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → (1 ≤ 𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐴))
Theorem	nn0ledivnn 9842	Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≤ 𝐴)
Theorem	addlelt 9843	If the sum of a real number and a positive real number is less than or equal to a third real number, the first real number is less than the third real number. (Contributed by AV, 1-Jul-2021.)
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁 → 𝑀 < 𝑁))
4.5.2  Infinity and the extended real number system (cont.)
Syntax	cxne 9844	Extend class notation to include the negative of an extended real.
class -𝑒𝐴
Syntax	cxad 9845	Extend class notation to include addition of extended reals.
class +𝑒
Syntax	cxmu 9846	Extend class notation to include multiplication of extended reals.
class ·e
Definition	df-xneg 9847	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
Definition	df-xadd 9848*	Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
Definition	df-xmul 9849*	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	ltxr 9850	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 9851	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Theorem	xrnemnf 9852	An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))
Theorem	xrnepnf 9853	An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞))
Theorem	xrltnr 9854	The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)
Theorem	ltpnf 9855	Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
Theorem	ltpnfd 9856	Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 < +∞)
Theorem	0ltpnf 9857	Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 < +∞
Theorem	mnflt 9858	Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
Theorem	mnflt0 9859	Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ < 0
Theorem	mnfltpnf 9860	Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ -∞ < +∞
Theorem	mnfltxr 9861	Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴)
Theorem	pnfnlt 9862	No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
Theorem	nltmnf 9863	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
Theorem	pnfge 9864	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
Theorem	0lepnf 9865	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≤ +∞
Theorem	nn0pnfge0 9866	If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
⊢ ((𝑁 ∈ ℕ0 ∨ 𝑁 = +∞) → 0 ≤ 𝑁)
Theorem	mnfle 9867	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
Theorem	xrltnsym 9868	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
Theorem	xrltnsym2 9869	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴))
Theorem	xrlttr 9870	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	xrltso 9871	'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
⊢ < Or ℝ*
Theorem	xrlttri3 9872	Extended real version of lttri3 8106. (Contributed by NM, 9-Feb-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
Theorem	xrltle 9873	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
Theorem	xrltled 9874	'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 9873. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	xrleid 9875	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴)
Theorem	xrleidd 9876	'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 9875. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐴)
Theorem	xnn0dcle 9877	Decidability of ≤ for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → DECID 𝐴 ≤ 𝐵)
Theorem	xnn0letri 9878	Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴))
Theorem	xrletri3 9879	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
Theorem	xrletrid 9880	Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	xrlelttr 9881	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	xrltletr 9882	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
Theorem	xrletr 9883	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	xrlttrd 9884	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrlelttrd 9885	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrltletrd 9886	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrletrd 9887	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	xrltne 9888	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
Theorem	nltpnft 9889	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))
Theorem	npnflt 9890	An extended real is less than plus infinity iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
⊢ (𝐴 ∈ ℝ* → (𝐴 < +∞ ↔ 𝐴 ≠ +∞))
Theorem	xgepnf 9891	An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞))
Theorem	ngtmnft 9892	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
Theorem	nmnfgt 9893	An extended real is greater than minus infinite iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
⊢ (𝐴 ∈ ℝ* → (-∞ < 𝐴 ↔ 𝐴 ≠ -∞))
Theorem	xrrebnd 9894	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞)))
Theorem	xrre 9895	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
Theorem	xrre2 9896	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ)
Theorem	xrre3 9897	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ)
Theorem	ge0gtmnf 9898	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
Theorem	ge0nemnf 9899	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞)
Theorem	xrrege0 9900	A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)