P. 438 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43701-43800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	limsup10exlem 43701*	The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 1))    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 “ (𝐾[,)+∞)) = {0, 1})
Theorem	limsup10ex 43702	The superior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 1))    ⇒   ⊢ (lim sup‘𝐹) = 1
Theorem	liminf10ex 43703	The inferior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 1))    ⇒   ⊢ (lim inf‘𝐹) = 0
Theorem	liminflelimsuplem 43704*	The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
Theorem	liminflelimsup 43705*	The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 43726 for a counterexample). The inequality can be strict, see liminfltlimsupex 43710. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
Theorem	limsupgtlem 43706*	For any positive real, the superior limit of F is larger than any of its values at large enough arguments, up to that positive real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹))
Theorem	limsupgt 43707*	Given a sequence of real numbers, there exists an upper part of the sequence that's appxoximated from below by the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑋) < (lim sup‘𝐹))
Theorem	liminfresre 43708	The inferior limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim inf‘(𝐹 ↾ ℝ)) = (lim inf‘𝐹))
Theorem	liminfresicompt 43709*	The inferior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ 𝑍 = (𝑀[,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑥 ∈ (𝐴 ∩ 𝑍) ↦ 𝐵)) = (lim inf‘(𝑥 ∈ 𝐴 ↦ 𝐵)))
Theorem	liminfltlimsupex 43710	An example where the lim inf is strictly smaller than the lim sup. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 1))    ⇒   ⊢ (lim inf‘𝐹) < (lim sup‘𝐹)
Theorem	liminfgelimsup 43711*	The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)    ⇒   ⊢ (𝜑 → ((lim sup‘𝐹) ≤ (lim inf‘𝐹) ↔ (lim inf‘𝐹) = (lim sup‘𝐹)))
Theorem	liminfvalxr 43712*	Alternate definition of lim inf when 𝐹 is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑥))))
Theorem	liminfresuz 43713	If the real part of the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → dom (𝐹 ↾ ℝ) ⊆ ℤ)    ⇒   ⊢ (𝜑 → (lim inf‘(𝐹 ↾ 𝑍)) = (lim inf‘𝐹))
Theorem	liminflelimsupuz 43714	The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
Theorem	liminfvalxrmpt 43715*	Alternate definition of lim inf when 𝐹 is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒𝐵)))
Theorem	liminfresuz2 43716	If the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → dom 𝐹 ⊆ ℤ)    ⇒   ⊢ (𝜑 → (lim inf‘(𝐹 ↾ 𝑍)) = (lim inf‘𝐹))
Theorem	liminfgelimsupuz 43717	The inferior limit is greater than or equal to the superior limit if and only if they are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → ((lim sup‘𝐹) ≤ (lim inf‘𝐹) ↔ (lim inf‘𝐹) = (lim sup‘𝐹)))
Theorem	liminfval4 43718*	Alternate definition of lim inf when the given function is eventually real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ (𝑀[,)+∞))) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝐵)))
Theorem	liminfval3 43719*	Alternate definition of lim inf when the given function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ (𝑀[,)+∞))) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒𝐵)))
Theorem	liminfequzmpt2 43720*	Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑗𝐵    &   ⊢ 𝐴 = (ℤ≥‘𝑀)    &   ⊢ 𝐵 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim inf‘(𝑗 ∈ 𝐵 ↦ 𝐶)))
Theorem	liminfvaluz 43721*	Alternate definition of lim inf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = -𝑒(lim sup‘(𝑘 ∈ 𝑍 ↦ -𝑒𝐵)))
Theorem	liminf0 43722	The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (lim inf‘∅) = +∞
Theorem	limsupval4 43723*	Alternate definition of lim inf when the given a function is eventually extended real-valued. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ (𝑀[,)+∞))) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (lim sup‘(𝑥 ∈ 𝐴 ↦ 𝐵)) = -𝑒(lim inf‘(𝑥 ∈ 𝐴 ↦ -𝑒𝐵)))
Theorem	liminfvaluz2 43724*	Alternate definition of lim inf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (lim inf‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = -𝑒(lim sup‘(𝑘 ∈ 𝑍 ↦ -𝐵)))
Theorem	liminfvaluz3 43725*	Alternate definition of lim inf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim sup‘(𝑘 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑘))))
Theorem	liminflelimsupcex 43726	A counterexample for liminflelimsup 43705, showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (lim sup‘∅) < (lim inf‘∅)
Theorem	limsupvaluz3 43727*	Alternate definition of lim inf for an extended real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (lim sup‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = -𝑒(lim inf‘(𝑘 ∈ 𝑍 ↦ -𝑒𝐵)))
Theorem	liminfvaluz4 43728*	Alternate definition of lim inf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))))
Theorem	limsupvaluz4 43729*	Alternate definition of lim inf for a real-valued function, defined on a set of upper integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (lim sup‘(𝑘 ∈ 𝑍 ↦ 𝐵)) = -𝑒(lim inf‘(𝑘 ∈ 𝑍 ↦ -𝐵)))
Theorem	climliminflimsupd 43730	If a sequence of real numbers converges, its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = (lim sup‘𝐹))
Theorem	liminfreuzlem 43731*	Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → ((lim inf‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 ∃𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑗))))
Theorem	liminfreuz 43732*	Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → ((lim inf‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 ∃𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑗))))
Theorem	liminfltlem 43733*	Given a sequence of real numbers, there exists an upper part of the sequence that's approximated from above by the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋))
Theorem	liminflt 43734*	Given a sequence of real numbers, there exists an upper part of the sequence that's approximated from above by the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋))
Theorem	climliminf 43735	A sequence of real numbers converges if and only if it converges to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ (lim inf‘𝐹)))
Theorem	liminflimsupclim 43736	A sequence of real numbers converges if its inferior limit is real, and it is greater than or equal to the superior limit (in such a case, they are actually equal, see liminflelimsupuz 43714). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≤ (lim inf‘𝐹))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	climliminflimsup 43737	A sequence of real numbers converges if and only if its inferior limit is real and it is greater than or equal to its superior limit (in such a case, they are actually equal, see liminfgelimsupuz 43717). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim inf‘𝐹) ∈ ℝ ∧ (lim sup‘𝐹) ≤ (lim inf‘𝐹))))
Theorem	climliminflimsup2 43738	A sequence of real numbers converges if and only if its superior limit is real and it is less than or equal to its inferior limit (in such a case, they are actually equal, see liminfgelimsupuz 43717). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim sup‘𝐹) ∈ ℝ ∧ (lim sup‘𝐹) ≤ (lim inf‘𝐹))))
Theorem	climliminflimsup3 43739	A sequence of real numbers converges if and only if its inferior limit is real and equal to its superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim inf‘𝐹) ∈ ℝ ∧ (lim inf‘𝐹) = (lim sup‘𝐹))))
Theorem	climliminflimsup4 43740	A sequence of real numbers converges if and only if its superior limit is real and equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim sup‘𝐹) ∈ ℝ ∧ (lim inf‘𝐹) = (lim sup‘𝐹))))
Theorem	limsupub2 43741*	A extended real valued function, with limsup that is not +∞, is eventually less than +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < +∞))
Theorem	limsupubuz2 43742*	A sequence with values in the extended reals, and with limsup that is not +∞, is eventually less than +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) < +∞)
Theorem	xlimpnfxnegmnf 43743*	A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥))
Theorem	liminflbuz2 43744*	A sequence with values in the extended reals, and with liminf that is not -∞, is eventually greater than -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝜑    &   ⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → (lim inf‘𝐹) ≠ -∞)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-∞ < (𝐹‘𝑗))
Theorem	liminfpnfuz 43745*	The inferior limit of a function is +∞ if and only if every real number is the lower bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → ((lim inf‘𝐹) = +∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗)))
Theorem	liminflimsupxrre 43746*	A sequence with values in the extended reals, and with real liminf and limsup, is eventually real. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)    &   ⊢ (𝜑 → (lim inf‘𝐹) ≠ -∞)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ)
21.38.7.2  Limits for sequences of extended real numbers Textbooks generally use a single symbol to denote the limit of a sequence of real numbers. But then, three distinct definitions are usually given: one for the case of convergence to a real number, one for the case of limit to +∞ and one for the case of limit to -∞. It turns out that these three definitions can be expressed as the limit w.r.t. to the standard topology on the extended reals. In this section, a relation ~~>* is defined that captures all three definitions (and can be applied to sequences of extended reals, also), see dfxlim2 43777.
Syntax	clsxlim 43747	Extend class notation with convergence relation for limits in the extended real numbers.
class ~~>*
Definition	df-xlim 43748	Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))
Theorem	xlimrel 43749	The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Rel ~~>*
Theorem	xlimres 43750	A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ↾ (ℤ≥‘𝑀))~~>*𝐴))
Theorem	xlimcl 43751	The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝐹~~>*𝐴 → 𝐴 ∈ ℝ*)
Theorem	rexlimddv2 43752*	Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	xlimclim 43753	Given a sequence of reals, it converges to a real number 𝐴 w.r.t. the standard topology on the reals, if and only if it converges to 𝐴 w.r.t. to the standard topology on the extended reals (see climreeq 43542). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimconst 43754*	A constant sequence converges to its value, w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 Fn 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	climxlim 43755	A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	xlimbr 43756*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ (𝜑 → (𝐹~~>*𝑃 ↔ (𝑃 ∈ ℝ* ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))))
Theorem	fuzxrpmcn 43757	A function mapping from an upper set of integers to the extended reals is a partial map on the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))
Theorem	cnrefiisplem 43758*	Lemma for cnrefiisp 43759 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝐶 = (ℝ ∪ 𝐵)    &   ⊢ 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})    &   ⊢ 𝑋 = inf(𝐷, ℝ*, < )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))))
Theorem	cnrefiisp 43759*	A non-real, complex number is an isolated point w.r.t. the union of the reals with any finite set (the extended reals is an example of such a union). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝐶 = (ℝ ∪ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))))
Theorem	xlimxrre 43760*	If a sequence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued (the weaker hypothesis 𝐹 ∈ dom ⇝ is probably not enough, since in principle we could have +∞ ∈ ℂ and -∞ ∈ ℂ). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹~~>*𝐴)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ)
Theorem	xlimmnfvlem1 43761*	Lemma for xlimmnfv 43763: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*-∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑋)
Theorem	xlimmnfvlem2 43762*	Lemma for xlimmnf 43770: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥)    ⇒   ⊢ (𝜑 → 𝐹~~>*-∞)
Theorem	xlimmnfv 43763*	A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥))
Theorem	xlimconst2 43764*	A sequence that eventually becomes constant, converges to its constant value (w.r.t. the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	xlimpnfvlem1 43765*	Lemma for xlimpnfv 43767: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*+∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑋 ≤ (𝐹‘𝑘))
Theorem	xlimpnfvlem2 43766*	Lemma for xlimpnfv 43767: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹~~>*+∞)
Theorem	xlimpnfv 43767*	A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))
Theorem	xlimclim2lem 43768*	Lemma for xlimclim2 43769. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimclim2 43769	Given a sequence of extended reals, it converges to a real number 𝐴 w.r.t. the standard topology on the reals (see climreeq 43542), if and only if it converges to 𝐴 w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimmnf 43770*	A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥))
Theorem	xlimpnf 43771*	A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))
Theorem	xlimmnfmpt 43772*	A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ*)    &   ⊢ 𝐹 = (𝑘 ∈ 𝑍 ↦ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹~~>*-∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐵 ≤ 𝑥))
Theorem	xlimpnfmpt 43773*	A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ*)    &   ⊢ 𝐹 = (𝑘 ∈ 𝑍 ↦ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ 𝐵))
Theorem	climxlim2lem 43774	In this lemma for climxlim2 43775 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	climxlim2 43775	A sequence of extended reals, converging w.r.t. the standard topology on the complex numbers is a converging sequence w.r.t. the standard topology on the extended reals. This is non-trivial, because +∞ and -∞ could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	dfxlim2v 43776*	An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))))
Theorem	dfxlim2 43777*	An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))))
Theorem	climresd 43778	A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	climresdm 43779	A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ⇝ ))
Theorem	dmclimxlim 43780	A real valued sequence that converges w.r.t. the topology on the complex numbers, converges w.r.t. the topology on the extended reals (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ~~>*)
Theorem	xlimmnflimsup2 43781	A sequence of extended reals converges to -∞ if and only if its superior limit is also -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*-∞ ↔ (lim sup‘𝐹) = -∞))
Theorem	xlimuni 43782	An infinite sequence converges to at most one limit (w.r.t. to the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝐹~~>*𝐴)    &   ⊢ (𝜑 → 𝐹~~>*𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	xlimclimdm 43783	A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	xlimfun 43784	The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Fun ~~>*
Theorem	xlimmnflimsup 43785	If a sequence of extended reals converges to -∞ then its superior limit is also -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*-∞)    ⇒   ⊢ (𝜑 → (lim sup‘𝐹) = -∞)
Theorem	xlimdm 43786	Two ways to express that a function has a limit. (The expression (~~>*‘𝐹) is sometimes useful as a shorthand for "the unique limit of the function 𝐹"). (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝐹 ∈ dom ~~>* ↔ 𝐹~~>*(~~>*‘𝐹))
Theorem	xlimpnfxnegmnf2 43787*	A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))~~>*-∞))
Theorem	xlimresdm 43788	A function converges in the extended reals iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ~~>*))
Theorem	xlimpnfliminf 43789	If a sequence of extended reals converges to +∞ then its superior limit is also +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*+∞)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) = +∞)
Theorem	xlimpnfliminf2 43790	A sequence of extended reals converges to +∞ if and only if its superior limit is also +∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ (lim inf‘𝐹) = +∞))
Theorem	xlimliminflimsup 43791	A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (lim inf‘𝐹) = (lim sup‘𝐹)))
Theorem	xlimlimsupleliminf 43792	A sequence of extended reals converges if and only if its superior limit is smaller than or equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Dec-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ~~>* ↔ (lim sup‘𝐹) ≤ (lim inf‘𝐹)))
21.38.8  Trigonometry
Theorem	coseq0 43793	A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) = 0 ↔ ((𝐴 / π) + (1 / 2)) ∈ ℤ))
Theorem	sinmulcos 43794	Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (cos‘𝐵)) = (((sin‘(𝐴 + 𝐵)) + (sin‘(𝐴 − 𝐵))) / 2))
Theorem	coskpi2 43795	The cosine of an integer multiple of negative π is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · π)) = if(2 ∥ 𝐾, 1, -1))
Theorem	cosnegpi 43796	The cosine of negative π is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (cos‘-π) = -1
Theorem	sinaover2ne0 43797	If 𝐴 in (0, 2π) then sin(𝐴 / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (0(,)(2 · π)) → (sin‘(𝐴 / 2)) ≠ 0)
Theorem	cosknegpi 43798	The cosine of an integer multiple of negative π is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1))
21.38.9  Continuous Functions
Theorem	mulcncff 43799	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	cncfmptssg 43800*	A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 43516 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐸 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷))