P. 447 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44601-44700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fmul01lt1lem2 44601*	Given a finite multiplication of values betweeen 0 and 1, a value 𝐸 larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐵    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ 𝐴 = seq𝐿( · , 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑀))    &   ⊢ (𝜑 → (𝐵‘𝐽) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)
Theorem	fmul01lt1 44602*	Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑖𝐵    &   ⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ 𝐴 = seq1( · , 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵:(1...𝑀)⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ (𝐵‘𝑖))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵‘𝑖) ≤ 1)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → ∃𝑗 ∈ (1...𝑀)(𝐵‘𝑗) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)
Theorem	cncfmptss 44603*	A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ (𝐶–cn→𝐵))
Theorem	rrpsscn 44604	The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ℝ+ ⊆ ℂ
Theorem	mulc1cncfg 44605*	A version of mulc1cncf 24646 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (𝐹‘𝑥))) ∈ (𝐴–cn→ℂ))
Theorem	infrglb 44606*	The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐵 ∈ ℝ) → (inf(𝐴, ℝ, < ) < 𝐵 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝐵))
Theorem	expcnfg 44607*	If 𝐹 is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 24668. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)↑𝑁)) ∈ (𝐴–cn→ℂ))
Theorem	prodeq2ad 44608*	Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	fprodsplit1 44609*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (𝐷 · ∏𝑘 ∈ (𝐴 ∖ {𝐶})𝐵))
Theorem	fprodexp 44610*	Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵↑𝑁) = (∏𝑘 ∈ 𝐴 𝐵↑𝑁))
Theorem	fprodabs2 44611*	The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (abs‘∏𝑘 ∈ 𝐴 𝐵) = ∏𝑘 ∈ 𝐴 (abs‘𝐵))
Theorem	fprod0 44612*	A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐶    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 = 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0)
Theorem	mccllem 44613*	* Induction step for mccl 44614. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶))    &   ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m (𝐶 ∪ {𝐷})))    &   ⊢ (𝜑 → ∀𝑏 ∈ (ℕ0 ↑m 𝐶)((!‘Σ𝑘 ∈ 𝐶 (𝑏‘𝑘)) / ∏𝑘 ∈ 𝐶 (!‘(𝑏‘𝑘))) ∈ ℕ)    ⇒   ⊢ (𝜑 → ((!‘Σ𝑘 ∈ (𝐶 ∪ {𝐷})(𝐵‘𝑘)) / ∏𝑘 ∈ (𝐶 ∪ {𝐷})(!‘(𝐵‘𝑘))) ∈ ℕ)
Theorem	mccl 44614*	A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ (ℕ0 ↑m 𝐴))    ⇒   ⊢ (𝜑 → ((!‘Σ𝑘 ∈ 𝐴 (𝐵‘𝑘)) / ∏𝑘 ∈ 𝐴 (!‘(𝐵‘𝑘))) ∈ ℕ)
Theorem	fprodcnlem 44615*	A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ (𝐴 ∖ 𝑍))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝑍 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ (𝑍 ∪ {𝑊})𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	fprodcn 44616*	A finite product of functions to complex numbers from a common topological space is continuous. The class expression for 𝐵 normally contains free variables 𝑘 and 𝑥 to index it. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ∏𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
21.40.7  Limits
Theorem	clim1fr1 44617*	A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴 · 𝑛) + 𝐵) / (𝐴 · 𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	isumneg 44618*	Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 -𝐴 = -Σ𝑘 ∈ 𝑍 𝐴)
Theorem	climrec 44619*	Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘)))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴))
Theorem	climmulf 44620*	A version of climmul 15582 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 · 𝐵))
Theorem	climexp 44621*	The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘)↑𝑁))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴↑𝑁))
Theorem	climinf 44622*	A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < ))
Theorem	climsuselem1 44623*	The subsequence index 𝐼 has the expected properties: it belongs to the same upper integers as the original index, and it is always greater than or equal to the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1)))    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐼‘𝐾) ∈ (ℤ≥‘𝐾))
Theorem	climsuse 44624*	A subsequence 𝐺 of a converging sequence 𝐹, converges to the same limit. 𝐼 is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐼    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → (𝐼‘𝑀) ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐼‘(𝑘 + 1)) ∈ (ℤ≥‘((𝐼‘𝑘) + 1)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑌)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐹‘(𝐼‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)
Theorem	climrecf 44625*	A version of climrec 44619 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘)))    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴))
Theorem	climneg 44626*	Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) ⇝ -𝐴)
Theorem	climinff 44627*	A version of climinf 44622 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < ))
Theorem	climdivf 44628*	Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 / 𝐵))
Theorem	climreeq 44629	If 𝐹 is a real function, then 𝐹 converges to 𝐴 with respect to the standard topology on the reals if and only if it converges to 𝐴 with respect to the standard topology on complex numbers. In the theorem, 𝑅 is defined to be convergence w.r.t. the standard topology on the reals and then 𝐹𝑅𝐴 represents the statement "𝐹 converges to 𝐴, with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that 𝐴 is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.)
⊢ 𝑅 = (⇝𝑡‘(topGen‘ran (,)))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹𝑅𝐴 ↔ 𝐹 ⇝ 𝐴))
Theorem	ellimciota 44630*	An explicit value for the limit, when the limit exists at a limit point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    &   ⊢ (𝜑 → (𝐹 limℂ 𝐵) ≠ ∅)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → (℩𝑥𝑥 ∈ (𝐹 limℂ 𝐵)) ∈ (𝐹 limℂ 𝐵))
Theorem	climaddf 44631*	A version of climadd 15581 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ Ⅎ𝑘𝐻    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → 𝐻 ⇝ (𝐴 + 𝐵))
Theorem	mullimc 44632*	Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐻 limℂ 𝐷))
Theorem	ellimcabssub0 44633*	An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶))    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ 0 ∈ (𝐺 limℂ 𝐷)))
Theorem	limcdm0 44634	If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:∅⟶ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ℂ)
Theorem	islptre 44635*	An equivalence condition for a limit point w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)))
Theorem	limccog 44636	Limit of the composition of two functions. If the limit of 𝐹 at 𝐴 is 𝐵 and the limit of 𝐺 at 𝐵 is 𝐶, then the limit of 𝐺 ∘ 𝐹 at 𝐴 is 𝐶. With respect to limcco 25643 and limccnp 25641, here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ran 𝐹 ⊆ (dom 𝐺 ∖ {𝐵}))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐵))    ⇒   ⊢ (𝜑 → 𝐶 ∈ ((𝐺 ∘ 𝐹) limℂ 𝐴))
Theorem	limciccioolb 44637	The limit of a function at the lower 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	climf 44638*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 15443, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	mullimcf 44639*	Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))    &   ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷))
Theorem	constlimc 44640*	Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐶))
Theorem	rexlim2d 44641*	Inference removing two restricted quantifiers. Same as rexlimdvv 3209, but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒))
Theorem	idlimc 44642*	Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋))
Theorem	divcnvg 44643*	The sequence of reciprocals of positive integers, multiplied by the factor 𝐴, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑛 ∈ (ℤ≥‘𝑀) ↦ (𝐴 / 𝑛)) ⇝ 0)
Theorem	limcperiod 44644*	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 44645	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 44646*	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 44647	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 44648	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 44649	A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐵) → 𝐴 = 𝐶)
Theorem	elprn2 44650	A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐶) → 𝐴 = 𝐵)
Theorem	limcmptdm 44651*	The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ℂ)
Theorem	clim2f 44652*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15443. Similar to clim2 15453, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	limcicciooub 44653	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 44654	A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,)𝐴))    ⇒   ⊢ (𝜑 → (𝐶 mod 𝐵) < (𝐴 mod 𝐵))
Theorem	islpcn 44655*	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 44656*	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 44657*	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 44658	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 44659	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 44660	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 44661	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 44662	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 44663*	Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷))    ⇒   ⊢ (𝜑 → -𝐶 ∈ (𝐺 limℂ 𝐷))
Theorem	addlimc 44664*	Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 limℂ 𝐷))
Theorem	0ellimcdiv 44665*	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 44666*	Express the predicate 𝐹 converges to 𝐴. Similar to clim2 15453, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥))
Theorem	limclner 44667	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 44668*	Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷))    ⇒   ⊢ (𝜑 → (𝐸 − 𝐼) ∈ (𝐻 limℂ 𝐷))
Theorem	reclimc 44669*	Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖ {0}))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷))
Theorem	clim0cf 44670*	Express the predicate 𝐹 converges to 0. Similar to clim 15443, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥))
Theorem	limclr 44671	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 44672*	Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷))    &   ⊢ (𝜑 → 𝑌 ≠ 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋 / 𝑌) ∈ (𝐻 limℂ 𝐷))
Theorem	expfac 44673*	Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0)
Theorem	climconstmpt 44674*	A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐴)
Theorem	climresmpt 44675*	A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ 𝐺 = (𝑥 ∈ (ℤ≥‘𝑁) ↦ 𝐴)    ⇒   ⊢ (𝜑 → (𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵))
Theorem	climsubmpt 44676*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐷))
Theorem	climsubc2mpt 44677*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐵))
Theorem	climsubc1mpt 44678*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐴 − 𝐶))
Theorem	fnlimfv 44679*	The value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐷    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐺‘𝑋) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))))
Theorem	climreclf 44680*	The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	climeldmeq 44681*	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 44682*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 15443, but without the disjoint var constraint 𝜑𝑘 and 𝐹𝑘. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	fnlimcnv 44683*	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 44684*	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 44685*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺))
Theorem	clim2f2 44686*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15443. Similar to clim2 15453, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥))))
Theorem	climfveqmpt 44687*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷)))
Theorem	climd 44688*	Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋))
Theorem	clim2d 44689*	The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋))
Theorem	fnlimfvre 44690*	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 44691*	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 44692*	The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐶)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
Theorem	fnlimfvre2 44693*	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 44694*	The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺:𝐷⟶ℝ)
Theorem	fnlimabslt 44695*	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 44696*	Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐹    &   ⊢ Ⅎ𝑘𝐺    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘))    ⇒   ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺))
Theorem	climmptf 44697*	Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))    ⇒   ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴))
Theorem	climfveqmpt3 44698*	Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt 44687 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ⊆ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷)))
Theorem	climeldmeqf 44699*	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 44700*	The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ ℝ)