P. 457 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45601-45700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	constlimc 45601*	Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐶))
Theorem	rexlim2d 45602*	Inference removing two restricted quantifiers. Same as rexlimdvv 3197, but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
Theorem	idlimc 45603*	Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋))
Theorem	divcnvg 45604*	The sequence of reciprocals of positive integers, multiplied by the factor 𝐴, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑛 ∈ (ℤ≥‘𝑀) ↦ (𝐴 / 𝑛)) ⇝ 0)
Theorem	limcperiod 45605*	If 𝐹 is a periodic function with period 𝑇, the limit doesn't change if we shift the limiting point by 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)}    &   ⊢ (𝜑 → 𝐵 ⊆ dom 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))    &   ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝐷 + 𝑇)))
Theorem	limcrecl 45606	If 𝐹 is a real-valued function, 𝐵 is a limit point of its domain, and the limit of 𝐹 at 𝐵 exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐿 ∈ ℝ)
Theorem	sumnnodd 45607*	A series indexed by ℕ with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℕ⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0)    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵)    ⇒   ⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1))))
Theorem	lptioo2 45608	The upper bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)))
Theorem	lptioo1 45609	The lower bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)))
Theorem	elprn1 45610	A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐵) → 𝐴 = 𝐶)
Theorem	elprn2 45611	A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐶) → 𝐴 = 𝐵)
Theorem	limcmptdm 45612*	The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ℂ)
Theorem	clim2f 45613*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15508. Similar to clim2 15518, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	limcicciooub 45614	The limit of a function at the upper bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐹 limℂ 𝐵))
Theorem	ltmod 45615	A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,)𝐴))    ⇒   ⊢ (𝜑 → (𝐶 mod 𝐵) < (𝐴 mod 𝐵))
Theorem	islpcn 45616*	A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑃 ∈ ((limPt‘(TopOpen‘ℂfld))‘𝑆) ↔ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒))
Theorem	lptre2pt 45617*	If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → ((limPt‘𝐽)‘𝐴) ≠ ∅)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (abs‘(𝑥 − 𝑦)) < 𝐸))
Theorem	limsupre 45618*	If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → sup(𝐵, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ)    &   ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)
Theorem	limcresiooub 45619	The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶))
Theorem	limcresioolb 45620	The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ≤ 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵))
Theorem	limcleqr 45621	If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐿 = 𝑅)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))
Theorem	lptioo2cn 45622	The upper bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)))
Theorem	lptioo1cn 45623	The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵)))
Theorem	neglimc 45624*	Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷))    ⇒   ⊢ (𝜑 → -𝐶 ∈ (𝐺 limℂ 𝐷))
Theorem	addlimc 45625*	Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 limℂ 𝐷))
Theorem	0ellimcdiv 45626*	If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))    &   ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ (𝐺 limℂ 𝐸))    &   ⊢ (𝜑 → 𝐷 ≠ 0)    ⇒   ⊢ (𝜑 → 0 ∈ (𝐻 limℂ 𝐸))
Theorem	clim2cf 45627*	Express the predicate 𝐹 converges to 𝐴. Similar to clim2 15518, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	limclner 45628	For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))    &   ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐿 ≠ 𝑅)    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅)
Theorem	sublimc 45629*	Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝐸 − 𝐼) ∈ (𝐻 limℂ 𝐷))
Theorem	reclimc 45630*	Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖ {0}))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷))
Theorem	clim0cf 45631*	Express the predicate 𝐹 converges to 0. Similar to clim 15508, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥))
Theorem	limclr 45632	For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))    &   ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))    ⇒   ⊢ (𝜑 → (((𝐹 limℂ 𝐵) ≠ ∅ ↔ 𝐿 = 𝑅) ∧ (𝐿 = 𝑅 → 𝐿 ∈ (𝐹 limℂ 𝐵))))
Theorem	divlimc 45633*	Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷))    &   ⊢ (𝜑 → 𝑌 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋 / 𝑌) ∈ (𝐻 limℂ 𝐷))
Theorem	expfac 45634*	Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0)
Theorem	climconstmpt 45635*	A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐴)
Theorem	climresmpt 45636*	A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ 𝐺 = (𝑥 ∈ (ℤ≥‘𝑁) ↦ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵))
Theorem	climsubmpt 45637*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐷))
Theorem	climsubc2mpt 45638*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐵))
Theorem	climsubc1mpt 45639*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐴 − 𝐶))
Theorem	fnlimfv 45640*	The value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))))
Theorem	climreclf 45641*	The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	climeldmeq 45642*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ))
Theorem	climf2 45643*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 15508, but without the disjoint var constraint 𝜑𝑘 and 𝐹𝑘. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	fnlimcnv 45644*	The sequence of function values converges to the value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ (𝐺‘𝑋))
Theorem	climeldmeqmpt 45645*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ ))
Theorem	climfveq 45646*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺))
Theorem	clim2f2 45647*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15508. Similar to clim2 15518, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	climfveqmpt 45648*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷)))
Theorem	climd 45649*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋))
Theorem	clim2d 45650*	The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋))
Theorem	fnlimfvre 45651*	The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ)
Theorem	allbutfifvre 45652*	Given a sequence of real-valued functions, and 𝑋 that belongs to all but finitely many domains, then its function value is ultimately a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)    &   ⊢ 𝐷 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)((𝐹‘𝑚)‘𝑋) ∈ ℝ)
Theorem	climleltrp 45653*	The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
Theorem	fnlimfvre2 45654*	The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) ∈ ℝ)
Theorem	fnlimf 45655*	The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺:𝐷⟶ℝ)
Theorem	fnlimabslt 45656*	A sequence of function values, approximates the corresponding limit function value, all but finitely many times. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)(((𝐹‘𝑚)‘𝑋) ∈ ℝ ∧ (abs‘(((𝐹‘𝑚)‘𝑋) − (𝐺‘𝑋))) < 𝑌))
Theorem	climfveqf 45657*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺))
Theorem	climmptf 45658*	Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climfveqmpt3 45659*	Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt 45648 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷)))
Theorem	climeldmeqf 45660*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ ))
Theorem	climreclmpt 45661*	The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ℝ)
Theorem	limsupref 45662*	If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)
Theorem	limsupbnd1f 45663*	If a sequence is eventually at most 𝐴, then the limsup is also at most 𝐴. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) ≤ 𝐴)
Theorem	climbddf 45664*	A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ≤ 𝑥)
Theorem	climeqf 45665*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climeldmeqmpt3 45666*	Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt 45645 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ ))
Theorem	limsupcld 45667	Closure of the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ*)
Theorem	climfv 45668	The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐹 ⇝ 𝐴 → 𝐴 = ( ⇝ ‘𝐹))
Theorem	limsupval3 45669*	The superior limit of an infinite sequence 𝐹 of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup((𝐹 “ (𝑘[,)+∞)), ℝ*, < ))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < ))
Theorem	climfveqmpt2 45670*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐶)) = ( ⇝ ‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
Theorem	limsup0 45671	The superior limit of the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (lim sup‘∅) = -∞
Theorem	climeldmeqmpt2 45672*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐵 ↦ 𝐶) ∈ dom ⇝ ))
Theorem	limsupresre 45673	The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim sup‘(𝐹 ↾ ℝ)) = (lim sup‘𝐹))
Theorem	climeqmpt 45674*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝ 𝐷 ↔ (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝ 𝐷))
Theorem	climfvd 45675	The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = ( ⇝ ‘𝐹))
Theorem	limsuplesup 45676	An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) ≤ sup(((𝐹 “ (𝐾[,)+∞)) ∩ ℝ*), ℝ*, < ))
Theorem	limsupresico 45677	The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ 𝑍 = (𝑀[,)+∞)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹))
Theorem	limsuppnfdlem 45678*	If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))    &   ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = +∞)
Theorem	limsuppnfd 45679*	If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = +∞)
Theorem	limsupresuz 45680	If the real part of the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → dom (𝐹 ↾ ℝ) ⊆ ℤ)    ⇒   ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹))
Theorem	limsupub 45681*	If the limsup is not +∞, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))
Theorem	limsupres 45682	The superior limit of a restriction is less than or equal to the original superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝐶)) ≤ (lim sup‘𝐹))
Theorem	climinf2lem 45683*	A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < ))
Theorem	climinf2 45684*	A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < ))
Theorem	limsupvaluz 45685*	The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -∞ and the r.h.s. would be +∞). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑘)), ℝ*, < )), ℝ*, < ))
Theorem	limsupresuz2 45686	If the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → dom 𝐹 ⊆ ℤ)    ⇒   ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹))
Theorem	limsuppnflem 45687*	If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    ⇒   ⊢ (𝜑 → ((lim sup‘𝐹) = +∞ ↔ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))))
Theorem	limsuppnf 45688*	If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    ⇒   ⊢ (𝜑 → ((lim sup‘𝐹) = +∞ ↔ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))))
Theorem	limsupubuzlem 45689*	If the limsup is not +∞, then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝑋    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌))    &   ⊢ 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))    &   ⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < )    &   ⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥)
Theorem	limsupubuz 45690*	For a real-valued function on a set of upper integers, if the superior limit is not +∞, then the function is bounded above. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥)
Theorem	climinf2mpt 45691*	A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝑘 = 𝑗 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = (𝑘 + 1)) → 𝐶 ≤ 𝐵)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ inf(ran (𝑘 ∈ 𝑍 ↦ 𝐵), ℝ*, < ))
Theorem	climinfmpt 45692*	A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝑘 = 𝑗 → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = (𝑘 + 1)) → 𝐶 ≤ 𝐵)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ inf(ran (𝑘 ∈ 𝑍 ↦ 𝐵), ℝ*, < ))
Theorem	climinf3 45693*	A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < ))
Theorem	limsupvaluzmpt 45694*	The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -∞ and the r.h.s. would be +∞). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝑗 ∈ (ℤ≥‘𝑘) ↦ 𝐵), ℝ*, < )), ℝ*, < ))
Theorem	limsupequzmpt2 45695*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑗𝐵    &   ⊢ 𝐴 = (ℤ≥‘𝑀)    &   ⊢ 𝐵 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim sup‘(𝑗 ∈ 𝐵 ↦ 𝐶)))
Theorem	limsupubuzmpt 45696*	If the limsup is not +∞, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ 𝐵)) ≠ +∞)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥)
Theorem	limsupmnflem 45697*	The superior limit of a function is -∞ if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup((𝐹 “ (𝑘[,)+∞)), ℝ*, < ))    ⇒   ⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)))
Theorem	limsupmnf 45698*	The superior limit of a function is -∞ if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    ⇒   ⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)))
Theorem	limsupequzlem 45699*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 Fn (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 Fn (ℤ≥‘𝑁))    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = (lim sup‘𝐺))
Theorem	limsupequz 45700*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 Fn (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 Fn (ℤ≥‘𝑁))    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = (lim sup‘𝐺))