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	iccsuble 45501	An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐵 − 𝐴))
Theorem	iocopn 45502	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 45503	Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐶 ≠ 𝐴)))
Theorem	iooshift 45504*	An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝑇)(,)(𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴(,)𝐵)𝑤 = (𝑧 + 𝑇)})
Theorem	iccintsng 45505	Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) = {𝐵})
Theorem	icoiccdif 45506	Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵}))
Theorem	icoopn 45507	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 45508	A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ ℝ* → ¬ 𝐵 ∈ (𝐴[,)𝐵))
Theorem	eliccxrd 45509	Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))
Theorem	pnfel0pnf 45510	+∞ is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ +∞ ∈ (0[,]+∞)
Theorem	eliccnelico 45511	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 45512	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 45513	A nonnegative extended real that is not +∞ is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐴 ≠ +∞) → 𝐴 ∈ ℝ)
Theorem	ge0lere 45514	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 45515*	Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦))
Theorem	inficc 45516	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 45517	The rational numbers are dense in ℝ. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((ℚ ∩ (𝐴(,)𝐵)) = ∅ ↔ 𝐵 ≤ 𝐴))
Theorem	lenelioc 45518	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 45519	A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴(,)𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	xrgtnelicc 45520	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 45521	The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐴[,]𝐶) ∖ (𝐴[,]𝐵)) = (𝐵(,]𝐶))
Theorem	iocnct 45522	A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴(,]𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	iccnct 45523	A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐶 = (𝐴[,]𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ≼ ω)
Theorem	iooiinicc 45524*	A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ ((𝐴 − (1 / 𝑛))(,)(𝐵 + (1 / 𝑛))) = (𝐴[,]𝐵))
Theorem	iccgelbd 45525	An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐶)
Theorem	iooltubd 45526	An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 < 𝐵)
Theorem	icoltubd 45527	An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵))    ⇒   ⊢ (𝜑 → 𝐶 < 𝐵)
Theorem	qelioo 45528*	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 45529*	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 45530	An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝐵)
Theorem	elioored 45531	A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ (𝐵(,)𝐶))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	ioogtlbd 45532	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	ioofun 45533	(,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Fun (,)
Theorem	icomnfinre 45534	A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((-∞[,)𝐴) ∩ ℝ) = (-∞(,)𝐴))
Theorem	sqrlearg 45535	The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 ↔ 𝐴 ∈ (0[,]1)))
Theorem	ressiocsup 45536	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 45537	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 45538*	A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐴(,)(𝐵 + (1 / 𝑛))) = (𝐴(,]𝐵))
Theorem	ressiooinf 45539	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 45540	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 45541	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 45542*	Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (-∞(,]𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≤ 𝐵})
Theorem	uzinico2 45543	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 45544	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	dmico 45545	The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ dom [,) = (ℝ* × ℝ*)
Theorem	ndmico 45546	The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (¬ (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ∅)
Theorem	uzubioo 45547*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (𝑋(,)+∞)𝑘 ∈ 𝑍)
Theorem	uzubico 45548*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (𝑋[,)+∞)𝑘 ∈ 𝑍)
Theorem	uzubioo2 45549*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑘 ∈ (𝑥(,)+∞)𝑘 ∈ 𝑍)
Theorem	uzubico2 45550*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑘 ∈ (𝑥[,)+∞)𝑘 ∈ 𝑍)
Theorem	iocgtlbd 45551	An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵))    ⇒   ⊢ (𝜑 → 𝐴 < 𝐶)
Theorem	xrtgioo2 45552	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 45553*	Closure of a finite sum of complex numbers 𝐴(𝑘). A version of fsummulc1 15710 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐵 · 𝐶) = Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶))
Theorem	fsumnncl 45554*	Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℕ)
Theorem	fsumge0cl 45555*	The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞))
Theorem	fsumf1of 45556*	Re-index a finite sum using a bijection. Same as fsumf1o 15648, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)
Theorem	fsumiunss 45557*	Sum over a disjoint indexed union, intersected with a finite set 𝐷. Similar to fsumiun 15746, but here 𝐴 and 𝐵 need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐷)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐷) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝐷)𝐶)
Theorem	fsumreclf 45558*	Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ)
Theorem	fsumlessf 45559*	A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐶 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	fsumsupp0 45560*	Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ (𝐹 supp 0)(𝐹‘𝑘) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘))
Theorem	fsumsermpt 45561*	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 45562*	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 45563*	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 45564*	induction step for the proof of fmuldfeq 45565. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑓𝜑    &   ⊢ Ⅎ𝑔𝜑    &   ⊢ Ⅎ𝑡𝑌    &   ⊢ 𝑃 = (𝑓 ∈ 𝑌, 𝑔 ∈ 𝑌 ↦ (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))))    &   ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈‘𝑖)‘𝑡)))    &   ⊢ (𝜑 → 𝑇 ∈ V)    &   ⊢ (𝜑 → 𝑈:(1...𝑀)⟶𝑌)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝑌)    &   ⊢ (𝜑 → 𝑁 ∈ (1...𝑀))    &   ⊢ (𝜑 → (𝑁 + 1) ∈ (1...𝑀))    &   ⊢ (𝜑 → ((seq1(𝑃, 𝑈)‘𝑁)‘𝑡) = (seq1( · , (𝐹‘𝑡))‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑌) → 𝑓:𝑇⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((seq1(𝑃, 𝑈)‘(𝑁 + 1))‘𝑡) = (seq1( · , (𝐹‘𝑡))‘(𝑁 + 1)))
Theorem	fmuldfeq 45565*	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 45566*	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 45567*	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 45568*	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 45569*	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 45570	The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ℝ+ ⊆ ℂ
Theorem	mulc1cncfg 45571*	A version of mulc1cncf 24814 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (𝐹‘𝑥))) ∈ (𝐴–cn→ℂ))
Theorem	infrglb 45572*	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 45573*	If 𝐹 is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 24836. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)↑𝑁)) ∈ (𝐴–cn→ℂ))
Theorem	prodeq2ad 45574*	Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	fprodsplit1 45575*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (𝐷 · ∏𝑘 ∈ (𝐴 ∖ {𝐶})𝐵))
Theorem	fprodexp 45576*	Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵↑𝑁) = (∏𝑘 ∈ 𝐴 𝐵↑𝑁))
Theorem	fprodabs2 45577*	The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘∏𝑘 ∈ 𝐴 𝐵) = ∏𝑘 ∈ 𝐴 (abs‘𝐵))
Theorem	fprod0 45578*	A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐶    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 = 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0)
Theorem	mccllem 45579*	* Induction step for mccl 45580. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m (𝐶 ∪ {𝐷})))    &   ⊢ (𝜑 → ∀𝑏 ∈ (ℕ0 ↑m 𝐶)((!‘Σ𝑘 ∈ 𝐶 (𝑏‘𝑘)) / ∏𝑘 ∈ 𝐶 (!‘(𝑏‘𝑘))) ∈ ℕ)    ⇒   ⊢ (𝜑 → ((!‘Σ𝑘 ∈ (𝐶 ∪ {𝐷})(𝐵‘𝑘)) / ∏𝑘 ∈ (𝐶 ∪ {𝐷})(!‘(𝐵‘𝑘))) ∈ ℕ)
Theorem	mccl 45580*	A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m 𝐴))    ⇒   ⊢ (𝜑 → ((!‘Σ𝑘 ∈ 𝐴 (𝐵‘𝑘)) / ∏𝑘 ∈ 𝐴 (!‘(𝐵‘𝑘))) ∈ ℕ)
Theorem	fprodcnlem 45581*	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 11108. (Revised by GG, 19-Apr-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ (𝐴 ∖ 𝑍))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝑍 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ (𝑍 ∪ {𝑊})𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	fprodcn 45582*	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 45583*	A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴 · 𝑛) + 𝐵) / (𝐴 · 𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	isumneg 45584*	Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 -𝐴 = -Σ𝑘 ∈ 𝑍 𝐴)
Theorem	climrec 45585*	Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘)))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴))
Theorem	climmulf 45586*	A version of climmul 15558 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵))
Theorem	climexp 45587*	The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘)↑𝑁))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴↑𝑁))
Theorem	climinf 45588*	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 45589*	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 45590*	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 45591*	A version of climrec 45585 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘)))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴))
Theorem	climneg 45592*	Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) ⇝ -𝐴)
Theorem	climinff 45593*	A version of climinf 45588 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 45594*	Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 / 𝐵))
Theorem	climreeq 45595	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 (,)))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹𝑅𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	ellimciota 45596*	An explicit value for the limit, when the limit exists at a limit point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    &   ⊢ (𝜑 → (𝐹 limℂ 𝐵) ≠ ∅)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → (℩𝑥𝑥 ∈ (𝐹 limℂ 𝐵)) ∈ (𝐹 limℂ 𝐵))
Theorem	climaddf 45597*	A version of climadd 15557 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 + 𝐵))
Theorem	mullimc 45598*	Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐻 limℂ 𝐷))
Theorem	ellimcabssub0 45599*	An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶))    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ 0 ∈ (𝐺 limℂ 𝐷)))
Theorem	limcdm0 45600	If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:∅⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ℂ)