P. 422 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42101-42200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xlimpnfxnegmnf 42101*	A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥))
Theorem	liminflbuz2 42102*	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 42103*	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 42104*	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‘𝐹) ≠ -∞)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ)
20.37.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 42135.
Syntax	clsxlim 42105	Extend class notation with convergence relation for limits in the extended real numbers.
class ~~>*
Definition	df-xlim 42106	Define the convergence relation for extended real sequences. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ~~>* = (⇝𝑡‘(ordTop‘ ≤ ))
Theorem	xlimrel 42107	The limit on extended reals is a relation. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Rel ~~>*
Theorem	xlimres 42108	A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐹 ∈ (ℝ* ↑pm ℂ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ (𝐹 ↾ (ℤ≥‘𝑀))~~>*𝐴))
Theorem	xlimcl 42109	The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝐹~~>*𝐴 → 𝐴 ∈ ℝ*)
Theorem	rexlimddv2 42110*	Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	xlimclim 42111	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 41900). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimconst 42112*	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 42113	A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹~~>*𝐴)
Theorem	xlimbr 42114*	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 42115	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 42116*	Lemma for cnrefiisp 42117 (some local definitions are used). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ 𝐶 = (ℝ ∪ 𝐵)    &   ⊢ 𝐷 = ({(abs‘(ℑ‘𝐴))} ∪ ∪ 𝑦 ∈ ((𝐵 ∩ ℂ) ∖ {𝐴}){(abs‘(𝑦 − 𝐴))})    &   ⊢ 𝑋 = inf(𝐷, ℝ*, < )    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝐶 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴) → 𝑥 ≤ (abs‘(𝑦 − 𝐴))))
Theorem	cnrefiisp 42117*	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 42118*	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 42119*	Lemma for xlimmnfv 42121: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*-∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ≤ 𝑋)
Theorem	xlimmnfvlem2 42120*	Lemma for xlimmnf 42128: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥)    ⇒   ⊢ (𝜑 → 𝐹~~>*-∞)
Theorem	xlimmnfv 42121*	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 42122*	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 42123*	Lemma for xlimpnfv 42125: the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐹~~>*+∞)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑋 ≤ (𝐹‘𝑘))
Theorem	xlimpnfvlem2 42124*	Lemma for xlimpnfv 42125: the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑗𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹~~>*+∞)
Theorem	xlimpnfv 42125*	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 42126*	Lemma for xlimclim2 42127. Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹~~>*𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	xlimclim2 42127	Given a sequence of extended reals, it converges to a real number 𝐴 w.r.t. the standard topology on the reals (see climreeq 41900), 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 42128*	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 42129*	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 42130*	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 42131*	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 42132	In this lemma for climxlim2 42133 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 42133	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 42134*	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 42135*	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 42136	A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑀)) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	climresdm 42137	A real function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ (𝐹 ↾ (ℤ≥‘𝑀)) ∈ dom ⇝ ))
Theorem	dmclimxlim 42138	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 42139	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 42140	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 42141	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 42142	The convergence relation on the extended reals is a function. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Fun ~~>*
Theorem	xlimmnflimsup 42143	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 42144	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 42145*	A sequence converges to +∞ if and only if its negation converges to -∞. (Contributed by Glauco Siliprandi, 23-Apr-2023.)
⊢ Ⅎ𝑗𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*)    ⇒   ⊢ (𝜑 → (𝐹~~>*+∞ ↔ (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))~~>*-∞))
Theorem	xlimresdm 42146	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 42147	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 42148	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 42149	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 42150	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‘𝐹)))
20.37.8  Trigonometry
Theorem	coseq0 42151	A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) = 0 ↔ ((𝐴 / π) + (1 / 2)) ∈ ℤ))
Theorem	sinmulcos 42152	Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (cos‘𝐵)) = (((sin‘(𝐴 + 𝐵)) + (sin‘(𝐴 − 𝐵))) / 2))
Theorem	coskpi2 42153	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 42154	The cosine of negative π is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (cos‘-π) = -1
Theorem	sinaover2ne0 42155	If 𝐴 in (0, 2π) then sin(𝐴 / 2) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (0(,)(2 · π)) → (sin‘(𝐴 / 2)) ≠ 0)
Theorem	cosknegpi 42156	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))
20.37.9  Continuous Functions
Theorem	mulcncff 42157	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	subcncf 42158*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmptssg 42159*	A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 41874 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐸)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐸 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷))
Theorem	constcncfg 42160*	A constant function is a continuous function on ℂ. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→𝐶))
Theorem	idcncfg 42161*	The identity function is a continuous function on ℂ. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (𝐴–cn→𝐵))
Theorem	addcncf 42162*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfshift 42163*	A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)}    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐹‘(𝑥 − 𝑇)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→ℂ))
Theorem	resincncf 42164	sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
Theorem	addccncf2 42165*	Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝑥))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	0cnf 42166	The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ∅ ∈ ({∅} Cn {∅})
Theorem	fsumcncf 42167*	The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑋 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝑋–cn→ℂ))
Theorem	cncfperiod 42168*	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 42169	The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	negcncfg 42170*	The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ (𝐴–cn→ℂ))
Theorem	cnfdmsn 42171*	A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) ∈ (𝒫 {𝐴} Cn 𝒫 {𝐵}))
Theorem	cncfcompt 42172*	Composition of continuous functions. A generalization of cncfmpt1f 23524 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐴–cn→𝐶))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶–cn→𝐷))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ (𝐴–cn→𝐷))
Theorem	addcncff 42173	The sum of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	ioccncflimc 42174	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 42175*	A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈ ((TopOpen‘ℂfld) ↾t 𝐴))    &   ⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	icccncfext 42176*	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 𝐹)) ∧ (𝐺 ↾ (𝐴[,]𝐵)) = 𝐹))
Theorem	cncficcgt0 42177*	A the absolute value of a continuous function on a closed interval, that is never 0, has a strictly positive lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ (𝐴[,]𝐵)𝑦 ≤ (abs‘𝐶))
Theorem	icocncflimc 42178	Limit at the lower bound, of a continuous function defined on a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,)𝐵)–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴))
Theorem	cncfdmsn 42179*	A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ {𝐴} ↦ 𝐵) ∈ ({𝐴}–cn→{𝐵}))
Theorem	divcncff 42180	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑋–cn→(ℂ ∖ {0})))    ⇒   ⊢ (𝜑 → (𝐹 ∘f / 𝐺) ∈ (𝑋–cn→ℂ))
Theorem	cncfshiftioo 42181*	A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐶 = (𝐴(,)𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ ℝ)    &   ⊢ 𝐷 = ((𝐴 + 𝑇)(,)(𝐵 + 𝑇))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐶–cn→ℂ))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (𝐹‘(𝑥 − 𝑇)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐷–cn→ℂ))
Theorem	cncfiooicclem1 42182*	A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 can be complex-valued. This lemma assumes 𝐴 < 𝐵, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Theorem	cncfiooicc 42183*	A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 can be complex-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Theorem	cncfiooiccre 42184*	A continuous function 𝐹 on an open interval (𝐴(,)𝐵) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵. 𝐹 is assumed to be real-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))
Theorem	cncfioobdlem 42185*	𝐺 actually extends 𝐹. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶𝑉)    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → (𝐺‘𝐶) = (𝐹‘𝐶))
Theorem	cncfioobd 42186*	A continuous function 𝐹 on an open interval (𝐴(,)𝐵) with a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐵 is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥)
Theorem	jumpncnp 42187	Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵))))    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞))))    &   ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵))    &   ⊢ (𝜑 → 𝐿 ≠ 𝑅)    ⇒   ⊢ (𝜑 → ¬ 𝐹 ∈ ((𝐽 CnP (TopOpen‘ℂfld))‘𝐵))
Theorem	cncfcompt2 42188*	Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑆) ∈ (𝐶–cn→𝐸))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑇) ∈ (𝐴–cn→𝐸))
Theorem	cxpcncf2 42189*	The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝐴 ∈ (ℂ ∖ (-∞(,]0)) → (𝑥 ∈ ℂ ↦ (𝐴↑𝑐𝑥)) ∈ (ℂ–cn→ℂ))
Theorem	fprodcncf 42190*	The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ (𝐴–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∏𝑘 ∈ 𝐵 𝐶) ∈ (𝐴–cn→ℂ))
Theorem	add1cncf 42191*	Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	add2cncf 42192*	Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 + 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	sub1cncfd 42193*	Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	sub2cncfd 42194*	Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	fprodsub2cncf 42195*	𝐹 is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 − 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	fprodadd2cncf 42196*	𝐹 is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 + 𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	fprodsubrecnncnvlem 42197*	The sequence 𝑆 of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝐴 (𝐵 − (1 / 𝑛)))    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 − 𝑥))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝐴 𝐵)
Theorem	fprodsubrecnncnv 42198*	The sequence 𝑆 of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (𝐴 − (1 / 𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 𝐴)
Theorem	fprodaddrecnncnvlem 42199*	The sequence 𝑆 of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝐴 (𝐵 + (1 / 𝑛)))    &   ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ ∏𝑘 ∈ 𝐴 (𝐵 + 𝑥))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝐴 𝐵)
Theorem	fprodaddrecnncnv 42200*	The sequence 𝑆 of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℂ)    &   ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (𝐴 + (1 / 𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 𝐴)