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	$⊢ R = \underset{t}{⇝} (topGen (ran (.)))$
	climreeq.2	$⊢ Z = ℤ_{\geq M}$
	climreeq.3	$⊢ φ \to M \in ℤ$
	climreeq.4	$⊢ φ \to F : Z ⟶ ℝ$
Assertion	climreeq	$⊢ φ \to (F R A \leftrightarrow F ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		climreeq.1	$⊢ R = \underset{t}{⇝} (topGen (ran (.)))$
2		climreeq.2	$⊢ Z = ℤ_{\geq M}$
3		climreeq.3	$⊢ φ \to M \in ℤ$
4		climreeq.4	$⊢ φ \to F : Z ⟶ ℝ$
5	1	breqi	$⊢ F R A \leftrightarrow F \underset{t}{⇝} (topGen (ran (.))) A$
6		ax-resscn	$⊢ ℝ \subseteq ℂ$
7	6	a1i	$⊢ φ \to ℝ \subseteq ℂ$
8	4 7	fssd	$⊢ φ \to F : Z ⟶ ℂ$
9		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
10	9 2	lmclimf	$⊢ (M \in ℤ \land F : Z ⟶ ℂ) \to (F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A \leftrightarrow F ⇝ A)$
11	3 8 10	syl2anc	$⊢ φ \to (F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A \leftrightarrow F ⇝ A)$
12	9	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
13		reex	$⊢ ℝ \in V$
14	13	a1i	$⊢ (φ \land A \in ℝ) \to ℝ \in V$
15	9	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
16	15	a1i	$⊢ (φ \land A \in ℝ) \to TopOpen (ℂ_{fld}) \in Top$
17		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
18	3	adantr	$⊢ (φ \land A \in ℝ) \to M \in ℤ$
19	4	adantr	$⊢ (φ \land A \in ℝ) \to F : Z ⟶ ℝ$
20	12 2 14 16 17 18 19	lmss	$⊢ (φ \land A \in ℝ) \to (F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A \leftrightarrow F \underset{t}{⇝} (topGen (ran (.))) A)$
21	20	pm5.32da	$⊢ φ \to ((A \in ℝ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \leftrightarrow (A \in ℝ \land F \underset{t}{⇝} (topGen (ran (.))) A))$
22		simpr	$⊢ (A \in ℝ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \to F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A$
23	3	adantr	$⊢ (φ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \to M \in ℤ$
24	11	biimpa	$⊢ (φ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \to F ⇝ A$
25	4	ffvelcdmda	$⊢ (φ \land n \in Z) \to F (n) \in ℝ$
26	25	adantlr	$⊢ ((φ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \land n \in Z) \to F (n) \in ℝ$
27	2 23 24 26	climrecl	$⊢ (φ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \to A \in ℝ$
28	27	ex	$⊢ φ \to (F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A \to A \in ℝ)$
29	28	ancrd	$⊢ φ \to (F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A \to (A \in ℝ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A))$
30	22 29	impbid2	$⊢ φ \to ((A \in ℝ \land F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A) \leftrightarrow F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A)$
31		simpr	$⊢ (A \in ℝ \land F \underset{t}{⇝} (topGen (ran (.))) A) \to F \underset{t}{⇝} (topGen (ran (.))) A$
32		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
33	32	a1i	$⊢ (φ \land F \underset{t}{⇝} (topGen (ran (.))) A) \to topGen (ran (.)) \in TopOn (ℝ)$
34		simpr	$⊢ (φ \land F \underset{t}{⇝} (topGen (ran (.))) A) \to F \underset{t}{⇝} (topGen (ran (.))) A$
35		lmcl	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land F \underset{t}{⇝} (topGen (ran (.))) A) \to A \in ℝ$
36	33 34 35	syl2anc	$⊢ (φ \land F \underset{t}{⇝} (topGen (ran (.))) A) \to A \in ℝ$
37	36	ex	$⊢ φ \to (F \underset{t}{⇝} (topGen (ran (.))) A \to A \in ℝ)$
38	37	ancrd	$⊢ φ \to (F \underset{t}{⇝} (topGen (ran (.))) A \to (A \in ℝ \land F \underset{t}{⇝} (topGen (ran (.))) A))$
39	31 38	impbid2	$⊢ φ \to ((A \in ℝ \land F \underset{t}{⇝} (topGen (ran (.))) A) \leftrightarrow F \underset{t}{⇝} (topGen (ran (.))) A)$
40	21 30 39	3bitr3d	$⊢ φ \to (F \underset{t}{⇝} (TopOpen (ℂ_{fld})) A \leftrightarrow F \underset{t}{⇝} (topGen (ran (.))) A)$
41	11 40	bitr3d	$⊢ φ \to (F ⇝ A \leftrightarrow F \underset{t}{⇝} (topGen (ran (.))) A)$
42	5 41	bitr4id	$⊢ φ \to (F R A \leftrightarrow F ⇝ A)$

Metamath Proof Explorer

Theorem climreeq

Proof