Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝜑) |
2 | | liminflimsupxrre.2 |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | 2 | uztrn2 12355 |
. . . . . . 7
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ 𝑍) |
4 | 3 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ 𝑍) |
5 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
6 | | liminflimsupxrre.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
7 | 6 | fdmd 6525 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝑍) |
8 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → dom 𝐹 = 𝑍) |
9 | 5, 8 | eleqtrrd 2837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ dom 𝐹) |
10 | 9 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) ∧ -∞ < (𝐹‘𝑗)) → 𝑗 ∈ dom 𝐹) |
11 | 6 | ffvelrnda 6873 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈
ℝ*) |
12 | 11 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) ∧ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ∈
ℝ*) |
13 | | mnfxr 10788 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
14 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -∞ < (𝐹‘𝑗)) → -∞ ∈
ℝ*) |
15 | 11 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ∈
ℝ*) |
16 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -∞ < (𝐹‘𝑗)) → -∞ < (𝐹‘𝑗)) |
17 | 14, 15, 16 | xrgtned 42439 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ≠ -∞) |
18 | 17 | adantlr 715 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) ∧ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ≠ -∞) |
19 | 11 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) → (𝐹‘𝑗) ∈
ℝ*) |
20 | | pnfxr 10785 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) → +∞ ∈
ℝ*) |
22 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) → (𝐹‘𝑗) < +∞) |
23 | 19, 21, 22 | xrltned 42474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) → (𝐹‘𝑗) ≠ +∞) |
24 | 23 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) ∧ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ≠ +∞) |
25 | 12, 18, 24 | xrred 42482 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) ∧ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ∈ ℝ) |
26 | 10, 25 | jca 515 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝐹‘𝑗) < +∞) ∧ -∞ < (𝐹‘𝑗)) → (𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ)) |
27 | 26 | expl 461 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗)) → (𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ))) |
28 | 1, 4, 27 | syl2anc 587 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗)) → (𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ))) |
29 | 28 | ralimdva 3092 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗)) → ∀𝑗 ∈ (ℤ≥‘𝑘)(𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ))) |
30 | 29 | imp 410 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗))) → ∀𝑗 ∈ (ℤ≥‘𝑘)(𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ)) |
31 | 6 | ffund 6518 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
32 | | ffvresb 6910 |
. . . . 5
⊢ (Fun
𝐹 → ((𝐹 ↾
(ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ ↔
∀𝑗 ∈
(ℤ≥‘𝑘)(𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ))) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ ↔
∀𝑗 ∈
(ℤ≥‘𝑘)(𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ))) |
34 | 33 | ad2antrr 726 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗))) → ((𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ ↔
∀𝑗 ∈
(ℤ≥‘𝑘)(𝑗 ∈ dom 𝐹 ∧ (𝐹‘𝑗) ∈ ℝ))) |
35 | 30, 34 | mpbird 260 |
. 2
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗))) → (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ) |
36 | | nfv 1921 |
. . . 4
⊢
Ⅎ𝑗𝜑 |
37 | | nfcv 2900 |
. . . 4
⊢
Ⅎ𝑗𝐹 |
38 | | liminflimsupxrre.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
39 | | liminflimsupxrre.4 |
. . . 4
⊢ (𝜑 → (lim sup‘𝐹) ≠
+∞) |
40 | 36, 37, 38, 2, 6, 39 | limsupubuz2 42936 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) < +∞) |
41 | | liminflimsupxrre.5 |
. . . 4
⊢ (𝜑 → (lim inf‘𝐹) ≠
-∞) |
42 | 36, 37, 38, 2, 6, 41 | liminflbuz2 42938 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-∞ < (𝐹‘𝑗)) |
43 | 2 | rexanuz2 14811 |
. . 3
⊢
(∃𝑘 ∈
𝑍 ∀𝑗 ∈
(ℤ≥‘𝑘)((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗)) ↔ (∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) < +∞ ∧ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-∞ < (𝐹‘𝑗))) |
44 | 40, 42, 43 | sylanbrc 586 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝐹‘𝑗) < +∞ ∧ -∞ < (𝐹‘𝑗))) |
45 | 35, 44 | reximddv3 42278 |
1
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶ℝ) |