climxrrelem

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. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climxrrelem.m	$⊢ φ \to M \in ℤ$
	climxrrelem.z	$⊢ Z = ℤ_{\geq M}$
	climxrrelem.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	climxrrelem.c	$⊢ φ \to F ⇝ A$
	climxrrelem.d	$⊢ φ \to D \in ℝ^{+}$
	climxrrelem.p	$⊢ (φ \land +∞ \in ℂ) \to D \leq \|+∞ - A\|$
	climxrrelem.n	$⊢ (φ \land −∞ \in ℂ) \to D \leq \|−∞ - A\|$
Assertion	climxrrelem	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		climxrrelem.m	$⊢ φ \to M \in ℤ$
2		climxrrelem.z	$⊢ Z = ℤ_{\geq M}$
3		climxrrelem.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		climxrrelem.c	$⊢ φ \to F ⇝ A$
5		climxrrelem.d	$⊢ φ \to D \in ℝ^{+}$
6		climxrrelem.p	$⊢ (φ \land +∞ \in ℂ) \to D \leq \|+∞ - A\|$
7		climxrrelem.n	$⊢ (φ \land −∞ \in ℂ) \to D \leq \|−∞ - A\|$
8		nfv	$⊢ Ⅎ k φ$
9		nfv	$⊢ Ⅎ k j \in Z$
10		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D)$
11	9 10	nfan	$⊢ Ⅎ k (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))$
12	8 11	nfan	$⊢ Ⅎ k (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D)))$
13	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
14	13	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
15	3	fdmd	$⊢ φ \to dom F = Z$
16	15	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to dom F = Z$
17	14 16	eleqtrrd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in dom F$
18	17	adantlrr	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \land k \in ℤ_{\geq j}) \to k \in dom F$
19		simpll	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \land k \in ℤ_{\geq j}) \to φ$
20	14	adantlrr	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \land k \in ℤ_{\geq j}) \to k \in Z$
21		rspa	$⊢ (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - A\| < D)$
22	21	adantll	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D)) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - A\| < D)$
23	22	adantll	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - A\| < D)$
24	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ^{*}$
25	24	3adant3	$⊢ (φ \land k \in Z \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to F (k) \in ℝ^{*}$
26		simpll	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = −∞) \to φ$
27		simpr	$⊢ (F (k) \in ℂ \land F (k) = −∞) \to F (k) = −∞$
28		simpl	$⊢ (F (k) \in ℂ \land F (k) = −∞) \to F (k) \in ℂ$
29	27 28	eqeltrrd	$⊢ (F (k) \in ℂ \land F (k) = −∞) \to −∞ \in ℂ$
30	29	adantll	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = −∞) \to −∞ \in ℂ$
31	26 30 7	syl2anc	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = −∞) \to D \leq \|−∞ - A\|$
32	31	adantlrr	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = −∞) \to D \leq \|−∞ - A\|$
33		fvoveq1	$⊢ F (k) = −∞ \to \|F (k) - A\| = \|−∞ - A\|$
34	33	adantl	$⊢ (\|F (k) - A\| < D \land F (k) = −∞) \to \|F (k) - A\| = \|−∞ - A\|$
35		simpl	$⊢ (\|F (k) - A\| < D \land F (k) = −∞) \to \|F (k) - A\| < D$
36	34 35	eqbrtrrd	$⊢ (\|F (k) - A\| < D \land F (k) = −∞) \to \|−∞ - A\| < D$
37	36	adantll	$⊢ ((φ \land \|F (k) - A\| < D) \land F (k) = −∞) \to \|−∞ - A\| < D$
38	37	adantlrl	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = −∞) \to \|−∞ - A\| < D$
39	2	fvexi	$⊢ Z \in V$
40	39	a1i	$⊢ φ \to Z \in V$
41	3 40	fexd	$⊢ φ \to F \in V$
42		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
43	41 42	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)))$
44	4 43	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
45	44	simpld	$⊢ φ \to A \in ℂ$
46	45	ad2antrr	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = −∞) \to A \in ℂ$
47	30 46	subcld	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = −∞) \to −∞ - A \in ℂ$
48	47	abscld	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = −∞) \to \|−∞ - A\| \in ℝ$
49	48	adantlrr	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = −∞) \to \|−∞ - A\| \in ℝ$
50	5	rpred	$⊢ φ \to D \in ℝ$
51	50	ad2antrr	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = −∞) \to D \in ℝ$
52	49 51	ltnled	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = −∞) \to (\|−∞ - A\| < D \leftrightarrow \neg D \leq \|−∞ - A\|)$
53	38 52	mpbid	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = −∞) \to \neg D \leq \|−∞ - A\|$
54	32 53	pm2.65da	$⊢ (φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to \neg F (k) = −∞$
55	54	3adant2	$⊢ (φ \land k \in Z \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to \neg F (k) = −∞$
56	55	neqned	$⊢ (φ \land k \in Z \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to F (k) \neq −∞$
57		simpll	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = +∞) \to φ$
58		simpr	$⊢ (F (k) \in ℂ \land F (k) = +∞) \to F (k) = +∞$
59		simpl	$⊢ (F (k) \in ℂ \land F (k) = +∞) \to F (k) \in ℂ$
60	58 59	eqeltrrd	$⊢ (F (k) \in ℂ \land F (k) = +∞) \to +∞ \in ℂ$
61	60	adantll	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = +∞) \to +∞ \in ℂ$
62	57 61 6	syl2anc	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = +∞) \to D \leq \|+∞ - A\|$
63	62	adantlrr	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = +∞) \to D \leq \|+∞ - A\|$
64		fvoveq1	$⊢ F (k) = +∞ \to \|F (k) - A\| = \|+∞ - A\|$
65	64	adantl	$⊢ (\|F (k) - A\| < D \land F (k) = +∞) \to \|F (k) - A\| = \|+∞ - A\|$
66		simpl	$⊢ (\|F (k) - A\| < D \land F (k) = +∞) \to \|F (k) - A\| < D$
67	65 66	eqbrtrrd	$⊢ (\|F (k) - A\| < D \land F (k) = +∞) \to \|+∞ - A\| < D$
68	67	adantll	$⊢ ((φ \land \|F (k) - A\| < D) \land F (k) = +∞) \to \|+∞ - A\| < D$
69	68	adantlrl	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = +∞) \to \|+∞ - A\| < D$
70	45	ad2antrr	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = +∞) \to A \in ℂ$
71	61 70	subcld	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = +∞) \to +∞ - A \in ℂ$
72	71	abscld	$⊢ ((φ \land F (k) \in ℂ) \land F (k) = +∞) \to \|+∞ - A\| \in ℝ$
73	72	adantlrr	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = +∞) \to \|+∞ - A\| \in ℝ$
74	50	ad2antrr	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = +∞) \to D \in ℝ$
75	73 74	ltnled	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = +∞) \to (\|+∞ - A\| < D \leftrightarrow \neg D \leq \|+∞ - A\|)$
76	69 75	mpbid	$⊢ ((φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \land F (k) = +∞) \to \neg D \leq \|+∞ - A\|$
77	63 76	pm2.65da	$⊢ (φ \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to \neg F (k) = +∞$
78	77	3adant2	$⊢ (φ \land k \in Z \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to \neg F (k) = +∞$
79	78	neqned	$⊢ (φ \land k \in Z \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to F (k) \neq +∞$
80	25 56 79	xrred	$⊢ (φ \land k \in Z \land (F (k) \in ℂ \land \|F (k) - A\| < D)) \to F (k) \in ℝ$
81	19 20 23 80	syl3anc	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ$
82	18 81	jca	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \land k \in ℤ_{\geq j}) \to (k \in dom F \land F (k) \in ℝ)$
83	12 82	ralrimia	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ)$
84	3	ffund	$⊢ φ \to Fun F$
85		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
86	84 85	syl	$⊢ φ \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
87	86	adantr	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
88	83 87	mpbird	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
89		breq2	$⊢ x = D \to (\|F (k) - A\| < x \leftrightarrow \|F (k) - A\| < D)$
90	89	anbi2d	$⊢ x = D \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - A\| < D))$
91	90	rexralbidv	$⊢ x = D \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\| < D))$
92	44	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
93	91 92 5	rspcdva	$⊢ φ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D)$
94	2	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))$
95	1 94	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D))$
96	93 95	mpbird	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < D)$
97	88 96	reximddv	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$

Metamath Proof Explorer

Theorem climxrrelem

Proof