Theorem climreeq

Description: If F is a real function, then F converges to A with respect to the standard topology on the reals if and only if it converges to A with respect to the standard topology on complex numbers. In the theorem, R is defined to be convergence w.r.t. the standard topology on the reals and then F R A represents the statement " F converges to A , with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that A is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017)

	Ref	Expression
Hypotheses	climreeq.1	⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
	climreeq.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climreeq.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climreeq.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion	climreeq	⊢ ( 𝜑 → ( 𝐹 𝑅 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climreeq.1	⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
2		climreeq.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		climreeq.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		climreeq.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5	1	breqi	⊢ ( 𝐹 𝑅 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 )
6		ax-resscn	⊢ ℝ ⊆ ℂ
7	6	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
8	4 7	fssd	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
9		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
10	9 2	lmclimf	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
11	3 8 10	syl2anc	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
12		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
13		reex	⊢ ℝ ∈ V
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ℝ ∈ V )
15	9	cnfldtop	⊢ ( TopOpen ‘ ℂfld ) ∈ Top
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( TopOpen ‘ ℂfld ) ∈ Top )
17		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
18	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑀 ∈ ℤ )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ )
20	12 2 14 16 17 18 19	lmss	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
21	20	pm5.32da	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) ) )
22		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 )
23	3	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝑀 ∈ ℤ )
24	11	biimpa	⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝐹 ⇝ 𝐴 )
25	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
27	2 23 24 26	climrecl	⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) → 𝐴 ∈ ℝ )
28	27	ex	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 → 𝐴 ∈ ℝ ) )
29	28	ancrd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 → ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ) )
30	22 29	impbid2	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ) )
31		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 )
32		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
33	32	a1i	⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
34		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 )
35		lmcl	⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐴 ∈ ℝ )
36	33 34 35	syl2anc	⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) → 𝐴 ∈ ℝ )
37	36	ex	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 → 𝐴 ∈ ℝ ) )
38	37	ancrd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 → ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) ) )
39	31 38	impbid2	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
40	21 30 39	3bitr3d	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
41	11 40	bitr3d	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) ) 𝐴 ) )
42	5 41	bitr4id	⊢ ( 𝜑 → ( 𝐹 𝑅 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )