| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | climrel 15529 | . . 3
⊢ Rel
⇝ | 
| 2 | 1 | a1i 11 | . 2
⊢ (𝜑 → Rel ⇝
) | 
| 3 |  | liminflimsupclim.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) | 
| 4 |  | liminflimsupclim.2 | . . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 5 | 4 | fvexi 6919 | . . . . . . . . . 10
⊢ 𝑍 ∈ V | 
| 6 | 5 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ V) | 
| 7 | 3, 6 | fexd 7248 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ V) | 
| 8 | 7 | limsupcld 45710 | . . . . . . 7
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ*) | 
| 9 |  | liminflimsupclim.4 | . . . . . . . 8
⊢ (𝜑 → (lim inf‘𝐹) ∈
ℝ) | 
| 10 | 9 | rexrd 11312 | . . . . . . 7
⊢ (𝜑 → (lim inf‘𝐹) ∈
ℝ*) | 
| 11 |  | liminflimsupclim.5 | . . . . . . 7
⊢ (𝜑 → (lim sup‘𝐹) ≤ (lim inf‘𝐹)) | 
| 12 |  | liminflimsupclim.1 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 13 | 3 | frexr 45401 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) | 
| 14 | 12, 4, 13 | liminflelimsupuz 45805 | . . . . . . 7
⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹)) | 
| 15 | 8, 10, 11, 14 | xrletrid 13198 | . . . . . 6
⊢ (𝜑 → (lim sup‘𝐹) = (lim inf‘𝐹)) | 
| 16 | 15, 9 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ) | 
| 17 | 16 | recnd 11290 | . . . 4
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℂ) | 
| 18 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑘𝐹 | 
| 19 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) | 
| 20 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶ℝ) | 
| 21 | 9 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (lim
inf‘𝐹) ∈
ℝ) | 
| 22 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 23 | 18, 19, 4, 20, 21, 22 | liminflt 45825 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑥)) | 
| 24 | 21 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (lim inf‘𝐹) ∈
ℝ) | 
| 25 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:𝑍⟶ℝ) | 
| 26 | 4 | uztrn2 12898 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) | 
| 27 | 26 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) | 
| 28 | 25, 27 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) | 
| 29 | 28 | adantllr 719 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) | 
| 30 | 22 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ+) | 
| 31 |  | rpre 13044 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) | 
| 33 | 24, 29, 32 | ltsubadd2d 11862 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((lim inf‘𝐹) − (𝐹‘𝑘)) < 𝑥 ↔ (lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑥))) | 
| 34 | 33 | bicomd 223 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑥) ↔ ((lim inf‘𝐹) − (𝐹‘𝑘)) < 𝑥)) | 
| 35 | 28 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℂ) | 
| 36 | 15 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (lim inf‘𝐹) = (lim sup‘𝐹)) | 
| 37 | 36, 17 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (lim inf‘𝐹) ∈
ℂ) | 
| 38 | 37 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (lim inf‘𝐹) ∈
ℂ) | 
| 39 | 35, 38 | negsubdi2d 11637 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → -((𝐹‘𝑘) − (lim inf‘𝐹)) = ((lim inf‘𝐹) − (𝐹‘𝑘))) | 
| 40 | 39 | breq1d 5152 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (-((𝐹‘𝑘) − (lim inf‘𝐹)) < 𝑥 ↔ ((lim inf‘𝐹) − (𝐹‘𝑘)) < 𝑥)) | 
| 41 | 40 | adantllr 719 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (-((𝐹‘𝑘) − (lim inf‘𝐹)) < 𝑥 ↔ ((lim inf‘𝐹) − (𝐹‘𝑘)) < 𝑥)) | 
| 42 | 41 | bicomd 223 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((lim inf‘𝐹) − (𝐹‘𝑘)) < 𝑥 ↔ -((𝐹‘𝑘) − (lim inf‘𝐹)) < 𝑥)) | 
| 43 | 29, 24 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) − (lim inf‘𝐹)) ∈ ℝ) | 
| 44 |  | ltnegcon1 11765 | . . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑘) − (lim inf‘𝐹)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (-((𝐹‘𝑘) − (lim inf‘𝐹)) < 𝑥 ↔ -𝑥 < ((𝐹‘𝑘) − (lim inf‘𝐹)))) | 
| 45 | 43, 32, 44 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (-((𝐹‘𝑘) − (lim inf‘𝐹)) < 𝑥 ↔ -𝑥 < ((𝐹‘𝑘) − (lim inf‘𝐹)))) | 
| 46 | 42, 45 | bitrd 279 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((lim inf‘𝐹) − (𝐹‘𝑘)) < 𝑥 ↔ -𝑥 < ((𝐹‘𝑘) − (lim inf‘𝐹)))) | 
| 47 | 36 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝑘) − (lim inf‘𝐹)) = ((𝐹‘𝑘) − (lim sup‘𝐹))) | 
| 48 | 47 | breq2d 5154 | . . . . . . . . . . . . 13
⊢ (𝜑 → (-𝑥 < ((𝐹‘𝑘) − (lim inf‘𝐹)) ↔ -𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)))) | 
| 49 | 48 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (-𝑥 < ((𝐹‘𝑘) − (lim inf‘𝐹)) ↔ -𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)))) | 
| 50 | 34, 46, 49 | 3bitrd 305 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑥) ↔ -𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)))) | 
| 51 | 50 | ralbidva 3175 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑥) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)))) | 
| 52 | 51 | rexbidva 3176 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑥) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)))) | 
| 53 | 23, 52 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹))) | 
| 54 | 16 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (lim
sup‘𝐹) ∈
ℝ) | 
| 55 | 18, 19, 4, 20, 54, 22 | limsupgt 45798 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑥) < (lim sup‘𝐹)) | 
| 56 | 54 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (lim sup‘𝐹) ∈
ℝ) | 
| 57 |  | ltsub23 11744 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (lim sup‘𝐹) ∈ ℝ) →
(((𝐹‘𝑘) − 𝑥) < (lim sup‘𝐹) ↔ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 58 | 29, 32, 56, 57 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘) − 𝑥) < (lim sup‘𝐹) ↔ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 59 | 58 | ralbidva 3175 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑥) < (lim sup‘𝐹) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 60 | 59 | rexbidva 3176 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − 𝑥) < (lim sup‘𝐹) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 61 | 55, 60 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥) | 
| 62 | 53, 61 | jca 511 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 63 | 4 | rexanuz2 15389 | . . . . . . 7
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 64 | 62, 63 | sylibr 234 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 65 |  | simplll 774 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) | 
| 66 |  | simpllr 775 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ+) | 
| 67 | 26 | adantll 714 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) | 
| 68 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) ∧ (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) → (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) | 
| 69 | 3 | ffvelcdmda 7103 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) | 
| 70 | 16 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (lim sup‘𝐹) ∈ ℝ) | 
| 71 | 69, 70 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) − (lim sup‘𝐹)) ∈ ℝ) | 
| 72 | 71 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) − (lim sup‘𝐹)) ∈ ℝ) | 
| 73 | 31 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ ℝ) | 
| 74 |  | abslt 15354 | . . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑘) − (lim sup‘𝐹)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥 ↔ (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥))) | 
| 75 | 72, 73, 74 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥 ↔ (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥))) | 
| 76 | 75 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) ∧ (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) → ((abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥 ↔ (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥))) | 
| 77 | 68, 76 | mpbird 257 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) ∧ (-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥)) → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥) | 
| 78 | 77 | ex 412 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥) → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥)) | 
| 79 | 65, 66, 67, 78 | syl21anc 837 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥) → (abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥)) | 
| 80 | 79 | ralimdva 3166 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥)) | 
| 81 | 80 | reximdva 3167 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(-𝑥 < ((𝐹‘𝑘) − (lim sup‘𝐹)) ∧ ((𝐹‘𝑘) − (lim sup‘𝐹)) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥)) | 
| 82 | 64, 81 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥) | 
| 83 | 82 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥) | 
| 84 | 17, 83 | jca 511 | . . 3
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℂ ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥)) | 
| 85 |  | ax-resscn 11213 | . . . . . 6
⊢ ℝ
⊆ ℂ | 
| 86 | 85 | a1i 11 | . . . . 5
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 87 | 3, 86 | fssd 6752 | . . . 4
⊢ (𝜑 → 𝐹:𝑍⟶ℂ) | 
| 88 | 18, 12, 4, 87 | climuz 45764 | . . 3
⊢ (𝜑 → (𝐹 ⇝ (lim sup‘𝐹) ↔ ((lim sup‘𝐹) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (lim sup‘𝐹))) < 𝑥))) | 
| 89 | 84, 88 | mpbird 257 | . 2
⊢ (𝜑 → 𝐹 ⇝ (lim sup‘𝐹)) | 
| 90 |  | releldm 5954 | . 2
⊢ ((Rel
⇝ ∧ 𝐹 ⇝
(lim sup‘𝐹)) →
𝐹 ∈ dom ⇝
) | 
| 91 | 2, 89, 90 | syl2anc 584 | 1
⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |