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	rpge0d 8401	A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → 0 ≤ A)
Theorem	rpne0d 8402	A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → A ≠ 0)
Theorem	rpregt0d 8403	A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (A ∈ ℝ ∧ 0 < A))
Theorem	rprege0d 8404	A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (A ∈ ℝ ∧ 0 ≤ A))
Theorem	rprene0d 8405	A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (A ∈ ℝ ∧ A ≠ 0))
Theorem	rpcnne0d 8406	A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (A ∈ ℂ ∧ A ≠ 0))
Theorem	rpreccld 8407	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (1 / A) ∈ ℝ+)
Theorem	rprecred 8408	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (1 / A) ∈ ℝ)
Theorem	rphalfcld 8409	Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (A / 2) ∈ ℝ+)
Theorem	reclt1d 8410	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (A < 1 ↔ 1 < (1 / A)))
Theorem	recgt1d 8411	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    ⇒   ⊢ (φ → (1 < A ↔ (1 / A) < 1))
Theorem	rpaddcld 8412	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A + B) ∈ ℝ+)
Theorem	rpmulcld 8413	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A · B) ∈ ℝ+)
Theorem	rpdivcld 8414	Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A / B) ∈ ℝ+)
Theorem	ltrecd 8415	The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A < B ↔ (1 / B) < (1 / A)))
Theorem	lerecd 8416	The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A ≤ B ↔ (1 / B) ≤ (1 / A)))
Theorem	ltrec1d 8417	Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → (1 / A) < B)    ⇒   ⊢ (φ → (1 / B) < A)
Theorem	lerec2d 8418	Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → A ≤ (1 / B))    ⇒   ⊢ (φ → B ≤ (1 / A))
Theorem	lediv2ad 8419	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ)    &   ⊢ (φ → 0 ≤ 𝐶)    &   ⊢ (φ → A ≤ B)    ⇒   ⊢ (φ → (𝐶 / B) ≤ (𝐶 / A))
Theorem	ltdiv2d 8420	Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A < B ↔ (𝐶 / B) < (𝐶 / A)))
Theorem	lediv2d 8421	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 8422	Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ+)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → 𝐷 ∈ ℝ+)    &   ⊢ (φ → (A / B) ≤ (𝐶 / 𝐷))    ⇒   ⊢ (φ → (𝐷 / 𝐶) ≤ (B / A))
Theorem	ge0p1rpd 8423	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    ⇒   ⊢ (φ → (A + 1) ∈ ℝ+)
Theorem	rerpdivcld 8424	Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A / B) ∈ ℝ)
Theorem	ltsubrpd 8425	Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (A − B) < A)
Theorem	ltaddrpd 8426	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → A < (A + B))
Theorem	ltaddrp2d 8427	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → A < (B + A))
Theorem	ltmulgt11d 8428	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (1 < A ↔ B < (B · A)))
Theorem	ltmulgt12d 8429	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    ⇒   ⊢ (φ → (1 < A ↔ B < (A · B)))
Theorem	gt0divd 8430	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 8431	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 8432	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 8433	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 8434	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → (A < B ↔ (A · 𝐶) < (B · 𝐶)))
Theorem	ltmul2d 8435	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 8436	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 8437	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 8438	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 8439	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 8440	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A · 𝐶) < B ↔ A < (B / 𝐶)))
Theorem	ltmuldiv2d 8441	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((𝐶 · A) < B ↔ A < (B / 𝐶)))
Theorem	lemuldivd 8442	'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 8443	'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 8444	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) < B ↔ A < (𝐶 · B)))
Theorem	ltdivmul2d 8445	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) < B ↔ A < (B · 𝐶)))
Theorem	ledivmuld 8446	'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 8447	'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 8448	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → A < B)    ⇒   ⊢ (φ → (A · 𝐶) < (B · 𝐶))
Theorem	ltmul2dd 8449	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 8450	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 8451	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 8452	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → 𝐷 ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → 𝐶 ≤ 𝐷)    ⇒   ⊢ (φ → (A / 𝐷) ≤ (B / 𝐶))
Theorem	ltdiv23d 8453	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → (A / B) < 𝐶)    ⇒   ⊢ (φ → (A / 𝐶) < B)
Theorem	lediv23d 8454	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 8455	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 8456	Extend class notation to include the negative of an extended real.
class -𝑒A
Syntax	cxad 8457	Extend class notation to include addition of extended reals.
class +𝑒
Syntax	cxmu 8458	Extend class notation to include multiplication of extended reals.
class ·e
Definition	df-xneg 8459	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒A = if(A = +∞, -∞, if(A = -∞, +∞, -A))
Definition	df-xadd 8460*	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 8461*	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 8462	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 8463	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ +∞ ∈ V
Theorem	mnfxr 8464	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 8465	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 8466	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ* ↔ (A ∈ ℝ ∨ A = +∞ ∨ A = -∞))
Theorem	pnfnemnf 8467	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 8468	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	xrnemnf 8469	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 8470	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 8471	The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ A < A)
Theorem	ltpnf 8472	Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ → A < +∞)
Theorem	0ltpnf 8473	Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 < +∞
Theorem	mnflt 8474	Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ → -∞ < A)
Theorem	mnflt0 8475	Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ < 0
Theorem	mnfltpnf 8476	Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ -∞ < +∞
Theorem	mnfltxr 8477	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 8478	No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ +∞ < A)
Theorem	nltmnf 8479	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ A < -∞)
Theorem	pnfge 8480	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
⊢ (A ∈ ℝ* → A ≤ +∞)
Theorem	0lepnf 8481	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≤ +∞
Theorem	nn0pnfge0 8482	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 8483	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
⊢ (A ∈ ℝ* → -∞ ≤ A)
Theorem	xrltnsym 8484	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B → ¬ B < A))
Theorem	xrltnsym2 8485	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ (A < B ∧ B < A))
Theorem	xrlttr 8486	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A < B ∧ B < 𝐶) → A < 𝐶))
Theorem	xrltso 8487	'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
⊢ < Or ℝ*
Theorem	xrlttri3 8488	Extended real version of lttri3 6895. (Contributed by NM, 9-Feb-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔ (¬ A < B ∧ ¬ B < A)))
Theorem	xrltle 8489	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B → A ≤ B))
Theorem	xrleid 8490	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
⊢ (A ∈ ℝ* → A ≤ A)
Theorem	xrletri3 8491	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔ (A ≤ B ∧ B ≤ A)))
Theorem	xrlelttr 8492	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A ≤ B ∧ B < 𝐶) → A < 𝐶))
Theorem	xrltletr 8493	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A < B ∧ B ≤ 𝐶) → A < 𝐶))
Theorem	xrletr 8494	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A ≤ B ∧ B ≤ 𝐶) → A ≤ 𝐶))
Theorem	xrlttrd 8495	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B < 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrlelttrd 8496	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B < 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrltletrd 8497	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B ≤ 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrletrd 8498	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B ≤ 𝐶)    ⇒   ⊢ (φ → A ≤ 𝐶)
Theorem	xrltne 8499	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → B ≠ A)
Theorem	nltpnft 8500	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
⊢ (A ∈ ℝ* → (A = +∞ ↔ ¬ A < +∞))