P. 85 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8401-8500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lediv2d 8401	Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A ≤ B ↔ (𝐶 / B) ≤ (𝐶 / A)))
Theorem	ledivdivd 8402	Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → 𝐷 ∈ ℝ+)    &   ⊢ (φ → (A / B) ≤ (𝐶 / 𝐷))    ⇒   ⊢ (φ → (𝐷 / 𝐶) ≤ (B / A))
Theorem	ge0p1rpd 8403	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    ⇒   ⊢ (φ → (A + 1) ∈ ℝ+)
Theorem	rerpdivcld 8404	Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A / B) ∈ ℝ)
Theorem	ltsubrpd 8405	Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A − B) < A)
Theorem	ltaddrpd 8406	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → A < (A + B))
Theorem	ltaddrp2d 8407	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → A < (B + A))
Theorem	ltmulgt11d 8408	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (1 < A ↔ B < (B · A)))
Theorem	ltmulgt12d 8409	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (1 < A ↔ B < (A · B)))
Theorem	gt0divd 8410	Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (0 < A ↔ 0 < (A / B)))
Theorem	ge0divd 8411	Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (0 ≤ A ↔ 0 ≤ (A / B)))
Theorem	rpgecld 8412	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → B ≤ A)    ⇒   ⊢ (φ → A ∈ ℝ+)
Theorem	divge0d 8413	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 0 ≤ A)    ⇒   ⊢ (φ → 0 ≤ (A / B))
Theorem	ltmul1d 8414	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A < B ↔ (A · 𝐶) < (B · 𝐶)))
Theorem	ltmul2d 8415	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.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A < B ↔ (𝐶 · A) < (𝐶 · B)))
Theorem	lemul1d 8416	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A ≤ B ↔ (A · 𝐶) ≤ (B · 𝐶)))
Theorem	lemul2d 8417	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A ≤ B ↔ (𝐶 · A) ≤ (𝐶 · B)))
Theorem	ltdiv1d 8418	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A < B ↔ (A / 𝐶) < (B / 𝐶)))
Theorem	lediv1d 8419	Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A ≤ B ↔ (A / 𝐶) ≤ (B / 𝐶)))
Theorem	ltmuldivd 8420	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A · 𝐶) < B ↔ A < (B / 𝐶)))
Theorem	ltmuldiv2d 8421	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((𝐶 · A) < B ↔ A < (B / 𝐶)))
Theorem	lemuldivd 8422	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A · 𝐶) ≤ B ↔ A ≤ (B / 𝐶)))
Theorem	lemuldiv2d 8423	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((𝐶 · A) ≤ B ↔ A ≤ (B / 𝐶)))
Theorem	ltdivmuld 8424	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) < B ↔ A < (𝐶 · B)))
Theorem	ltdivmul2d 8425	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) < B ↔ A < (B · 𝐶)))
Theorem	ledivmuld 8426	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) ≤ B ↔ A ≤ (𝐶 · B)))
Theorem	ledivmul2d 8427	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) ≤ B ↔ A ≤ (B · 𝐶)))
Theorem	ltmul1dd 8428	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → A < B)    ⇒   ⊢ (φ → (A · 𝐶) < (B · 𝐶))
Theorem	ltmul2dd 8429	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.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → A < B)    ⇒   ⊢ (φ → (𝐶 · A) < (𝐶 · B))
Theorem	ltdiv1dd 8430	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → A < B)    ⇒   ⊢ (φ → (A / 𝐶) < (B / 𝐶))
Theorem	lediv1dd 8431	Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → A ≤ B)    ⇒   ⊢ (φ → (A / 𝐶) ≤ (B / 𝐶))
Theorem	lediv12ad 8432	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → 𝐷 ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → 𝐶 ≤ 𝐷)    ⇒   ⊢ (φ → (A / 𝐷) ≤ (B / 𝐶))
Theorem	ltdiv23d 8433	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → (A / B) < 𝐶)    ⇒   ⊢ (φ → (A / 𝐶) < B)
Theorem	lediv23d 8434	Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → (A / B) ≤ 𝐶)    ⇒   ⊢ (φ → (A / 𝐶) ≤ B)
Theorem	lt2mul2divd 8435	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 𝐷 ∈ ℝ+)    ⇒   ⊢ (φ → ((A · B) < (𝐶 · 𝐷) ↔ (A / 𝐷) < (𝐶 / B)))
3.5.2  Infinity and the extended real number system (cont.)
Syntax	cxne 8436	Extend class notation to include the negative of an extended real.
class -𝑒A
Syntax	cxad 8437	Extend class notation to include addition of extended reals.
class +𝑒
Syntax	cxmu 8438	Extend class notation to include multiplication of extended reals.
class ·e
Definition	df-xneg 8439	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒A = if(A = +∞, -∞, if(A = -∞, +∞, -A))
Definition	df-xadd 8440*	Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ +𝑒 = (x ∈ ℝ*, y ∈ ℝ* ↦ if(x = +∞, if(y = -∞, 0, +∞), if(x = -∞, if(y = +∞, 0, -∞), if(y = +∞, +∞, if(y = -∞, -∞, (x + y))))))
Definition	df-xmul 8441*	Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ·e = (x ∈ ℝ*, y ∈ ℝ* ↦ if((x = 0 ∨ y = 0), 0, if((((0 < y ∧ x = +∞) ∨ (y < 0 ∧ x = -∞)) ∨ ((0 < x ∧ y = +∞) ∨ (x < 0 ∧ y = -∞))), +∞, if((((0 < y ∧ x = -∞) ∨ (y < 0 ∧ x = +∞)) ∨ ((0 < x ∧ y = -∞) ∨ (x < 0 ∧ y = +∞))), -∞, (x · y)))))
Theorem	pnfxr 8442	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 8443	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ +∞ ∈ V
Theorem	mnfxr 8444	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 8445	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.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔ ((((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B) ∨ (A = -∞ ∧ B = +∞)) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ)))))
Theorem	elxr 8446	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ* ↔ (A ∈ ℝ ∨ A = +∞ ∨ A = -∞))
Theorem	pnfnemnf 8447	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 8448	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	xrnemnf 8449	An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ A ≠ -∞) ↔ (A ∈ ℝ ∨ A = +∞))
Theorem	xrnepnf 8450	An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ A ≠ +∞) ↔ (A ∈ ℝ ∨ A = -∞))
Theorem	xrltnr 8451	The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ A < A)
Theorem	ltpnf 8452	Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ → A < +∞)
Theorem	0ltpnf 8453	Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 < +∞
Theorem	mnflt 8454	Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ → -∞ < A)
Theorem	mnflt0 8455	Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ < 0
Theorem	mnfltpnf 8456	Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ -∞ < +∞
Theorem	mnfltxr 8457	Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
⊢ ((A ∈ ℝ ∨ A = +∞) → -∞ < A)
Theorem	pnfnlt 8458	No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ +∞ < A)
Theorem	nltmnf 8459	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ A < -∞)
Theorem	pnfge 8460	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
⊢ (A ∈ ℝ* → A ≤ +∞)
Theorem	0lepnf 8461	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≤ +∞
Theorem	nn0pnfge0 8462	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 8463	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
⊢ (A ∈ ℝ* → -∞ ≤ A)
Theorem	xrltnsym 8464	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B → ¬ B < A))
Theorem	xrltnsym2 8465	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ (A < B ∧ B < A))
Theorem	xrlttr 8466	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A < B ∧ B < 𝐶) → A < 𝐶))
Theorem	xrltso 8467	'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
⊢ < Or ℝ*
Theorem	xrlttri3 8468	Extended real version of lttri3 6875. (Contributed by NM, 9-Feb-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔ (¬ A < B ∧ ¬ B < A)))
Theorem	xrltle 8469	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B → A ≤ B))
Theorem	xrleid 8470	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
⊢ (A ∈ ℝ* → A ≤ A)
Theorem	xrletri3 8471	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔ (A ≤ B ∧ B ≤ A)))
Theorem	xrlelttr 8472	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A ≤ B ∧ B < 𝐶) → A < 𝐶))
Theorem	xrltletr 8473	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A < B ∧ B ≤ 𝐶) → A < 𝐶))
Theorem	xrletr 8474	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A ≤ B ∧ B ≤ 𝐶) → A ≤ 𝐶))
Theorem	xrlttrd 8475	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B < 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrlelttrd 8476	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B < 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrltletrd 8477	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B ≤ 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrletrd 8478	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B ≤ 𝐶)    ⇒   ⊢ (φ → A ≤ 𝐶)
Theorem	xrltne 8479	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → B ≠ A)
Theorem	nltpnft 8480	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
⊢ (A ∈ ℝ* → (A = +∞ ↔ ¬ A < +∞))
Theorem	ngtmnft 8481	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
⊢ (A ∈ ℝ* → (A = -∞ ↔ ¬ -∞ < A))
Theorem	xrrebnd 8482	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
⊢ (A ∈ ℝ* → (A ∈ ℝ ↔ (-∞ < A ∧ A < +∞)))
Theorem	xrre 8483	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (-∞ < A ∧ A ≤ B)) → A ∈ ℝ)
Theorem	xrre2 8484	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (A < B ∧ B < 𝐶)) → B ∈ ℝ)
Theorem	xrre3 8485	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (B ≤ A ∧ A < +∞)) → A ∈ ℝ)
Theorem	ge0gtmnf 8486	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ 0 ≤ A) → -∞ < A)
Theorem	ge0nemnf 8487	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ 0 ≤ A) → A ≠ -∞)
Theorem	xrrege0 8488	A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (0 ≤ A ∧ A ≤ B)) → A ∈ ℝ)
Theorem	z2ge 8489*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘))
Theorem	xnegeq 8490	Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
⊢ (A = B → -𝑒A = -𝑒B)
Theorem	xnegpnf 8491	Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒+∞ = -∞
Theorem	xnegmnf 8492	Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒-∞ = +∞
Theorem	rexneg 8493	Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ → -𝑒A = -A)
Theorem	xneg0 8494	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒0 = 0
Theorem	xnegcl 8495	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → -𝑒A ∈ ℝ*)
Theorem	xnegneg 8496	Extended real version of negneg 7037. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → -𝑒-𝑒A = A)
Theorem	xneg11 8497	Extended real version of neg11 7038. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (-𝑒A = -𝑒B ↔ A = B))
Theorem	xltnegi 8498	Forward direction of xltneg 8499. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → -𝑒B < -𝑒A)
Theorem	xltneg 8499	Extended real version of ltneg 7232. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔ -𝑒B < -𝑒A))
Theorem	xleneg 8500	Extended real version of leneg 7235. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A ≤ B ↔ -𝑒B ≤ -𝑒A))