P. 134 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ndmioo 13301	The open interval function's value is empty outside of its domain. (Contributed by NM, 21-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (¬ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = ∅)
Theorem	iooid 13302	An open interval with identical lower and upper bounds is empty. (Contributed by NM, 21-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝐴(,)𝐴) = ∅
Theorem	elioo3g 13303	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 𝐴 ∈ ℝ* and 𝐵 ∈ ℝ*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	elioore 13304	A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)
Theorem	lbioo 13305	An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ ¬ 𝐴 ∈ (𝐴(,)𝐵)
Theorem	ubioo 13306	An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ ¬ 𝐵 ∈ (𝐴(,)𝐵)
Theorem	iooval2 13307*	Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
Theorem	iooin 13308	Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) = (if(𝐴 ≤ 𝐶, 𝐶, 𝐴)(,)if(𝐵 ≤ 𝐷, 𝐵, 𝐷)))
Theorem	iooss1 13309	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐵(,)𝐶) ⊆ (𝐴(,)𝐶))
Theorem	iooss2 13310	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶) → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐶))
Theorem	iocval 13311*	Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵)})
Theorem	icoval 13312*	Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵)})
Theorem	iccval 13313*	Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,]𝐵) = {𝑥 ∈ ℝ* ∣ (𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)})
Theorem	elioo1 13314	Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	elioo2 13315	Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	elioc1 13316	Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
Theorem	elico1 13317	Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	elicc1 13318	Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
Theorem	iccid 13319	A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.)
⊢ (𝐴 ∈ ℝ* → (𝐴[,]𝐴) = {𝐴})
Theorem	ico0 13320	An empty open interval of extended reals. (Contributed by FL, 30-May-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
Theorem	ioc0 13321	An empty open interval of extended reals. (Contributed by FL, 30-May-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴(,]𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
Theorem	icc0 13322	An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
Theorem	dfrp2 13323	Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.)
⊢ ℝ+ = (0(,)+∞)
Theorem	elicod 13324	Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))
Theorem	icogelb 13325	An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶)
Theorem	elicore 13326	A member of a left-closed right-open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 ∈ ℝ)
Theorem	ubioc1 13327	The upper bound belongs to an open-below, closed-above interval. See ubicc2 13392. (Contributed by FL, 29-May-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
Theorem	lbico1 13328	The lower bound belongs to a closed-below, open-above interval. See lbicc2 13391. (Contributed by FL, 29-May-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐴 ∈ (𝐴[,)𝐵))
Theorem	iccleub 13329	An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵)
Theorem	iccgelb 13330	An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶)
Theorem	elioo5 13331	Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	eliooxr 13332	A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
Theorem	eliooord 13333	Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
Theorem	elioo4g 13334	Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐶 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	ioossre 13335	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
⊢ (𝐴(,)𝐵) ⊆ ℝ
Theorem	ioosscn 13336	An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴(,)𝐵) ⊆ ℂ
Theorem	elioc2 13337	Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝐵)))
Theorem	elico2 13338	Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
Theorem	elicc2 13339	Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
Theorem	elicc2i 13340	Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
Theorem	elicc4 13341	Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)))
Theorem	iccss 13342	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.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,]𝐵))
Theorem	iccssioo 13343	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵))
Theorem	icossico 13344	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.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴[,)𝐵))
Theorem	iccss2 13345	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.)
⊢ ((𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐷 ∈ (𝐴[,]𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,]𝐵))
Theorem	iccssico 13346	Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵))
Theorem	iccssioo2 13347	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐶 ∈ (𝐴(,)𝐵) ∧ 𝐷 ∈ (𝐴(,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴(,)𝐵))
Theorem	iccssico2 13348	Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
⊢ ((𝐶 ∈ (𝐴[,)𝐵) ∧ 𝐷 ∈ (𝐴[,)𝐵)) → (𝐶[,]𝐷) ⊆ (𝐴[,)𝐵))
Theorem	ioomax 13349	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
⊢ (-∞(,)+∞) = ℝ
Theorem	iccmax 13350	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ (-∞[,]+∞) = ℝ*
Theorem	ioopos 13351	The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
⊢ (0(,)+∞) = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
Theorem	ioorp 13352	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (0(,)+∞) = ℝ+
Theorem	iooshf 13353	Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐵) ∈ (𝐶(,)𝐷) ↔ 𝐴 ∈ ((𝐶 + 𝐵)(,)(𝐷 + 𝐵))))
Theorem	iocssre 13354	A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
Theorem	icossre 13355	A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ⊆ ℝ)
Theorem	iccssre 13356	A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
Theorem	iccssxr 13357	A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
⊢ (𝐴[,]𝐵) ⊆ ℝ*
Theorem	iocssxr 13358	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.)
⊢ (𝐴(,]𝐵) ⊆ ℝ*
Theorem	icossxr 13359	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.)
⊢ (𝐴[,)𝐵) ⊆ ℝ*
Theorem	ioossicc 13360	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
Theorem	iccssred 13361	A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
Theorem	eliccxr 13362	A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*)
Theorem	icossicc 13363	A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)
⊢ (𝐴[,)𝐵) ⊆ (𝐴[,]𝐵)
Theorem	iocssicc 13364	A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ (𝐴(,]𝐵) ⊆ (𝐴[,]𝐵)
Theorem	ioossico 13365	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,)𝐵)
Theorem	iocssioo 13366	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 < 𝐵)) → (𝐶(,]𝐷) ⊆ (𝐴(,)𝐵))
Theorem	icossioo 13367	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶[,)𝐷) ⊆ (𝐴(,)𝐵))
Theorem	ioossioo 13368	Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)) → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))
Theorem	iccsupr 13369*	A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 12124). (Contributed by Paul Chapman, 21-Jan-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑆 ⊆ (𝐴[,]𝐵) ∧ 𝐶 ∈ 𝑆) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))
Theorem	elioopnf 13370	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (𝐴(,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)))
Theorem	elioomnf 13371	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 ∈ ℝ* → (𝐵 ∈ (-∞(,)𝐴) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 𝐴)))
Theorem	elicopnf 13372	Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)))
Theorem	repos 13373	Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.)
⊢ (𝐴 ∈ (0(,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Theorem	ioof 13374	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 13375	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 13376	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 13377*	Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑤 ∈ ℝ ∣ (𝑥 < 𝑤 ∧ 𝑤 < 𝑦)})
Theorem	ioorebas 13378	Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝐴(,)𝐵) ∈ ran (,)
Theorem	xrge0neqmnf 13379	A nonnegative extended real is not equal to minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017.) (Proof shortened by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ (0[,]+∞) → 𝐴 ≠ -∞)
Theorem	xrge0nre 13380	An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ ¬ 𝐴 ∈ ℝ) → 𝐴 = +∞)
Theorem	elrege0 13381	The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
Theorem	nn0rp0 13382	A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.)
⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0[,)+∞))
Theorem	rge0ssre 13383	Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
⊢ (0[,)+∞) ⊆ ℝ
Theorem	elxrge0 13384	Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))
Theorem	0e0icopnf 13385	0 is a member of (0[,)+∞). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ∈ (0[,)+∞)
Theorem	0e0iccpnf 13386	0 is a member of (0[,]+∞). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ∈ (0[,]+∞)
Theorem	ge0addcl 13387	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 + 𝐵) ∈ (0[,)+∞))
Theorem	ge0mulcl 13388	The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐴 ∈ (0[,)+∞) ∧ 𝐵 ∈ (0[,)+∞)) → (𝐴 · 𝐵) ∈ (0[,)+∞))
Theorem	ge0xaddcl 13389	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞))
Theorem	ge0xmulcl 13390	The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴 ·e 𝐵) ∈ (0[,]+∞))
Theorem	lbicc2 13391	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.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
Theorem	ubicc2 13392	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.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
Theorem	elicc01 13393	Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022.)
⊢ (𝑋 ∈ (0[,]1) ↔ (𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ 1))
Theorem	elunitrn 13394	The closed unit interval is a subset of the set of the real numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.)
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℝ)
Theorem	elunitcn 13395	The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.)
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℂ)
Theorem	0elunit 13396	Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 0 ∈ (0[,]1)
Theorem	1elunit 13397	One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ 1 ∈ (0[,]1)
Theorem	iooneg 13398	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴(,)𝐵) ↔ -𝐶 ∈ (-𝐵(,)-𝐴)))
Theorem	iccneg 13399	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ -𝐶 ∈ (-𝐵[,]-𝐴)))
Theorem	icoshft 13400	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝑋 ∈ (𝐴[,)𝐵) → (𝑋 + 𝐶) ∈ ((𝐴 + 𝐶)[,)(𝐵 + 𝐶))))