P. 401 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40001-40100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	climlimsupcex 40001	Counterexample for climlimsup 39992, showing that the first hypothesis is needed, if the empty set is a complex number (see 0ncn 9954 and its comment) (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ¬ 𝑀 ∈ ℤ    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐹 = ∅    ⇒   ⊢ ((∅ ∈ ℂ ∧ ¬ -∞ ∈ ℂ) → (𝐹:𝑍⟶ℝ ∧ 𝐹 ∈ dom ⇝ ∧ ¬ 𝐹 ⇝ (lim sup‘𝐹)))
Theorem	liminfcld 40002	Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ*)
Theorem	liminfresico 40003	The inferior limit doesn't change when a function is restricted to an upperset of reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ 𝑍 = (𝑀[,)+∞)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (lim inf‘(𝐹 ↾ 𝑍)) = (lim inf‘𝐹))
Theorem	limsup10exlem 40004*	The range of the given function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 1))    &   ⊢ (𝜑 → 𝐾 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹 “ (𝐾[,)+∞)) = {0, 1})
Theorem	limsup10ex 40005	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 40006	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 40007*	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 40008*	The superior limit is greater than or equal to the inferior limit. The second hypothesis is needed (see liminflelimsupcex 40029 for a counterexample). The inequality can be strict, see liminfltlimsupex 40013. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)    ⇒   ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
Theorem	limsupgtlem 40009*	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 40010*	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 40011	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 40012*	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 40013	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 40014*	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 40015*	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 40016	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 40017	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 40018*	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 40019	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 40020	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 40021*	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 40022*	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 40023*	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 40024*	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 40025	The inferior limit of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (lim inf‘∅) = +∞
Theorem	limsupval4 40026*	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 40027*	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 40028*	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 40029	A counterexample for liminflelimsup 40008, showing that the second hypothesis is needed. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (lim sup‘∅) < (lim inf‘∅)
Theorem	limsupvaluz3 40030*	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 40031*	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 40032*	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 40033	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 40034*	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 40035*	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 40036*	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 40037*	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 40038	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 40039	A sequence of real numbers converges if its inferior limit is real, and it is greater or equal to the superior limit (in such a case, they are actually equal, see liminflelimsupuz 40017). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → (lim inf‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → (lim sup‘𝐹) ≤ (lim inf‘𝐹))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝ )
Theorem	climliminflimsup 40040	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 40020). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim inf‘𝐹) ∈ ℝ ∧ (lim sup‘𝐹) ≤ (lim inf‘𝐹))))
Theorem	climliminflimsup2 40041	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 40020). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ ((lim sup‘𝐹) ∈ ℝ ∧ (lim sup‘𝐹) ≤ (lim inf‘𝐹))))
Theorem	climliminflimsup3 40042	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 40043	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‘𝐹))))
20.32.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 40074.
Syntax	clsxlim 40044	Extend class notation with convergence relation for limits in the extended real numbers.
class ~~>*
Definition	df-xlim 40045	Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))
Theorem	xlimrel 40046	The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Rel ~~>*
Theorem	xlimres 40047	A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ↾ (ℤ≥‘𝑀))~~>*𝐴))
Theorem	xlimcl 40048	The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝐹~~>*𝐴 → 𝐴 ∈ ℝ*)
Theorem	rexlimddv2 40049*	Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	xlimclim 40050	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 39845). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimconst 40051*	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 40052	A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	xlimbr 40053*	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 40054	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 40055*	Lemma for cnrefiisp 40056 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝐶 = (ℝ ∪ 𝐵)    &   ⊢ 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})    &   ⊢ 𝑋 = inf(𝐷, ℝ*, < )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))))
Theorem	cnrefiisp 40056*	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 40057*	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 40058*	The "only if" part of the biconditional in xlimmnf 40067. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*-∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑋)
Theorem	xlimmnfvlem2 40059*	The "if" part of the biconditional in xlimpnf 40068. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥)    ⇒   ⊢ (𝜑 → 𝐹~~>*-∞)
Theorem	xlimmnfv 40060*	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 40061*	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 40062*	The "only if" part of the biconditional in xlimmnf 40067. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*+∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑋 ≤ (𝐹‘𝑘))
Theorem	xlimpnfvlem2 40063*	The "if" part of the biconditional in xlimpnf 40068. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹~~>*+∞)
Theorem	xlimpnfv 40064*	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 40065*	Lemma for xlimclim2 40066. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimclim2 40066	Given a sequence of extended reals, it converges to a real number 𝐴 w.r.t. the standard topology on the reals (see climreeq 39845), 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 40067*	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 40068*	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 40069*	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 40070*	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 40071	In this lemma for climxlim2 40072 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 40072	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 40073*	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 40074*	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.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ⇝ 𝐴 ∨ (𝐴 = -∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑥) ∨ (𝐴 = +∞ ∧ ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 ≤ (𝐹‘𝑘)))))
20.32.8  Trigonometry
Theorem	coseq0 40075	A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) = 0 ↔ ((𝐴 / π) + (1 / 2)) ∈ ℤ))
Theorem	sinmulcos 40076	Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (cos‘𝐵)) = (((sin‘(𝐴 + 𝐵)) + (sin‘(𝐴 − 𝐵))) / 2))
Theorem	coskpi2 40077	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 40078	The cosine of negative π is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (cos‘-π) = -1
Theorem	sinaover2ne0 40079	If 𝐴 in (0, 2π) then sin(𝐴 / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (0(,)(2 · π)) → (sin‘(𝐴 / 2)) ≠ 0)
Theorem	cosknegpi 40080	The cosine of an integer multiple of negative π is either 1 ore negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1))
20.32.9  Continuous Functions
Theorem	mulcncff 40081	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	subcncf 40082*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmptssg 40083*	A continuous complex function restricted to a subset is continuous, using "map to" notation. This theorem generalizes cncfmptss 39819 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐸 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷))
Theorem	constcncfg 40084*	A constant function is a continuous function on ℂ. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→𝐶))
Theorem	idcncfg 40085*	The identity function is a continuous function on ℂ. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (𝐴–cn→𝐵))
Theorem	addcncf 40086*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfshift 40087*	A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)}    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐹‘(𝑥 − 𝑇)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→ℂ))
Theorem	resincncf 40088	sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
Theorem	addccncf2 40089*	Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝑥))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	0cnf 40090	The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ∅ ∈ ({∅} Cn {∅})
Theorem	fsumcncf 40091*	The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝑋–cn→ℂ))
Theorem	cncfperiod 40092*	A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)}    &   ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ⊆ dom 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ))
Theorem	subcncff 40093	The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	negcncfg 40094*	The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (𝐴–cn→ℂ))
Theorem	cnfdmsn 40095*	A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) ∈ (𝒫 {𝐴} Cn 𝒫 {𝐵}))
Theorem	cncfcompt 40096*	Composition of continuous functions. A generalization of cncfmpt1f 22716 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→𝐶))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶–cn→𝐷))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→𝐷))
Theorem	addcncff 40097	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	ioccncflimc 40098	Limit at the upper bound, of a continuous function defined on a left open right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,]𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹‘𝐵) ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵))
Theorem	cncfuni 40099*	A function is continuous if it's domain is the union of sets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴))    &   ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	icccncfext 40100*	A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝑌 = ∪ 𝐾    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴[,]𝐵), (𝐹‘𝑥), if(𝑥 < 𝐴, (𝐹‘𝐴), (𝐹‘𝐵))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ Top)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t (𝐴[,]𝐵)) Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝐺 ∈ (𝐽 Cn (𝐾 ↾t ran 𝐹)) ∧ (𝐺 ↾ (𝐴[,]𝐵)) = 𝐹))