Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimxrre.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimxrre.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
xlimxrre.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
xlimxrre.c ⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )
Assertion xlimxrre ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 xlimxrre.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 xlimxrre.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimxrre.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 xlimxrre.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5 xlimxrre.c ⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )
6 elioore ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
7 6 anim2i ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
8 7 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
10 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
11 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
12 10 11 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) )
14 9 13 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
15 14 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
16 peano2rem ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
17 4 16 syl ⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℝ )
18 17 rexrd ⊢ ( 𝜑 → ( 𝐴 − 1 ) ∈ ℝ* )
19 peano2re ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
20 4 19 syl ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ )
21 20 rexrd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ* )
22 4 ltm1d ⊢ ( 𝜑 → ( 𝐴 − 1 ) < 𝐴 )
23 4 ltp1d ⊢ ( 𝜑 → 𝐴 < ( 𝐴 + 1 ) )
24 18 21 4 22 23 eliood ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) )
25 iooordt ⊢ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ∈ ( ordTop ‘ ≤ )
26 nfcv ⊢ Ⅎ 𝑘 𝐹
27 eqid ⊢ ( ordTop ‘ ≤ ) = ( ordTop ‘ ≤ )
28 26 1 2 3 27 xlimbr ⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐴 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝐴 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
29 5 28 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝐴 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
30 29 simprd ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝐴 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
31 eleq2 ⊢ ( 𝑢 = ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ( 𝐴 ∈ 𝑢 ↔ 𝐴 ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) )
32 eleq2 ⊢ ( 𝑢 = ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) )
33 32 anbi2d ⊢ ( 𝑢 = ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) )
34 33 rexralbidv ⊢ ( 𝑢 = ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) )
35 31 34 imbi12d ⊢ ( 𝑢 = ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ( ( 𝐴 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ↔ ( 𝐴 ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) ) )
36 35 rspcva ⊢ ( ( ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ∈ ( ordTop ‘ ≤ ) ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( 𝐴 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ( 𝐴 ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) )
37 25 30 36 sylancr ⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) ) )
38 24 37 mpd ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 − 1 ) (,) ( 𝐴 + 1 ) ) ) )
39 15 38 reximddv ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )