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	ixxssixx 8501*	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 8502*	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 8503*	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 8504*	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 8505*	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 8506	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 8507*	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 8508	An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
⊢ (A ∈ ℝ* → (A(,)A) = ∅)
Theorem	elioo3g 8509	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 8510	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 8511	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 8512	An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ A ∈ (A(,)B))
Theorem	ubioog 8513	An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ¬ B ∈ (A(,)B))
Theorem	iooval2 8514*	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 8515	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 8516	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 8517*	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 8518*	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 8519*	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 8520	Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (𝐶 ∈ (A(,)B) ↔ (𝐶 ∈ ℝ ∧ A < 𝐶 ∧ 𝐶 < B)))
Theorem	elioc1 8521	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 8522	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 8523	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 8524	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 8525	An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (B < A → (A[,]B) = ∅))
Theorem	eliooxr 8526	An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
⊢ (A ∈ (B(,)𝐶) → (B ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
Theorem	eliooord 8527	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 8528	The upper bound belongs to an open-below, closed-above interval. See ubicc2 8583. (Contributed by FL, 29-May-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → B ∈ (A(,]B))
Theorem	lbico1 8529	The lower bound belongs to a closed-below, open-above interval. See lbicc2 8582. (Contributed by FL, 29-May-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A < B) → A ∈ (A[,)B))
Theorem	iccleub 8530	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 8531	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 8532	Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (A(,)B) ↔ (A < 𝐶 ∧ 𝐶 < B)))
Theorem	elioo4g 8533	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 8534	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
⊢ (A(,)B) ⊆ ℝ
Theorem	elioc2 8535	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 8536	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 8537	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 8538	Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (𝐶 ∈ (A[,]B) ↔ (𝐶 ∈ ℝ ∧ A ≤ 𝐶 ∧ 𝐶 ≤ B))
Theorem	elicc4 8539	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 8540	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 8541	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 8542	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 8543	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 8544	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 8545	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 8546	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 8547	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
⊢ (-∞(,)+∞) = ℝ
Theorem	iccmax 8548	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ (-∞[,]+∞) = ℝ*
Theorem	ioopos 8549	The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
⊢ (0(,)+∞) = {x ∈ ℝ ∣ 0 < x}
Theorem	ioorp 8550	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (0(,)+∞) = ℝ+
Theorem	iooshf 8551	Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((A − B) ∈ (𝐶(,)𝐷) ↔ A ∈ ((𝐶 + B)(,)(𝐷 + B))))
Theorem	iocssre 8552	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 8553	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 8554	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 8555	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 8556	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 8557	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 8558	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
⊢ (A(,)B) ⊆ (A[,]B)
Theorem	icossicc 8559	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 8560	A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ (A(,]B) ⊆ (A[,]B)
Theorem	ioossico 8561	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ (A(,)B) ⊆ (A[,)B)
Theorem	iocssioo 8562	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A ≤ 𝐶 ∧ 𝐷 < B)) → (𝐶(,]𝐷) ⊆ (A(,)B))
Theorem	icossioo 8563	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A < 𝐶 ∧ 𝐷 ≤ B)) → (𝐶[,)𝐷) ⊆ (A(,)B))
Theorem	ioossioo 8564	Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
⊢ (((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (A ≤ 𝐶 ∧ 𝐷 ≤ B)) → (𝐶(,)𝐷) ⊆ (A(,)B))
Theorem	iccsupr 8565*	A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum. To be useful without excluded middle, we'll probably need to change not equal to apart, and perhaps make other changes, but the theorem does hold as stated here. (Contributed by Paul Chapman, 21-Jan-2008.)
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ 𝑆 ⊆ (A[,]B) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃x ∈ ℝ ∀y ∈ 𝑆 y ≤ x))
Theorem	elioopnf 8566	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (A ∈ ℝ* → (B ∈ (A(,)+∞) ↔ (B ∈ ℝ ∧ A < B)))
Theorem	elioomnf 8567	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (A ∈ ℝ* → (B ∈ (-∞(,)A) ↔ (B ∈ ℝ ∧ B < A)))
Theorem	elicopnf 8568	Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (A ∈ ℝ → (B ∈ (A[,)+∞) ↔ (B ∈ ℝ ∧ A ≤ B)))
Theorem	repos 8569	Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.)
⊢ (A ∈ (0(,)+∞) ↔ (A ∈ ℝ ∧ 0 < A))
Theorem	ioof 8570	The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
Theorem	iccf 8571	The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ [,]:(ℝ* × ℝ*)⟶𝒫 ℝ*
Theorem	unirnioo 8572	The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
⊢ ℝ = ∪ ran (,)
Theorem	dfioo2 8573*	Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (,) = (x ∈ ℝ*, y ∈ ℝ* ↦ {w ∈ ℝ ∣ (x < w ∧ w < y)})
Theorem	ioorebasg 8574	Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(,)B) ∈ ran (,))
Theorem	elrege0 8575	The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
⊢ (A ∈ (0[,)+∞) ↔ (A ∈ ℝ ∧ 0 ≤ A))
Theorem	rge0ssre 8576	Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
⊢ (0[,)+∞) ⊆ ℝ
Theorem	elxrge0 8577	Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (A ∈ (0[,]+∞) ↔ (A ∈ ℝ* ∧ 0 ≤ A))
Theorem	0e0icopnf 8578	0 is a member of (0[,)+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ∈ (0[,)+∞)
Theorem	0e0iccpnf 8579	0 is a member of (0[,]+∞) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ∈ (0[,]+∞)
Theorem	ge0addcl 8580	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((A ∈ (0[,)+∞) ∧ B ∈ (0[,)+∞)) → (A + B) ∈ (0[,)+∞))
Theorem	ge0mulcl 8581	The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((A ∈ (0[,)+∞) ∧ B ∈ (0[,)+∞)) → (A · B) ∈ (0[,)+∞))
Theorem	lbicc2 8582	The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A ≤ B) → A ∈ (A[,]B))
Theorem	ubicc2 8583	The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ A ≤ B) → B ∈ (A[,]B))
Theorem	0elunit 8584	Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 0 ∈ (0[,]1)
Theorem	1elunit 8585	One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 1 ∈ (0[,]1)
Theorem	iooneg 8586	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (A(,)B) ↔ -𝐶 ∈ (-B(,)-A)))
Theorem	iccneg 8587	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (A[,]B) ↔ -𝐶 ∈ (-B[,]-A)))
Theorem	icoshft 8588	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (A[,)B) → (𝑋 + 𝐶) ∈ ((A + 𝐶)[,)(B + 𝐶))))
Theorem	icoshftf1o 8589*	Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐹 = (x ∈ (A[,)B) ↦ (x + 𝐶))    ⇒   ⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐹:(A[,)B)–1-1-onto→((A + 𝐶)[,)(B + 𝐶)))
Theorem	icodisj 8590	End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((A ∈ ℝ* ∧ B ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((A[,)B) ∩ (B[,)𝐶)) = ∅)
Theorem	ioodisj 8591	If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009.)
⊢ ((((A ∈ ℝ* ∧ B ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) ∧ B ≤ 𝐶) → ((A(,)B) ∩ (𝐶(,)𝐷)) = ∅)
Theorem	iccshftr 8592	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (A + 𝑅) = 𝐶    &   ⊢ (B + 𝑅) = 𝐷    ⇒   ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (A[,]B) ↔ (𝑋 + 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccshftri 8593	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (A + 𝑅) = 𝐶    &   ⊢ (B + 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (A[,]B) → (𝑋 + 𝑅) ∈ (𝐶[,]𝐷))
Theorem	iccshftl 8594	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (A − 𝑅) = 𝐶    &   ⊢ (B − 𝑅) = 𝐷    ⇒   ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → (𝑋 ∈ (A[,]B) ↔ (𝑋 − 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccshftli 8595	Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (A − 𝑅) = 𝐶    &   ⊢ (B − 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (A[,]B) → (𝑋 − 𝑅) ∈ (𝐶[,]𝐷))
Theorem	iccdil 8596	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (A · 𝑅) = 𝐶    &   ⊢ (B · 𝑅) = 𝐷    ⇒   ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (A[,]B) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	iccdili 8597	Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ+    &   ⊢ (A · 𝑅) = 𝐶    &   ⊢ (B · 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (A[,]B) → (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))
Theorem	icccntr 8598	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (A / 𝑅) = 𝐶    &   ⊢ (B / 𝑅) = 𝐷    ⇒   ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)) → (𝑋 ∈ (A[,]B) ↔ (𝑋 / 𝑅) ∈ (𝐶[,]𝐷)))
Theorem	icccntri 8599	Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    &   ⊢ 𝑅 ∈ ℝ+    &   ⊢ (A / 𝑅) = 𝐶    &   ⊢ (B / 𝑅) = 𝐷    ⇒   ⊢ (𝑋 ∈ (A[,]B) → (𝑋 / 𝑅) ∈ (𝐶[,]𝐷))
Theorem	divelunit 8600	A condition for a ratio to be a member of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 < B)) → ((A / B) ∈ (0[,]1) ↔ A ≤ B))