P. 86 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8501-8600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ngtmnft 8501	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
⊢ (A ∈ ℝ* → (A = -∞ ↔ ¬ -∞ < A))
Theorem	xrrebnd 8502	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
⊢ (A ∈ ℝ* → (A ∈ ℝ ↔ (-∞ < A ∧ A < +∞)))
Theorem	xrre 8503	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (-∞ < A ∧ A ≤ B)) → A ∈ ℝ)
Theorem	xrre2 8504	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (A < B ∧ B < 𝐶)) → B ∈ ℝ)
Theorem	xrre3 8505	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ) ∧ (B ≤ A ∧ A < +∞)) → A ∈ ℝ)
Theorem	ge0gtmnf 8506	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ 0 ≤ A) → -∞ < A)
Theorem	ge0nemnf 8507	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ 0 ≤ A) → A ≠ -∞)
Theorem	xrrege0 8508	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 8509*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘))
Theorem	xnegeq 8510	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 8511	Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒+∞ = -∞
Theorem	xnegmnf 8512	Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒-∞ = +∞
Theorem	rexneg 8513	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 8514	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒0 = 0
Theorem	xnegcl 8515	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → -𝑒A ∈ ℝ*)
Theorem	xnegneg 8516	Extended real version of negneg 7057. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → -𝑒-𝑒A = A)
Theorem	xneg11 8517	Extended real version of neg11 7058. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (-𝑒A = -𝑒B ↔ A = B))
Theorem	xltnegi 8518	Forward direction of xltneg 8519. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → -𝑒B < -𝑒A)
Theorem	xltneg 8519	Extended real version of ltneg 7252. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔ -𝑒B < -𝑒A))
Theorem	xleneg 8520	Extended real version of leneg 7255. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A ≤ B ↔ -𝑒B ≤ -𝑒A))
Theorem	xlt0neg1 8521	Extended real version of lt0neg1 7258. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → (A < 0 ↔ 0 < -𝑒A))
Theorem	xlt0neg2 8522	Extended real version of lt0neg2 7259. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (A ∈ ℝ* → (0 < A ↔ -𝑒A < 0))
Theorem	xle0neg1 8523	Extended real version of le0neg1 7260. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (A ∈ ℝ* → (A ≤ 0 ↔ 0 ≤ -𝑒A))
Theorem	xle0neg2 8524	Extended real version of le0neg2 7261. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (A ∈ ℝ* → (0 ≤ A ↔ -𝑒A ≤ 0))
Theorem	xnegcld 8525	Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℝ*)    ⇒   ⊢ (φ → -𝑒A ∈ ℝ*)
Theorem	xrex 8526	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
⊢ ℝ* ∈ V
3.5.3  Real number intervals
Syntax	cioo 8527	Extend class notation with the set of open intervals of extended reals.
class (,)
Syntax	cioc 8528	Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
Syntax	cico 8529	Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
Syntax	cicc 8530	Extend class notation with the set of closed intervals of extended reals.
class [,]
Definition	df-ioo 8531*	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 8532*	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 8533*	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 8534*	Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
⊢ [,] = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x ≤ z ∧ z ≤ y)})
Theorem	ixxval 8535*	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 8536*	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 8537*	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 8538*	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 8539*	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 8540*	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)))
Theorem	ixxssixx 8541*	An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    &   ⊢ 𝑃 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑈y)})    &   ⊢ ((A ∈ ℝ* ∧ w ∈ ℝ*) → (A𝑅w → A𝑇w))    &   ⊢ ((w ∈ ℝ* ∧ B ∈ ℝ*) → (w𝑆B → w𝑈B))    ⇒   ⊢ (A𝑂B) ⊆ (A𝑃B)
Theorem	ixxdisj 8542*	Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    &   ⊢ 𝑃 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑈y)})    &   ⊢ ((B ∈ ℝ* ∧ w ∈ ℝ*) → (B𝑇w ↔ ¬ w𝑆B))    ⇒   ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A𝑂B) ∩ (B𝑃𝐶)) = ∅)
Theorem	ixxss1 8543*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    &   ⊢ 𝑃 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑆y)})    &   ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ w ∈ ℝ*) → ((A𝑊B ∧ B𝑇w) → A𝑅w))    ⇒   ⊢ ((A ∈ ℝ* ∧ A𝑊B) → (B𝑃𝐶) ⊆ (A𝑂𝐶))
Theorem	ixxss2 8544*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    &   ⊢ 𝑃 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑇y)})    &   ⊢ ((w ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((w𝑇B ∧ B𝑊𝐶) → w𝑆𝐶))    ⇒   ⊢ ((𝐶 ∈ ℝ* ∧ B𝑊𝐶) → (A𝑃B) ⊆ (A𝑂𝐶))
Theorem	ixxss12 8545*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ 𝑂 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑅z ∧ z𝑆y)})    &   ⊢ 𝑃 = (x ∈ ℝ*, y ∈ ℝ* ↦ {z ∈ ℝ* ∣ (x𝑇z ∧ z𝑈y)})    &   ⊢ ((A ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ w ∈ ℝ*) → ((A𝑊𝐶 ∧ 𝐶𝑇w) → A𝑅w))    &   ⊢ ((w ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ B ∈ ℝ*) → ((w𝑈𝐷 ∧ 𝐷𝑋B) → w𝑆B))    ⇒   ⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A𝑊𝐶 ∧ 𝐷𝑋B)) → (𝐶𝑃𝐷) ⊆ (A𝑂B))
Theorem	iooex 8546	The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (,) ∈ V
Theorem	iooval 8547*	Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,)B) = {x ∈ ℝ* ∣ (A < x ∧ x < B)})
Theorem	iooidg 8548	An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
⊢ (A ∈ ℝ* → (A(,)A) = ∅)
Theorem	elioo3g 8549	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 NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝐶 ∈ (A(,)B) ↔ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (A < 𝐶 ∧ 𝐶 < B)))
Theorem	elioo1 8550	Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A(,)B) ↔ (𝐶 ∈ ℝ* ∧ A < 𝐶 ∧ 𝐶 < B)))
Theorem	elioore 8551	A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (A ∈ (B(,)𝐶) → A ∈ ℝ)
Theorem	lbioog 8552	An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ A ∈ (A(,)B))
Theorem	ubioog 8553	An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ B ∈ (A(,)B))
Theorem	iooval2 8554*	Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,)B) = {x ∈ ℝ ∣ (A < x ∧ x < B)})
Theorem	iooss1 8555	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
⊢ ((A ∈ ℝ* ∧ A ≤ B) → (B(,)𝐶) ⊆ (A(,)𝐶))
Theorem	iooss2 8556	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐶 ∈ ℝ* ∧ B ≤ 𝐶) → (A(,)B) ⊆ (A(,)𝐶))
Theorem	iocval 8557*	Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,]B) = {x ∈ ℝ* ∣ (A < x ∧ x ≤ B)})
Theorem	icoval 8558*	Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A[,)B) = {x ∈ ℝ* ∣ (A ≤ x ∧ x < B)})
Theorem	iccval 8559*	Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A[,]B) = {x ∈ ℝ* ∣ (A ≤ x ∧ x ≤ B)})
Theorem	elioo2 8560	Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A(,)B) ↔ (𝐶 ∈ ℝ ∧ A < 𝐶 ∧ 𝐶 < B)))
Theorem	elioc1 8561	Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A(,]B) ↔ (𝐶 ∈ ℝ* ∧ A < 𝐶 ∧ 𝐶 ≤ B)))
Theorem	elico1 8562	Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A[,)B) ↔ (𝐶 ∈ ℝ* ∧ A ≤ 𝐶 ∧ 𝐶 < B)))
Theorem	elicc1 8563	Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A[,]B) ↔ (𝐶 ∈ ℝ* ∧ A ≤ 𝐶 ∧ 𝐶 ≤ B)))
Theorem	iccid 8564	A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.)
⊢ (A ∈ ℝ* → (A[,]A) = {A})
Theorem	icc0r 8565	An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (B < A → (A[,]B) = ∅))
Theorem	eliooxr 8566	An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
⊢ (A ∈ (B(,)𝐶) → (B ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
Theorem	eliooord 8567	Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (A ∈ (B(,)𝐶) → (B < A ∧ A < 𝐶))
Theorem	ubioc1 8568	The upper bound belongs to an open-below, closed-above interval. See ubicc2 8623. (Contributed by FL, 29-May-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → B ∈ (A(,]B))
Theorem	lbico1 8569	The lower bound belongs to a closed-below, open-above interval. See lbicc2 8622. (Contributed by FL, 29-May-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → A ∈ (A[,)B))
Theorem	iccleub 8570	An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ (A[,]B)) → 𝐶 ≤ B)
Theorem	iccgelb 8571	An element of a closed interval is more than or equal to its lower bound (Contributed by Thierry Arnoux, 23-Dec-2016.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ (A[,]B)) → A ≤ 𝐶)
Theorem	elioo5 8572	Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (A(,)B) ↔ (A < 𝐶 ∧ 𝐶 < B)))
Theorem	elioo4g 8573	Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐶 ∈ (A(,)B) ↔ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ) ∧ (A < 𝐶 ∧ 𝐶 < B)))
Theorem	ioossre 8574	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
⊢ (A(,)B) ⊆ ℝ
Theorem	elioc2 8575	Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ) → (𝐶 ∈ (A(,]B) ↔ (𝐶 ∈ ℝ ∧ A < 𝐶 ∧ 𝐶 ≤ B)))
Theorem	elico2 8576	Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ*) → (𝐶 ∈ (A[,)B) ↔ (𝐶 ∈ ℝ ∧ A ≤ 𝐶 ∧ 𝐶 < B)))
Theorem	elicc2 8577	Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (𝐶 ∈ (A[,]B) ↔ (𝐶 ∈ ℝ ∧ A ≤ 𝐶 ∧ 𝐶 ≤ B)))
Theorem	elicc2i 8578	Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (𝐶 ∈ (A[,]B) ↔ (𝐶 ∈ ℝ ∧ A ≤ 𝐶 ∧ 𝐶 ≤ B))
Theorem	elicc4 8579	Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (A[,]B) ↔ (A ≤ 𝐶 ∧ 𝐶 ≤ B)))
Theorem	iccss 8580	Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.)
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ≤ 𝐶 ∧ 𝐷 ≤ B)) → (𝐶[,]𝐷) ⊆ (A[,]B))
Theorem	iccssioo 8581	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A < 𝐶 ∧ 𝐷 < B)) → (𝐶[,]𝐷) ⊆ (A(,)B))
Theorem	icossico 8582	Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A ≤ 𝐶 ∧ 𝐷 ≤ B)) → (𝐶[,)𝐷) ⊆ (A[,)B))
Theorem	iccss2 8583	Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐶 ∈ (A[,]B) ∧ 𝐷 ∈ (A[,]B)) → (𝐶[,]𝐷) ⊆ (A[,]B))
Theorem	iccssico 8584	Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A ≤ 𝐶 ∧ 𝐷 < B)) → (𝐶[,]𝐷) ⊆ (A[,)B))
Theorem	iccssioo2 8585	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐶 ∈ (A(,)B) ∧ 𝐷 ∈ (A(,)B)) → (𝐶[,]𝐷) ⊆ (A(,)B))
Theorem	iccssico2 8586	Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐶 ∈ (A[,)B) ∧ 𝐷 ∈ (A[,)B)) → (𝐶[,]𝐷) ⊆ (A[,)B))
Theorem	ioomax 8587	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
⊢ (-∞(,)+∞) = ℝ
Theorem	iccmax 8588	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ (-∞[,]+∞) = ℝ*
Theorem	ioopos 8589	The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
⊢ (0(,)+∞) = {x ∈ ℝ ∣ 0 < x}
Theorem	ioorp 8590	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (0(,)+∞) = ℝ+
Theorem	iooshf 8591	Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((A − B) ∈ (𝐶(,)𝐷) ↔ A ∈ ((𝐶 + B)(,)(𝐷 + B))))
Theorem	iocssre 8592	A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ) → (A(,]B) ⊆ ℝ)
Theorem	icossre 8593	A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ*) → (A[,)B) ⊆ ℝ)
Theorem	iccssre 8594	A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A[,]B) ⊆ ℝ)
Theorem	iccssxr 8595	A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
⊢ (A[,]B) ⊆ ℝ*
Theorem	iocssxr 8596	An open-below, closed-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)
⊢ (A(,]B) ⊆ ℝ*
Theorem	icossxr 8597	A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)
⊢ (A[,)B) ⊆ ℝ*
Theorem	ioossicc 8598	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
⊢ (A(,)B) ⊆ (A[,]B)
Theorem	icossicc 8599	A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)
⊢ (A[,)B) ⊆ (A[,]B)
Theorem	iocssicc 8600	A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ (A(,]B) ⊆ (A[,]B)