P. 132 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltdiv1d 13101	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))
Theorem	lediv1d 13102	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 13103	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	ltmuldiv2d 13104	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶)))
Theorem	lemuldivd 13105	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	lemuldiv2d 13106	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶)))
Theorem	ltdivmuld 13107	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵)))
Theorem	ltdivmul2d 13108	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶)))
Theorem	ledivmuld 13109	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵)))
Theorem	ledivmul2d 13110	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶)))
Theorem	ltmul1dd 13111	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶))
Theorem	ltmul2dd 13112	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 13113	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶))
Theorem	lediv1dd 13114	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 13115	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))
Theorem	mul2lt0rlt0 13116	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 13117	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 13118	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 13119	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	mul2lt0bi 13120	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 < 𝐵) ∨ (0 < 𝐴 ∧ 𝐵 < 0))))
Theorem	prodge0rd 13121	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.) (Revised by AV, 9-Jul-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))    ⇒   ⊢ (𝜑 → 0 ≤ 𝐵)
Theorem	prodge0ld 13122	Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by AV, 9-Jul-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))    ⇒   ⊢ (𝜑 → 0 ≤ 𝐴)
Theorem	ltdiv23d 13123	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) < 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) < 𝐵)
Theorem	lediv23d 13124	Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 / 𝐵) ≤ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) ≤ 𝐵)
Theorem	lt2mul2divd 13125	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))
Theorem	nnledivrp 13126	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 13127	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 13128	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.)
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁 → 𝑀 < 𝑁))
5.5.2  Infinity and the extended real number system (cont.)
Syntax	cxne 13129	Extend class notation to include the negative of an extended real.
class -𝑒𝐴
Syntax	cxad 13130	Extend class notation to include addition of extended reals.
class +𝑒
Syntax	cxmu 13131	Extend class notation to include multiplication of extended reals.
class ·e
Definition	df-xneg 13132	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
Definition	df-xadd 13133*	Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ +𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))
Definition	df-xmul 13134*	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 13135	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 13136	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Theorem	xrnemnf 13137	An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))
Theorem	xrnepnf 13138	An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞))
Theorem	xrltnr 13139	The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)
Theorem	ltpnf 13140	Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
Theorem	ltpnfd 13141	Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 < +∞)
Theorem	0ltpnf 13142	Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 < +∞
Theorem	mnflt 13143	Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
Theorem	mnfltd 13144	Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → -∞ < 𝐴)
Theorem	mnflt0 13145	Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ < 0
Theorem	mnfltpnf 13146	Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ -∞ < +∞
Theorem	mnfltxr 13147	Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴)
Theorem	pnfnlt 13148	No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
Theorem	nltmnf 13149	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
Theorem	pnfge 13150	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
Theorem	xnn0n0n1ge2b 13151	An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021.)
⊢ (𝑁 ∈ ℕ0* → ((𝑁 ≠ 0 ∧ 𝑁 ≠ 1) ↔ 2 ≤ 𝑁))
Theorem	0lepnf 13152	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≤ +∞
Theorem	xnn0ge0 13153	An extended nonnegative integer is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 10-Dec-2020.)
⊢ (𝑁 ∈ ℕ0* → 0 ≤ 𝑁)
Theorem	mnfle 13154	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
Theorem	mnfled 13155	Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -∞ ≤ 𝐴)
Theorem	xrltnsym 13156	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
Theorem	xrltnsym2 13157	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴))
Theorem	xrlttri 13158	Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri 11220 or axlttri 11323. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	xrlttr 13159	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	xrltso 13160	'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
⊢ < Or ℝ*
Theorem	xrlttri2 13161	Trichotomy law for 'less than' for extended reals. (Contributed by NM, 10-Dec-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≠ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	xrlttri3 13162	Trichotomy law for 'less than' for extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
Theorem	xrleloe 13163	'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	xrleltne 13164	'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴))
Theorem	xrltlen 13165	'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴)))
Theorem	dfle2 13166	Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ ≤ = ( < ∪ ( I ↾ ℝ*))
Theorem	dflt2 13167	Alternative definition of 'less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.)
⊢ < = ( ≤ ∖ I )
Theorem	xrltle 13168	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
Theorem	xrltled 13169	'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 13168. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	xrleid 13170	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴)
Theorem	xrleidd 13171	'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 13170. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐴)
Theorem	xrletri 13172	Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴))
Theorem	xrletri3 13173	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
Theorem	xrletrid 13174	Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	xrlelttr 13175	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
Theorem	xrltletr 13176	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
Theorem	xrletr 13177	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
Theorem	xrlttrd 13178	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrlelttrd 13179	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrltletrd 13180	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrletrd 13181	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	xrltne 13182	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
Theorem	nltpnft 13183	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))
Theorem	xgepnf 13184	An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞))
Theorem	ngtmnft 13185	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
Theorem	xlemnf 13186	An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ -∞ ↔ 𝐴 = -∞))
Theorem	xrrebnd 13187	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞)))
Theorem	xrre 13188	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
Theorem	xrre2 13189	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ)
Theorem	xrre3 13190	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ)
Theorem	ge0gtmnf 13191	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
Theorem	ge0nemnf 13192	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞)
Theorem	xrrege0 13193	A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
Theorem	xrmax1 13194	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	xrmax2 13195	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	xrmin1 13196	The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	xrmin2 13197	The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	xrmaxeq 13198	The maximum of two extended reals is equal to the first if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐴)
Theorem	xrmineq 13199	The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) = 𝐵)
Theorem	xrmaxlt 13200	Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))