Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climxlim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climxlim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
	climxlim2.a	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
Assertion	climxlim2	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		climxlim2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climxlim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		climxlim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4		climxlim2.a	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
5	2	eluzelz2	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
6	5	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → 𝑗 ∈ ℤ )
7		eqid	⊢ ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑗 )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ℝ* )
9	2	uzssd3	⊢ ( 𝑗 ∈ 𝑍 → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
11	8 10	fssresd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ* )
12	11	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ* )
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐹 ⇝ 𝐴 )
15	2	fvexi	⊢ 𝑍 ∈ V
16	15	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
17	3 16	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
18		climres	⊢ ( ( 𝑗 ∈ ℤ ∧ 𝐹 ∈ V ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
19	5 17 18	syl2anr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
20	14 19	mpbird	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ⇝ 𝐴 )
21	20	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ⇝ 𝐴 )
22	6 7 12 13 21	climxlim2lem	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ~~>* 𝐴 )
23	2 3	fuzxrpmcn	⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
25	5	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ℤ )
26	24 25	xlimres	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ~~>* 𝐴 ) )
27	26	adantr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ~~>* 𝐴 ) )
28	22 27	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ ) → 𝐹 ~~>* 𝐴 )
29	3	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
30		climcl	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
31	4 30	syl	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
32		breldmg	⊢ ( ( 𝐹 ∈ V ∧ 𝐴 ∈ ℂ ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ∈ dom ⇝ )
33	17 31 4 32	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
34	1 2 29 33	climrescn	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℂ )
35	28 34	r19.29a	⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )