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	iccdifprioo 45501	An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) ∖ {𝐴, 𝐵}) = (𝐴(,)𝐵))
Theorem	ioossioobi 45502	Biconditional form of ioossioo 13463. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    ⇒   ⊢ (𝜑 → ((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵)))
Theorem	iccshift 45503*	A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})
Theorem	iccsuble 45504	An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐵 − 𝐴))
Theorem	iocopn 45505	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 45506	Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐶 ≠ 𝐴)))
Theorem	iooshift 45507*	An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝑇)(,)(𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴(,)𝐵)𝑤 = (𝑧 + 𝑇)})
Theorem	iccintsng 45508	Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) = {𝐵})
Theorem	icoiccdif 45509	Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵}))
Theorem	icoopn 45510	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 45511	A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐵 ∈ (𝐴[,)𝐵))
Theorem	eliccxrd 45512	Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
Theorem	pnfel0pnf 45513	+∞ is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ +∞ ∈ (0[,]+∞)
Theorem	eliccnelico 45514	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 45515	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 45516	A nonnegative extended real that is not +∞ is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐴 ≠ +∞) → 𝐴 ∈ ℝ)
Theorem	ge0lere 45517	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 45518*	Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦))
Theorem	inficc 45519	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 45520	The rational numbers are dense in ℝ. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((ℚ ∩ (𝐴(,)𝐵)) = ∅ ↔ 𝐵 ≤ 𝐴))
Theorem	lenelioc 45521	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 45522	A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴(,)𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	xrgtnelicc 45523	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 45524	The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶))
Theorem	iocnct 45525	A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴(,]𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	iccnct 45526	A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴[,]𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	iooiinicc 45527*	A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ ((𝐴 − (1 / 𝑛))(,)(𝐵 + (1 / 𝑛))) = (𝐴[,]𝐵))
Theorem	iccgelbd 45528	An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	iooltubd 45529	An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 < 𝐵)
Theorem	icoltubd 45530	An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 < 𝐵)
Theorem	qelioo 45531*	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 45532*	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 45533	An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐵)
Theorem	elioored 45534	A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ (𝐵(,)𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	ioogtlbd 45535	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	ioofun 45536	(,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Fun (,)
Theorem	icomnfinre 45537	A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((-∞[,)𝐴) ∩ ℝ) = (-∞(,)𝐴))
Theorem	sqrlearg 45538	The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 ↔ 𝐴 ∈ (0[,]1)))
Theorem	ressiocsup 45539	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 45540	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 45541*	A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) = (𝐴(,]𝐵))
Theorem	ressiooinf 45542	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	icogelbd 45543	An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	iocleubd 45544	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 45545	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 45546*	Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≤ 𝐵})
Theorem	uzinico2 45547	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.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (ℤ≥‘𝑁) = ((ℤ≥‘𝑀) ∩ (𝑁[,)+∞)))
Theorem	uzinico3 45548	An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → 𝑍 = (𝑍 ∩ (𝑀[,)+∞)))
Theorem	icossico2 45549	Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐴[,)𝐶) ⊆ (𝐵[,)𝐶))
Theorem	dmico 45550	The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ dom [,) = (ℝ* × ℝ*)
Theorem	ndmico 45551	The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (¬ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ∅)
Theorem	uzubioo 45552*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (𝑋(,)+∞)𝑘 ∈ 𝑍)
Theorem	uzubico 45553*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (𝑋[,)+∞)𝑘 ∈ 𝑍)
Theorem	uzubioo2 45554*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑘 ∈ (𝑥(,)+∞)𝑘 ∈ 𝑍)
Theorem	uzubico2 45555*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑘 ∈ (𝑥[,)+∞)𝑘 ∈ 𝑍)
Theorem	iocgtlbd 45556	An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrtgioo2 45557	The topology on the extended reals coincides with the standard topology on the reals, when restricted to ℝ. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t ℝ)
21.43.5  Finite sums
Theorem	fsummulc1f 45558*	Closure of a finite sum of complex numbers 𝐴(𝑘). A version of fsummulc1 15804 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶))
Theorem	fsumnncl 45559*	Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ)
Theorem	fsumge0cl 45560*	The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞))
Theorem	fsumf1of 45561*	Re-index a finite sum using a bijection. Same as fsumf1o 15742, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)
Theorem	fsumiunss 45562*	Sum over a disjoint indexed union, intersected with a finite set 𝐷. Similar to fsumiun 15840, but here 𝐴 and 𝐵 need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐷)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐷) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝐷)𝐶)
Theorem	fsumreclf 45563*	Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)
Theorem	fsumlessf 45564*	A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsumsupp0 45565*	Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝐹 supp 0)(𝐹‘𝑘) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘))
Theorem	fsumsermpt 45566*	A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ Σ𝑘 ∈ (𝑀...𝑛)𝐴)    &   ⊢ 𝐺 = seq𝑀( + , (𝑘 ∈ 𝑍 ↦ 𝐴))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.43.6  Finite multiplication of numbers and finite multiplication of functions
Theorem	fmul01 45567*	Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐵    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ 𝐴 = seq𝐿( · , 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ (𝐿...𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)    ⇒   ⊢ (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1))
Theorem	fmulcl 45568*	If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)    &   ⊢ (𝜑 → 𝑇 ∈ V)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑌)
Theorem	fmuldfeqlem1 45569*	induction step for the proof of fmuldfeq 45570. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑓𝜑    &   ⊢ Ⅎ𝑔𝜑    &   ⊢ Ⅎ𝑡𝑌    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)    &   ⊢ (𝜑 → 𝑁 ∈ (1...𝑀))    &   ⊢ (𝜑 → (𝑁 + 1) ∈ (1...𝑀))    &   ⊢ (𝜑 → ((seq1(𝑃, 𝑈)‘𝑁)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑁 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑁 + 1)))
Theorem	fmuldfeq 45570*	X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑡𝑌    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ 𝑍 = (𝑡 ∈ 𝑇 ↦ (seq1( · , (𝐹‘𝑡))‘𝑀))    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (𝑍‘𝑡))
Theorem	fmul01lt1lem1 45571*	Given a finite multiplication of values between 0 and 1, a value larger than its first element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐵    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ 𝐴 = seq𝐿( · , 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐵‘𝐿) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)
Theorem	fmul01lt1lem2 45572*	Given a finite multiplication of values between 0 and 1, a value 𝐸 larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐵    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ 𝐴 = seq𝐿( · , 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑀))    &   ⊢ (𝜑 → (𝐵‘𝐽) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)
Theorem	fmul01lt1 45573*	Given a finite multiplication of values between 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐵    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ 𝐴 = seq1( · , 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵:(1...𝑀)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ (𝐵‘𝑖))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵‘𝑖) ≤ 1)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → ∃𝑗 ∈ (1...𝑀)(𝐵‘𝑗) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)
Theorem	cncfmptss 45574*	A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ (𝐶–cn→𝐵))
Theorem	rrpsscn 45575	The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ℝ+ ⊆ ℂ
Theorem	mulc1cncfg 45576*	A version of mulc1cncf 24868 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (𝐹‘𝑥))) ∈ (𝐴–cn→ℂ))
Theorem	infrglb 45577*	The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐵 ∈ ℝ) → (inf(𝐴, ℝ, < ) < 𝐵 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝐵))
Theorem	expcnfg 45578*	If 𝐹 is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 24890. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)↑𝑁)) ∈ (𝐴–cn→ℂ))
Theorem	prodeq2ad 45579*	Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	fprodsplit1 45580*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (𝐷 · ∏𝑘 ∈ (𝐴 ∖ {𝐶})𝐵))
Theorem	fprodexp 45581*	Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵↑𝑁) = (∏𝑘 ∈ 𝐴 𝐵↑𝑁))
Theorem	fprodabs2 45582*	The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘∏𝑘 ∈ 𝐴 𝐵) = ∏𝑘 ∈ 𝐴 (abs‘𝐵))
Theorem	fprod0 45583*	A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐶    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 = 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0)
Theorem	mccllem 45584*	* Induction step for mccl 45585. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m (𝐶 ∪ {𝐷})))    &   ⊢ (𝜑 → ∀𝑏 ∈ (ℕ0 ↑m 𝐶)((!‘Σ𝑘 ∈ 𝐶 (𝑏‘𝑘)) / ∏𝑘 ∈ 𝐶 (!‘(𝑏‘𝑘))) ∈ ℕ)    ⇒   ⊢ (𝜑 → ((!‘Σ𝑘 ∈ (𝐶 ∪ {𝐷})(𝐵‘𝑘)) / ∏𝑘 ∈ (𝐶 ∪ {𝐷})(!‘(𝐵‘𝑘))) ∈ ℕ)
Theorem	mccl 45585*	A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m 𝐴))    ⇒   ⊢ (𝜑 → ((!‘Σ𝑘 ∈ 𝐴 (𝐵‘𝑘)) / ∏𝑘 ∈ 𝐴 (!‘(𝐵‘𝑘))) ∈ ℕ)
Theorem	fprodcnlem 45586*	A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.) Avoid ax-mulf 11217. (Revised by GG, 19-Apr-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ (𝐴 ∖ 𝑍))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝑍 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ (𝑍 ∪ {𝑊})𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	fprodcn 45587*	A finite product of functions to complex numbers from a common topological space is continuous. The class expression for 𝐵 normally contains free variables 𝑘 and 𝑥 to index it. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
21.43.7  Limits
Theorem	clim1fr1 45588*	A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴 · 𝑛) + 𝐵) / (𝐴 · 𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	isumneg 45589*	Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 -𝐴 = -Σ𝑘 ∈ 𝑍 𝐴)
Theorem	climrec 45590*	Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘)))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴))
Theorem	climmulf 45591*	A version of climmul 15652 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵))
Theorem	climexp 45592*	The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘)↑𝑁))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴↑𝑁))
Theorem	climinf 45593*	A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < ))
Theorem	climsuselem1 45594*	The subsequence index 𝐼 has the expected properties: it belongs to the same upper integers as the original index, and it is always greater than or equal to the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐼‘𝐾) ∈ (ℤ≥‘𝐾))
Theorem	climsuse 45595*	A subsequence 𝐺 of a converging sequence 𝐹, converges to the same limit. 𝐼 is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐼    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐹‘(𝐼‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
Theorem	climrecf 45596*	A version of climrec 45590 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘)))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴))
Theorem	climneg 45597*	Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) ⇝ -𝐴)
Theorem	climinff 45598*	A version of climinf 45593 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < ))
Theorem	climdivf 45599*	Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 / 𝐵))
Theorem	climreeq 45600	If 𝐹 is a real function, then 𝐹 converges to 𝐴 with respect to the standard topology on the reals if and only if it converges to 𝐴 with respect to the standard topology on complex numbers. In the theorem, 𝑅 is defined to be convergence w.r.t. the standard topology on the reals and then 𝐹𝑅𝐴 represents the statement "𝐹 converges to 𝐴, with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that 𝐴 is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.)
⊢ 𝑅 = (⇝𝑡‘(topGen‘ran (,)))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹𝑅𝐴 ↔ 𝐹 ⇝ 𝐴))