climxlim2

Description: 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 +oo and -oo could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climxlim2.m	$⊢ φ \to M \in ℤ$
	climxlim2.z	$⊢ Z = ℤ_{\geq M}$
	climxlim2.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	climxlim2.a	$⊢ φ \to F ⇝ A$
Assertion	climxlim2	$⊢ φ \to F \underset{*}{⇝} A$

Proof

Step	Hyp	Ref	Expression
1		climxlim2.m	$⊢ φ \to M \in ℤ$
2		climxlim2.z	$⊢ Z = ℤ_{\geq M}$
3		climxlim2.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		climxlim2.a	$⊢ φ \to F ⇝ A$
5	2	eluzelz2	$⊢ j \in Z \to j \in ℤ$
6	5	ad2antlr	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to j \in ℤ$
7		eqid	$⊢ ℤ_{\geq j} = ℤ_{\geq j}$
8	3	adantr	$⊢ (φ \land j \in Z) \to F : Z ⟶ ℝ^{*}$
9	2	uzssd3	$⊢ j \in Z \to ℤ_{\geq j} \subseteq Z$
10	9	adantl	$⊢ (φ \land j \in Z) \to ℤ_{\geq j} \subseteq Z$
11	8 10	fssresd	$⊢ (φ \land j \in Z) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ^{*}$
12	11	adantr	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ^{*}$
13		simpr	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ$
14	4	adantr	$⊢ (φ \land j \in Z) \to F ⇝ A$
15	2	fvexi	$⊢ Z \in V$
16	15	a1i	$⊢ φ \to Z \in V$
17	3 16	fexd	$⊢ φ \to F \in V$
18		climres	$⊢ (j \in ℤ \land F \in V) \to (({F ↾}_{ℤ_{\geq j}}) ⇝ A \leftrightarrow F ⇝ A)$
19	5 17 18	syl2anr	$⊢ (φ \land j \in Z) \to (({F ↾}_{ℤ_{\geq j}}) ⇝ A \leftrightarrow F ⇝ A)$
20	14 19	mpbird	$⊢ (φ \land j \in Z) \to ({F ↾}_{ℤ_{\geq j}}) ⇝ A$
21	20	adantr	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to ({F ↾}_{ℤ_{\geq j}}) ⇝ A$
22	6 7 12 13 21	climxlim2lem	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to ({F ↾}_{ℤ_{\geq j}}) \underset{*}{⇝} A$
23	2 3	fuzxrpmcn	$⊢ φ \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
24	23	adantr	$⊢ (φ \land j \in Z) \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
25	5	adantl	$⊢ (φ \land j \in Z) \to j \in ℤ$
26	24 25	xlimres	$⊢ (φ \land j \in Z) \to (F \underset{}{⇝} A \leftrightarrow ({F ↾}_{ℤ_{\geq j}}) \underset{}{⇝} A)$
27	26	adantr	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to (F \underset{}{⇝} A \leftrightarrow ({F ↾}_{ℤ_{\geq j}}) \underset{}{⇝} A)$
28	22 27	mpbird	$⊢ ((φ \land j \in Z) \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ) \to F \underset{*}{⇝} A$
29	3	ffnd	$⊢ φ \to F Fn Z$
30		climcl	$⊢ F ⇝ A \to A \in ℂ$
31	4 30	syl	$⊢ φ \to A \in ℂ$
32		breldmg	$⊢ (F \in V \land A \in ℂ \land F ⇝ A) \to F \in dom ⇝$
33	17 31 4 32	syl3anc	$⊢ φ \to F \in dom ⇝$
34	1 2 29 33	climrescn	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℂ$
35	28 34	r19.29a	$⊢ φ \to F \underset{*}{⇝} A$

Metamath Proof Explorer

Theorem climxlim2

Proof