Metamath Proof Explorer

Theorem liminflimsupclim

Description: A sequence of real numbers converges if its inferior limit is real, and it is greater than or equal to the superior limit (in such a case, they are actually equal, see liminflelimsupuz ). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminflimsupclim.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminflimsupclim.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminflimsupclim.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
liminflimsupclim.4 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ )
liminflimsupclim.5 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
Assertion liminflimsupclim ( 𝜑 → 𝐹 ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 liminflimsupclim.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 liminflimsupclim.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 liminflimsupclim.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 liminflimsupclim.4 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ )
5 liminflimsupclim.5 ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
6 climrel ⊢ Rel ⇝
7 6 a1i ⊢ ( 𝜑 → Rel ⇝ )
8 2 fvexi ⊢ 𝑍 ∈ V
9 8 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
10 3 9 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
11 10 limsupcld ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
12 4 rexrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
13 3 frexr ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
14 1 2 13 liminflelimsupuz ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
15 11 12 5 14 xrletrid ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = ( lim inf ‘ 𝐹 ) )
16 15 4 eqeltrd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
17 16 recnd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℂ )
18 nfcv ⊢ Ⅎ 𝑘 𝐹
19 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
20 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ℝ )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
23 18 19 2 20 21 22 liminflt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑥 ) )
24 21 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
25 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
26 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
27 26 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
28 25 27 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
29 28 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
30 22 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ+ )
31 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
32 30 31 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
33 24 29 32 ltsubadd2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ↔ ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑥 ) ) )
34 33 bicomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑥 ) ↔ ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
35 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
36 15 eqcomd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
37 36 17 eqeltrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℂ )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( lim inf ‘ 𝐹 ) ∈ ℂ )
39 35 38 negsubdi2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → - ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) = ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) )
40 39 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( - ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) < 𝑥 ↔ ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
41 40 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( - ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) < 𝑥 ↔ ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
42 41 bicomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ↔ - ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) < 𝑥 ) )
43 29 24 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ∈ ℝ )
44 ltnegcon1 ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( - ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) < 𝑥 ↔ - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ) )
45 43 32 44 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( - ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) < 𝑥 ↔ - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ) )
46 42 45 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( lim inf ‘ 𝐹 ) − ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ↔ - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ) )
47 36 oveq2d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) )
48 47 breq2d ⊢ ( 𝜑 → ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ↔ - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) )
49 48 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim inf ‘ 𝐹 ) ) ↔ - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) )
50 34 46 49 3bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑥 ) ↔ - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) )
51 50 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) )
52 51 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( lim inf ‘ 𝐹 ) < ( ( 𝐹 ‘ 𝑘 ) + 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) )
53 23 52 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) )
54 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
55 18 19 2 20 54 22 limsupgt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − 𝑥 ) < ( lim sup ‘ 𝐹 ) )
56 54 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
57 ltsub23 ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑘 ) − 𝑥 ) < ( lim sup ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
58 29 32 56 57 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) − 𝑥 ) < ( lim sup ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
59 58 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − 𝑥 ) < ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
60 59 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − 𝑥 ) < ( lim sup ‘ 𝐹 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
61 55 60 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 )
62 53 61 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
63 2 rexanuz2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
64 62 63 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
65 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 )
66 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ+ )
67 26 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
68 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ) → ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) )
69 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
70 16 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
71 69 70 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∈ ℝ )
72 71 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∈ ℝ )
73 31 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑥 ∈ ℝ )
74 abslt ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ↔ ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ) )
75 72 73 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ↔ ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ) )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ↔ ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ) )
77 68 76 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 )
78 77 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ) )
79 65 66 67 78 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ) )
80 79 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ) )
81 80 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( - 𝑥 < ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ) )
82 64 81 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 )
83 82 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 )
84 17 83 jca ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ) )
85 ax-resscn ⊢ ℝ ⊆ ℂ
86 85 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
87 3 86 fssd ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
88 18 1 2 87 climuz ⊢ ( 𝜑 → ( 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ↔ ( ( lim sup ‘ 𝐹 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( lim sup ‘ 𝐹 ) ) ) < 𝑥 ) ) )
89 84 88 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )
90 releldm ⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) → 𝐹 ∈ dom ⇝ )
91 7 89 90 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )