xlimxrre

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	xlimxrre.m	$⊢ φ \to M \in ℤ$
	xlimxrre.z	$⊢ Z = ℤ_{\geq M}$
	xlimxrre.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	xlimxrre.a	$⊢ φ \to A \in ℝ$
	xlimxrre.c	$⊢ φ \to F \underset{*}{⇝} A$
Assertion	xlimxrre	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		xlimxrre.m	$⊢ φ \to M \in ℤ$
2		xlimxrre.z	$⊢ Z = ℤ_{\geq M}$
3		xlimxrre.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		xlimxrre.a	$⊢ φ \to A \in ℝ$
5		xlimxrre.c	$⊢ φ \to F \underset{*}{⇝} A$
6		elioore	$⊢ F (k) \in (A - 1, A + 1) \to F (k) \in ℝ$
7	6	anim2i	$⊢ (k \in dom F \land F (k) \in (A - 1, A + 1)) \to (k \in dom F \land F (k) \in ℝ)$
8	7	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1)) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ)$
9	8	adantl	$⊢ (φ \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1))) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ)$
10	3	ffund	$⊢ φ \to Fun F$
11		ffvresb	$⊢ Fun F \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
12	10 11	syl	$⊢ φ \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
13	12	adantr	$⊢ (φ \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1))) \to (({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℝ))$
14	9 13	mpbird	$⊢ (φ \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1))) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
15	14	adantrl	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1)))) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$
16		peano2rem	$⊢ A \in ℝ \to A - 1 \in ℝ$
17	4 16	syl	$⊢ φ \to A - 1 \in ℝ$
18	17	rexrd	$⊢ φ \to A - 1 \in ℝ^{*}$
19		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
20	4 19	syl	$⊢ φ \to A + 1 \in ℝ$
21	20	rexrd	$⊢ φ \to A + 1 \in ℝ^{*}$
22	4	ltm1d	$⊢ φ \to A - 1 < A$
23	4	ltp1d	$⊢ φ \to A < A + 1$
24	18 21 4 22 23	eliood	$⊢ φ \to A \in (A - 1, A + 1)$
25		iooordt	$⊢ (A - 1, A + 1) \in ordTop (\leq)$
26		nfcv	$⊢ \underline{Ⅎ} k F$
27		eqid	$⊢ ordTop (\leq) = ordTop (\leq)$
28	26 1 2 3 27	xlimbr	$⊢ φ \to (F \underset{}{⇝} A \leftrightarrow (A \in ℝ^{} \land \forall u \in ordTop (\leq) (A \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
29	5 28	mpbid	$⊢ φ \to (A \in ℝ^{*} \land \forall u \in ordTop (\leq) (A \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
30	29	simprd	$⊢ φ \to \forall u \in ordTop (\leq) (A \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
31		eleq2	$⊢ u = (A - 1, A + 1) \to (A \in u \leftrightarrow A \in (A - 1, A + 1))$
32		eleq2	$⊢ u = (A - 1, A + 1) \to (F (k) \in u \leftrightarrow F (k) \in (A - 1, A + 1))$
33	32	anbi2d	$⊢ u = (A - 1, A + 1) \to ((k \in dom F \land F (k) \in u) \leftrightarrow (k \in dom F \land F (k) \in (A - 1, A + 1)))$
34	33	rexralbidv	$⊢ u = (A - 1, A + 1) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1)))$
35	31 34	imbi12d	$⊢ u = (A - 1, A + 1) \to ((A \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \leftrightarrow (A \in (A - 1, A + 1) \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1))))$
36	35	rspcva	$⊢ ((A - 1, A + 1) \in ordTop (\leq) \land \forall u \in ordTop (\leq) (A \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))) \to (A \in (A - 1, A + 1) \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1)))$
37	25 30 36	sylancr	$⊢ φ \to (A \in (A - 1, A + 1) \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1)))$
38	24 37	mpd	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in (A - 1, A + 1))$
39	15 38	reximddv	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ ℝ$

Metamath Proof Explorer

Theorem xlimxrre

Proof