climxrre

Description: If a sequence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued (the weaker hypothesis F e. dom ~> is probably not enough, since in principle we could have +oo e. CC and -oo e. CC ). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climxrre.m	$⊢ φ \to M \in ℤ$
	climxrre.z	$⊢ Z = ℤ_{\geq M}$
	climxrre.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	climxrre.a	$⊢ φ \to A \in ℝ$
	climxrre.c	$⊢ φ \to F ⇝ A$
Assertion	climxrre	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		climxrre.m	$⊢ φ \to M \in ℤ$
2		climxrre.z	$⊢ Z = ℤ_{\geq M}$
3		climxrre.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		climxrre.a	$⊢ φ \to A \in ℝ$
5		climxrre.c	$⊢ φ \to F ⇝ A$
6	1	ad2antrr	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to M \in ℤ$
7	3	ad2antrr	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to F : Z ⟶ ℝ^{*}$
8	5	ad2antrr	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to F ⇝ A$
9		simpr	$⊢ (φ \land +∞ \in ℂ) \to +∞ \in ℂ$
10	4	recnd	$⊢ φ \to A \in ℂ$
11	10	adantr	$⊢ (φ \land +∞ \in ℂ) \to A \in ℂ$
12	9 11	subcld	$⊢ (φ \land +∞ \in ℂ) \to +∞ - A \in ℂ$
13		renepnf	$⊢ A \in ℝ \to A \neq +∞$
14	13	necomd	$⊢ A \in ℝ \to +∞ \neq A$
15	4 14	syl	$⊢ φ \to +∞ \neq A$
16	15	adantr	$⊢ (φ \land +∞ \in ℂ) \to +∞ \neq A$
17	9 11 16	subne0d	$⊢ (φ \land +∞ \in ℂ) \to +∞ - A \neq 0$
18	12 17	absrpcld	$⊢ (φ \land +∞ \in ℂ) \to \|+∞ - A\| \in ℝ^{+}$
19	18	adantr	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to \|+∞ - A\| \in ℝ^{+}$
20		simpr	$⊢ (φ \land −∞ \in ℂ) \to −∞ \in ℂ$
21	10	adantr	$⊢ (φ \land −∞ \in ℂ) \to A \in ℂ$
22	20 21	subcld	$⊢ (φ \land −∞ \in ℂ) \to −∞ - A \in ℂ$
23	4	adantr	$⊢ (φ \land −∞ \in ℂ) \to A \in ℝ$
24		renemnf	$⊢ A \in ℝ \to A \neq −∞$
25	24	necomd	$⊢ A \in ℝ \to −∞ \neq A$
26	23 25	syl	$⊢ (φ \land −∞ \in ℂ) \to −∞ \neq A$
27	20 21 26	subne0d	$⊢ (φ \land −∞ \in ℂ) \to −∞ - A \neq 0$
28	22 27	absrpcld	$⊢ (φ \land −∞ \in ℂ) \to \|−∞ - A\| \in ℝ^{+}$
29	28	adantlr	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to \|−∞ - A\| \in ℝ^{+}$
30	19 29	ifcld	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to if (\|+∞ - A\| \leq \|−∞ - A\|, \|+∞ - A\|, \|−∞ - A\|) \in ℝ^{+}$
31	19	rpred	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to \|+∞ - A\| \in ℝ$
32	29	rpred	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to \|−∞ - A\| \in ℝ$
33	31 32	min1d	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to if (\|+∞ - A\| \leq \|−∞ - A\|, \|+∞ - A\|, \|−∞ - A\|) \leq \|+∞ - A\|$
34	33	adantr	$⊢ (((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \land +∞ \in ℂ) \to if (\|+∞ - A\| \leq \|−∞ - A\|, \|+∞ - A\|, \|−∞ - A\|) \leq \|+∞ - A\|$
35	31 32	min2d	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to if (\|+∞ - A\| \leq \|−∞ - A\|, \|+∞ - A\|, \|−∞ - A\|) \leq \|−∞ - A\|$
36	35	adantr	$⊢ (((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \land −∞ \in ℂ) \to if (\|+∞ - A\| \leq \|−∞ - A\|, \|+∞ - A\|, \|−∞ - A\|) \leq \|−∞ - A\|$
37	6 2 7 8 30 34 36	climxrrelem	$⊢ ((φ \land +∞ \in ℂ) \land −∞ \in ℂ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
38	1	ad2antrr	$⊢ ((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \to M \in ℤ$
39	3	ad2antrr	$⊢ ((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \to F : Z ⟶ ℝ^{*}$
40	5	ad2antrr	$⊢ ((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \to F ⇝ A$
41	18	adantr	$⊢ ((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \to \|+∞ - A\| \in ℝ^{+}$
42	18	rpred	$⊢ (φ \land +∞ \in ℂ) \to \|+∞ - A\| \in ℝ$
43	42	leidd	$⊢ (φ \land +∞ \in ℂ) \to \|+∞ - A\| \leq \|+∞ - A\|$
44	43	ad2antrr	$⊢ (((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \land +∞ \in ℂ) \to \|+∞ - A\| \leq \|+∞ - A\|$
45		pm2.21	$⊢ \neg −∞ \in ℂ \to (−∞ \in ℂ \to \|+∞ - A\| \leq \|−∞ - A\|)$
46	45	imp	$⊢ (\neg −∞ \in ℂ \land −∞ \in ℂ) \to \|+∞ - A\| \leq \|−∞ - A\|$
47	46	adantll	$⊢ (((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \land −∞ \in ℂ) \to \|+∞ - A\| \leq \|−∞ - A\|$
48	38 2 39 40 41 44 47	climxrrelem	$⊢ ((φ \land +∞ \in ℂ) \land \neg −∞ \in ℂ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
49	37 48	pm2.61dan	$⊢ (φ \land +∞ \in ℂ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
50	1	ad2antrr	$⊢ ((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \to M \in ℤ$
51	3	ad2antrr	$⊢ ((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \to F : Z ⟶ ℝ^{*}$
52	5	ad2antrr	$⊢ ((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \to F ⇝ A$
53	28	adantlr	$⊢ ((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \to \|−∞ - A\| \in ℝ^{+}$
54		pm2.21	$⊢ \neg +∞ \in ℂ \to (+∞ \in ℂ \to \|−∞ - A\| \leq \|+∞ - A\|)$
55	54	imp	$⊢ (\neg +∞ \in ℂ \land +∞ \in ℂ) \to \|−∞ - A\| \leq \|+∞ - A\|$
56	55	ad4ant24	$⊢ (((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \land +∞ \in ℂ) \to \|−∞ - A\| \leq \|+∞ - A\|$
57	28	rpred	$⊢ (φ \land −∞ \in ℂ) \to \|−∞ - A\| \in ℝ$
58	57	leidd	$⊢ (φ \land −∞ \in ℂ) \to \|−∞ - A\| \leq \|−∞ - A\|$
59	58	ad4ant13	$⊢ (((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \land −∞ \in ℂ) \to \|−∞ - A\| \leq \|−∞ - A\|$
60	50 2 51 52 53 56 59	climxrrelem	$⊢ ((φ \land \neg +∞ \in ℂ) \land −∞ \in ℂ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
61		nfv	$⊢ Ⅎ k ((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ)$
62		nfv	$⊢ Ⅎ k j \in Z$
63		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} F (k) \in ℂ$
64	62 63	nfan	$⊢ Ⅎ k (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)$
65	61 64	nfan	$⊢ Ⅎ k (((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ))$
66		simp-4l	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to φ$
67	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
68	67	adantlr	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ) \land k \in ℤ_{\geq j}) \to k \in Z$
69	68	adantll	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to k \in Z$
70		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
71	3	fdmd	$⊢ φ \to dom F = Z$
72	71	adantr	$⊢ (φ \land k \in Z) \to dom F = Z$
73	70 72	eleqtrrd	$⊢ (φ \land k \in Z) \to k \in dom F$
74	66 69 73	syl2anc	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to k \in dom F$
75	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ^{*}$
76	66 69 75	syl2anc	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{*}$
77		rspa	$⊢ (\forall k \in ℤ_{\geq j} F (k) \in ℂ \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
78	77	adantll	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
79	78	adantll	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
80		simpllr	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to \neg −∞ \in ℂ$
81		nelne2	$⊢ (F (k) \in ℂ \land \neg −∞ \in ℂ) \to F (k) \neq −∞$
82	79 80 81	syl2anc	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to F (k) \neq −∞$
83		simp-4r	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to \neg +∞ \in ℂ$
84		nelne2	$⊢ (F (k) \in ℂ \land \neg +∞ \in ℂ) \to F (k) \neq +∞$
85	79 83 84	syl2anc	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to F (k) \neq +∞$
86	76 82 85	xrred	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ$
87	74 86	jca	$⊢ ((((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \land k \in ℤ_{\geq j}) \to (k \in dom F \land F (k) \in ℝ)$
88	65 87	ralrimia	$⊢ (((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ)$
89	3	ffund	$⊢ φ \to Fun F$
90		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
91	89 90	syl	$⊢ φ \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
92	91	ad3antrrr	$⊢ (((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
93	88 92	mpbird	$⊢ (((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℂ)) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
94		r19.26	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < 1) \leftrightarrow (\forall k \in ℤ_{\geq j} F (k) \in ℂ \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < 1)$
95	94	simplbi	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < 1) \to \forall k \in ℤ_{\geq j} F (k) \in ℂ$
96	95	ad2antll	$⊢ (φ \land (j \in ℤ \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < 1))) \to \forall k \in ℤ_{\geq j} F (k) \in ℂ$
97		breq2	$⊢ x = 1 \to (\|F (k) - A\| < x \leftrightarrow \|F (k) - A\| < 1)$
98	97	anbi2d	$⊢ x = 1 \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - A\| < 1))$
99	98	rexralbidv	$⊢ x = 1 \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < 1))$
100	2	fvexi	$⊢ Z \in V$
101	100	a1i	$⊢ φ \to Z \in V$
102	3 101	fexd	$⊢ φ \to F \in V$
103		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
104	102 103	clim	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
105	5 104	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
106	105	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
107		1rp	$⊢ 1 \in ℝ^{+}$
108	107	a1i	$⊢ φ \to 1 \in ℝ^{+}$
109	99 106 108	rspcdva	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < 1)$
110	96 109	reximddv	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) \in ℂ$
111	2	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) \in ℂ)$
112	1 111	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) \in ℂ)$
113	110 112	mpbird	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ$
114	113	ad2antrr	$⊢ ((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ$
115	93 114	reximddv	$⊢ ((φ \land \neg +∞ \in ℂ) \land \neg −∞ \in ℂ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
116	60 115	pm2.61dan	$⊢ (φ \land \neg +∞ \in ℂ) \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
117	49 116	pm2.61dan	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$

Metamath Proof Explorer

Theorem climxrre

Proof