P. 456 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45501-45600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	supminfxr 45501*	The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = -𝑒inf({𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}, ℝ*, < ))
Theorem	infrpgernmpt 45502*	The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐵 ≤ (inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) +𝑒 𝐶))
Theorem	xnegre 45503	An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ -𝑒𝐴 ∈ ℝ))
Theorem	xnegrecl2d 45504	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	uzxr 45505	An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐴 ∈ (ℤ≥‘𝑀) → 𝐴 ∈ ℝ*)
Theorem	supminfxr2 45506*	The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = -𝑒inf({𝑥 ∈ ℝ* ∣ -𝑒𝑥 ∈ 𝐴}, ℝ*, < ))
Theorem	xnegred 45507	An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ↔ -𝑒𝐴 ∈ ℝ))
Theorem	supminfxrrnmpt 45508*	The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -𝑒inf(ran (𝑥 ∈ 𝐴 ↦ -𝑒𝐵), ℝ*, < ))
Theorem	min1d 45509	The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	min2d 45510	The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	xrnpnfmnf 45511	An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ +∞)    ⇒   ⊢ (𝜑 → 𝐴 = -∞)
Theorem	uzsscn 45512	An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (ℤ≥‘𝑀) ⊆ ℂ
Theorem	absimnre 45513	The absolute value of the imaginary part of a non-real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘(ℑ‘𝐴)) ∈ ℝ+)
Theorem	uzsscn2 45514	An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ 𝑍 ⊆ ℂ
Theorem	xrtgcntopre 45515	The standard topologies on the extended reals and on the complex numbers, coincide when restricted to the reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ((ordTop‘ ≤ ) ↾t ℝ) = ((TopOpen‘ℂfld) ↾t ℝ)
Theorem	absimlere 45516	The absolute value of the imaginary part of a complex number is a lower bound of the distance to any real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘(ℑ‘𝐴)) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	rpssxr 45517	The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ℝ+ ⊆ ℝ*
Theorem	monoordxrv 45518*	Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁))
Theorem	monoordxr 45519*	Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁))
Theorem	monoord2xrv 45520*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	monoord2xr 45521*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀))
Theorem	xrpnf 45522*	An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴))
Theorem	xlenegcon1 45523	Extended real version of lenegcon1 11618. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ 𝐴))
Theorem	xlenegcon2 45524	Extended real version of lenegcon2 11619. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ -𝑒𝐵 ↔ 𝐵 ≤ -𝑒𝐴))
Theorem	pimxrneun 45525	The preimage of a set of extended reals that does not contain a value 𝐶 is the union of the preimage of the elements smaller than 𝐶 and the preimage of the subset of elements larger than 𝐶. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶} = ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}))
Theorem	caucvgbf 45526*	A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑗𝐹    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉) → (𝐹 ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))
Theorem	cvgcau 45527*	A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑗𝐹    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑋))
Theorem	cvgcaule 45528*	A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑗𝐹    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) ≤ 𝑋))
Theorem	rexanuz2nf 45529*	A simple counterexample related to theorem rexanuz2 15254, demonstrating the necessity of its disjoint variable constraints. Here, 𝑗 appears free in 𝜑, showing that without these constraints, rexanuz2 15254 and similar theorems would not hold (see rexanre 15251 and rexanuz 15250). (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ 𝑍 = ℕ0    &   ⊢ (𝜑 ↔ (𝑗 = 0 ∧ 𝑗 ≤ 𝑘))    &   ⊢ (𝜓 ↔ 0 < 𝑘)    ⇒   ⊢ ¬ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
21.43.4  Real intervals
Theorem	gtnelioc 45530	A real number larger than the upper bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴(,]𝐵))
Theorem	ioossioc 45531	An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵)
Theorem	ioondisj2 45532	A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅)
Theorem	ioondisj1 45533	A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅)
Theorem	ioogtlb 45534	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝐶)
Theorem	evthiccabs 45535*	Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑤))))
Theorem	ltnelicc 45536	A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 < 𝐴)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵))
Theorem	eliood 45537	Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐶)    &   ⊢ (𝜑 → 𝐶 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))
Theorem	iooabslt 45538	An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − 𝐵)(,)(𝐴 + 𝐵)))    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < 𝐵)
Theorem	gtnelicc 45539	A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵))
Theorem	iooinlbub 45540	An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅
Theorem	iocgtlb 45541	An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐶)
Theorem	iocleub 45542	An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ≤ 𝐵)
Theorem	eliccd 45543	Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
Theorem	eliccre 45544	A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
Theorem	eliooshift 45545	Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)(,)(𝐶 + 𝐷))))
Theorem	eliocd 45546	Membership in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐶)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))
Theorem	icoltub 45547	An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵)
Theorem	eliocre 45548	A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ∈ ℝ)
Theorem	iooltub 45549	An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵)
Theorem	ioontr 45550	The interior of an interval in the standard topology on ℝ is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
Theorem	snunioo1 45551	The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵))
Theorem	lbioc 45552	A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ¬ 𝐴 ∈ (𝐴(,]𝐵)
Theorem	ioomidp 45553	The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
Theorem	iccdifioo 45554	If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,]𝐵) ∖ (𝐴(,)𝐵)) = {𝐴, 𝐵})
Theorem	iccdifprioo 45555	An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) ∖ {𝐴, 𝐵}) = (𝐴(,)𝐵))
Theorem	ioossioobi 45556	Biconditional form of ioossioo 13338. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → ((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)))
Theorem	iccshift 45557*	A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})
Theorem	iccsuble 45558	An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐵 − 𝐴))
Theorem	iocopn 45559	A left-open right-closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝐽 = (𝐾 ↾t (𝐴(,]𝐵))    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐶(,]𝐵) ∈ 𝐽)
Theorem	eliccelioc 45560	Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐶 ≠ 𝐴)))
Theorem	iooshift 45561*	An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝑇)(,)(𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴(,)𝐵)𝑤 = (𝑧 + 𝑇)})
Theorem	iccintsng 45562	Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) = {𝐵})
Theorem	icoiccdif 45563	Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵}))
Theorem	icoopn 45564	A left-closed right-open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝐽 = (𝐾 ↾t (𝐴[,)𝐵))    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴[,)𝐶) ∈ 𝐽)
Theorem	icoub 45565	A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐵 ∈ (𝐴[,)𝐵))
Theorem	eliccxrd 45566	Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
Theorem	pnfel0pnf 45567	+∞ is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ +∞ ∈ (0[,]+∞)
Theorem	eliccnelico 45568	An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 = 𝐵)
Theorem	eliccelicod 45569	A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐶 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))
Theorem	ge0xrre 45570	A nonnegative extended real that is not +∞ is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐴 ≠ +∞) → 𝐴 ∈ ℝ)
Theorem	ge0lere 45571	A nonnegative extended Real number smaller than or equal to a Real number, is a Real number. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ℝ)
Theorem	elicores 45572*	Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦))
Theorem	inficc 45573	The infimum of a nonempty set, included in a closed interval, is a member of the interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑆 ≠ ∅)    ⇒   ⊢ (𝜑 → inf(𝑆, ℝ*, < ) ∈ (𝐴[,]𝐵))
Theorem	qinioo 45574	The rational numbers are dense in ℝ. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((ℚ ∩ (𝐴(,)𝐵)) = ∅ ↔ 𝐵 ≤ 𝐴))
Theorem	lenelioc 45575	A real number smaller than or equal to the lower bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴(,]𝐵))
Theorem	ioonct 45576	A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴(,)𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	xrgtnelicc 45577	A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵))
Theorem	iccdificc 45578	The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶))
Theorem	iocnct 45579	A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴(,]𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	iccnct 45580	A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴[,]𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	iooiinicc 45581*	A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ ((𝐴 − (1 / 𝑛))(,)(𝐵 + (1 / 𝑛))) = (𝐴[,]𝐵))
Theorem	iccgelbd 45582	An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	iooltubd 45583	An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 < 𝐵)
Theorem	icoltubd 45584	An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 < 𝐵)
Theorem	qelioo 45585*	The rational numbers are dense in ℝ*: any two extended real numbers have a rational between them. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℚ 𝑥 ∈ (𝐴(,)𝐵))
Theorem	tgqioo2 45586*	Every open set of reals is the (countable) union of open interval with rational bounds. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    ⇒   ⊢ (𝜑 → ∃𝑞(𝑞 ⊆ ((,) “ (ℚ × ℚ)) ∧ 𝐴 = ∪ 𝑞))
Theorem	iccleubd 45587	An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐵)
Theorem	elioored 45588	A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ (𝐵(,)𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	ioogtlbd 45589	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	ioofun 45590	(,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Fun (,)
Theorem	icomnfinre 45591	A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((-∞[,)𝐴) ∩ ℝ) = (-∞(,)𝐴))
Theorem	sqrlearg 45592	The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 ↔ 𝐴 ∈ (0[,]1)))
Theorem	ressiocsup 45593	If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑆 = sup(𝐴, ℝ*, < )    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    &   ⊢ 𝐼 = (-∞(,]𝑆)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)
Theorem	ressioosup 45594	If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑆 = sup(𝐴, ℝ*, < )    &   ⊢ (𝜑 → ¬ 𝑆 ∈ 𝐴)    &   ⊢ 𝐼 = (-∞(,)𝑆)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)
Theorem	iooiinioc 45595*	A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) = (𝐴(,]𝐵))
Theorem	ressiooinf 45596	If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑆 = inf(𝐴, ℝ*, < )    &   ⊢ (𝜑 → ¬ 𝑆 ∈ 𝐴)    &   ⊢ 𝐼 = (𝑆(,)+∞)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)
Theorem	iocleubd 45597	An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐵)
Theorem	uzinico 45598	An upper interval of integers is the intersection of the integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑍 = (ℤ ∩ (𝑀[,)+∞)))
Theorem	preimaiocmnf 45599*	Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≤ 𝐵})
Theorem	uzinico2 45600	An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) = ((ℤ≥‘𝑀) ∩ (𝑁[,)+∞)))