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	ltmuldiv2d 8401	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((𝐶 · A) < B ↔ A < (B / 𝐶)))
Theorem	lemuldivd 8402	'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 8403	'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 8404	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) < B ↔ A < (𝐶 · B)))
Theorem	ltdivmul2d 8405	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    ⇒   ⊢ (φ → ((A / 𝐶) < B ↔ A < (B · 𝐶)))
Theorem	ledivmuld 8406	'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 8407	'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 8408	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → A < B)    ⇒   ⊢ (φ → (A · 𝐶) < (B · 𝐶))
Theorem	ltmul2dd 8409	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 8410	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 8411	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 8412	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → 𝐷 ∈ ℝ)    &   ⊢ (φ → 0 ≤ A)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → 𝐶 ≤ 𝐷)    ⇒   ⊢ (φ → (A / 𝐷) ≤ (B / 𝐶))
Theorem	ltdiv23d 8413	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ+)    &   ⊢ (φ → 𝐶 ∈ ℝ+)    &   ⊢ (φ → (A / B) < 𝐶)    ⇒   ⊢ (φ → (A / 𝐶) < B)
Theorem	lediv23d 8414	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 8415	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 8416	Extend class notation to include the negative of an extended real.
class -𝑒A
Syntax	cxad 8417	Extend class notation to include addition of extended reals.
class +𝑒
Syntax	cxmu 8418	Extend class notation to include multiplication of extended reals.
class ·e
Definition	df-xneg 8419	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒A = if(A = +∞, -∞, if(A = -∞, +∞, -A))
Definition	df-xadd 8420*	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 8421*	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 8422	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 8423	Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ +∞ ∈ V
Theorem	mnfxr 8424	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 8425	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 8426	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ* ↔ (A ∈ ℝ ∨ A = +∞ ∨ A = -∞))
Theorem	pnfnemnf 8427	Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.)
⊢ +∞ ≠ -∞
Theorem	mnfnepnf 8428	Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ ≠ +∞
Theorem	xrnemnf 8429	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 8430	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 8431	The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ A < A)
Theorem	ltpnf 8432	Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ → A < +∞)
Theorem	0ltpnf 8433	Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 < +∞
Theorem	mnflt 8434	Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
⊢ (A ∈ ℝ → -∞ < A)
Theorem	mnflt0 8435	Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -∞ < 0
Theorem	mnfltpnf 8436	Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
⊢ -∞ < +∞
Theorem	mnfltxr 8437	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 8438	No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ +∞ < A)
Theorem	nltmnf 8439	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ (A ∈ ℝ* → ¬ A < -∞)
Theorem	pnfge 8440	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
⊢ (A ∈ ℝ* → A ≤ +∞)
Theorem	0lepnf 8441	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≤ +∞
Theorem	nn0pnfge0 8442	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 8443	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
⊢ (A ∈ ℝ* → -∞ ≤ A)
Theorem	xrltnsym 8444	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B → ¬ B < A))
Theorem	xrltnsym2 8445	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ (A < B ∧ B < A))
Theorem	xrlttr 8446	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A < B ∧ B < 𝐶) → A < 𝐶))
Theorem	xrltso 8447	'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
⊢ < Or ℝ*
Theorem	xrlttri3 8448	Extended real version of lttri3 6855. (Contributed by NM, 9-Feb-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔ (¬ A < B ∧ ¬ B < A)))
Theorem	xrltle 8449	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B → A ≤ B))
Theorem	xrleid 8450	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
⊢ (A ∈ ℝ* → A ≤ A)
Theorem	xrletri3 8451	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A = B ↔ (A ≤ B ∧ B ≤ A)))
Theorem	xrlelttr 8452	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A ≤ B ∧ B < 𝐶) → A < 𝐶))
Theorem	xrltletr 8453	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A < B ∧ B ≤ 𝐶) → A < 𝐶))
Theorem	xrletr 8454	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A ≤ B ∧ B ≤ 𝐶) → A ≤ 𝐶))
Theorem	xrlttrd 8455	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B < 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrlelttrd 8456	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B < 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrltletrd 8457	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A < B)    &   ⊢ (φ → B ≤ 𝐶)    ⇒   ⊢ (φ → A < 𝐶)
Theorem	xrletrd 8458	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (φ → A ∈ ℝ*)    &   ⊢ (φ → B ∈ ℝ*)    &   ⊢ (φ → 𝐶 ∈ ℝ*)    &   ⊢ (φ → A ≤ B)    &   ⊢ (φ → B ≤ 𝐶)    ⇒   ⊢ (φ → A ≤ 𝐶)
Theorem	xrltne 8459	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → B ≠ A)
Theorem	nltpnft 8460	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
⊢ (A ∈ ℝ* → (A = +∞ ↔ ¬ A < +∞))
Theorem	ngtmnft 8461	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
⊢ (A ∈ ℝ* → (A = -∞ ↔ ¬ -∞ < A))
Theorem	xrrebnd 8462	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
⊢ (A ∈ ℝ* → (A ∈ ℝ ↔ (-∞ < A ∧ A < +∞)))
Theorem	xrre 8463	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (-∞ < A ∧ A ≤ B)) → A ∈ ℝ)
Theorem	xrre2 8464	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (A < B ∧ B < 𝐶)) → B ∈ ℝ)
Theorem	xrre3 8465	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (B ≤ A ∧ A < +∞)) → A ∈ ℝ)
Theorem	ge0gtmnf 8466	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ 0 ≤ A) → -∞ < A)
Theorem	ge0nemnf 8467	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ 0 ≤ A) → A ≠ -∞)
Theorem	xrrege0 8468	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 8469*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘))
Theorem	xnegeq 8470	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 8471	Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒+∞ = -∞
Theorem	xnegmnf 8472	Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒-∞ = +∞
Theorem	rexneg 8473	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 8474	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒0 = 0
Theorem	xnegcl 8475	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → -𝑒A ∈ ℝ*)
Theorem	xnegneg 8476	Extended real version of negneg 7017. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → -𝑒-𝑒A = A)
Theorem	xneg11 8477	Extended real version of neg11 7018. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (-𝑒A = -𝑒B ↔ A = B))
Theorem	xltnegi 8478	Forward direction of xltneg 8479. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → -𝑒B < -𝑒A)
Theorem	xltneg 8479	Extended real version of ltneg 7212. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔ -𝑒B < -𝑒A))
Theorem	xleneg 8480	Extended real version of leneg 7215. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A ≤ B ↔ -𝑒B ≤ -𝑒A))
Theorem	xlt0neg1 8481	Extended real version of lt0neg1 7218. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → (A < 0 ↔ 0 < -𝑒A))
Theorem	xlt0neg2 8482	Extended real version of lt0neg2 7219. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → (0 < A ↔ -𝑒A < 0))
Theorem	xle0neg1 8483	Extended real version of le0neg1 7220. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (A ∈ ℝ* → (A ≤ 0 ↔ 0 ≤ -𝑒A))
Theorem	xle0neg2 8484	Extended real version of le0neg2 7221. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (A ∈ ℝ* → (0 ≤ A ↔ -𝑒A ≤ 0))
Theorem	xnegcld 8485	Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ*)    ⇒   ⊢ (φ → -𝑒A ∈ ℝ*)
Theorem	xrex 8486	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
⊢ ℝ* ∈ V
3.5.3  Real number intervals
Syntax	cioo 8487	Extend class notation with the set of open intervals of extended reals.
class (,)
Syntax	cioc 8488	Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
Syntax	cico 8489	Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
Syntax	cicc 8490	Extend class notation with the set of closed intervals of extended reals.
class [,]
Definition	df-ioo 8491*	Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
⊢ (,) = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x < z ∧ z < y)})
Definition	df-ioc 8492*	Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
⊢ (,] = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x < z ∧ z ≤ y)})
Definition	df-ico 8493*	Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
⊢ [,) = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x ≤ z ∧ z < y)})
Definition	df-icc 8494*	Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
⊢ [,] = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x ≤ z ∧ z ≤ y)})
Theorem	ixxval 8495*	Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    ⇒   ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A𝑂B) = {z ∈ ℝ* ∣ (A𝑅z ∧ z𝑆B)})
Theorem	elixx1 8496*	Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    ⇒   ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A𝑂B) ↔ (𝐶 ∈ ℝ* ∧ A𝑅𝐶 ∧ 𝐶𝑆B)))
Theorem	ixxf 8497*	The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    ⇒   ⊢ 𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ*
Theorem	ixxex 8498*	The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    ⇒   ⊢ 𝑂 ∈ V
Theorem	ixxssxr 8499*	The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    ⇒   ⊢ (A𝑂B) ⊆ ℝ*
Theorem	elixx3g 8500*	Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A ∈ ℝ* and B ∈ ℝ*. (Contributed by Mario Carneiro, 3-Nov-2013.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    ⇒   ⊢ (𝐶 ∈ (A𝑂B) ↔ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (A𝑅𝐶 ∧ 𝐶𝑆B)))