| Step | Hyp | Ref
| Expression |
| 1 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑗𝐹 |
| 2 | | limsupmnfuzlem.2 |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 3 | | uzssre 12900 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
| 4 | 2, 3 | eqsstri 4030 |
. . . 4
⊢ 𝑍 ⊆
ℝ |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑍 ⊆ ℝ) |
| 6 | | limsupmnfuzlem.3 |
. . 3
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
| 7 | 1, 5, 6 | limsupmnf 45736 |
. 2
⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔
∀𝑥 ∈ ℝ
∃𝑘 ∈ ℝ
∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 8 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗)) |
| 9 | 8 | imbi1d 341 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → ((𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 10 | 9 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → (∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 11 | 10 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑘 ∈
ℝ ∀𝑗 ∈
𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∃𝑖 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 12 | 11 | biimpi 216 |
. . . . . 6
⊢
(∃𝑘 ∈
ℝ ∀𝑗 ∈
𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) → ∃𝑖 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 13 | | iftrue 4531 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ≤ (⌈‘𝑖) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) = (⌈‘𝑖)) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑀 ≤ (⌈‘𝑖)) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) = (⌈‘𝑖)) |
| 15 | | limsupmnfuzlem.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑀 ≤ (⌈‘𝑖)) → 𝑀 ∈ ℤ) |
| 17 | | ceilcl 13882 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℝ →
(⌈‘𝑖) ∈
ℤ) |
| 18 | 17 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑀 ≤ (⌈‘𝑖)) → (⌈‘𝑖) ∈ ℤ) |
| 19 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑀 ≤ (⌈‘𝑖)) → 𝑀 ≤ (⌈‘𝑖)) |
| 20 | 2, 16, 18, 19 | eluzd 45420 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑀 ≤ (⌈‘𝑖)) → (⌈‘𝑖) ∈ 𝑍) |
| 21 | 14, 20 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑀 ≤ (⌈‘𝑖)) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ∈ 𝑍) |
| 22 | | iffalse 4534 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑀 ≤ (⌈‘𝑖) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) = 𝑀) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ ¬ 𝑀 ≤ (⌈‘𝑖)) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) = 𝑀) |
| 24 | 15, 2 | uzidd2 45427 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
| 25 | 24 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ ¬ 𝑀 ≤ (⌈‘𝑖)) → 𝑀 ∈ 𝑍) |
| 26 | 23, 25 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ ¬ 𝑀 ≤ (⌈‘𝑖)) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ∈ 𝑍) |
| 27 | 21, 26 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ∈ 𝑍) |
| 28 | 27 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ∈ 𝑍) |
| 29 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗𝜑 |
| 30 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑖 ∈ ℝ |
| 31 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) |
| 32 | 29, 30, 31 | nf3an 1901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 33 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑖 ∈ ℝ) |
| 34 | 4, 27 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ∈ ℝ) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ∈ ℝ) |
| 36 | | eluzelre 12889 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) → 𝑗 ∈ ℝ) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑗 ∈ ℝ) |
| 38 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → 𝑖 ∈ ℝ) |
| 39 | 17 | zred 12722 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℝ →
(⌈‘𝑖) ∈
ℝ) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (⌈‘𝑖) ∈
ℝ) |
| 41 | | ceilge 13885 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℝ → 𝑖 ≤ (⌈‘𝑖)) |
| 42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → 𝑖 ≤ (⌈‘𝑖)) |
| 43 | 4, 24 | sselid 3981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → 𝑀 ∈ ℝ) |
| 45 | | max2 13229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧
(⌈‘𝑖) ∈
ℝ) → (⌈‘𝑖) ≤ if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) |
| 46 | 44, 40, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (⌈‘𝑖) ≤ if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) |
| 47 | 38, 40, 34, 42, 46 | letrd 11418 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → 𝑖 ≤ if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑖 ≤ if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) |
| 49 | | eluzle 12891 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ≤ 𝑗) |
| 50 | 49 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) ≤ 𝑗) |
| 51 | 33, 35, 37, 48, 50 | letrd 11418 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑖 ≤ 𝑗) |
| 52 | 51 | 3adantl3 1169 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑖 ≤ 𝑗) |
| 53 | | simpl3 1194 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 54 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑀 ∈ ℤ) |
| 55 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) → 𝑗 ∈ ℤ) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑗 ∈ ℤ) |
| 57 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑀 ∈ ℝ) |
| 58 | | max1 13227 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℝ ∧
(⌈‘𝑖) ∈
ℝ) → 𝑀 ≤
if(𝑀 ≤
(⌈‘𝑖),
(⌈‘𝑖), 𝑀)) |
| 59 | 43, 39, 58 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑀 ≤ if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) |
| 61 | 57, 35, 37, 60, 50 | letrd 11418 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑀 ≤ 𝑗) |
| 62 | 2, 54, 56, 61 | eluzd 45420 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑗 ∈ 𝑍) |
| 63 | 62 | 3adantl3 1169 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → 𝑗 ∈ 𝑍) |
| 64 | | rspa 3248 |
. . . . . . . . . . . . . 14
⊢
((∀𝑗 ∈
𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ∧ 𝑗 ∈ 𝑍) → (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 65 | 53, 63, 64 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 66 | 52, 65 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) ∧ 𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) → (𝐹‘𝑗) ≤ 𝑥) |
| 67 | 66 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → (𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀)) → (𝐹‘𝑗) ≤ 𝑥)) |
| 68 | 32, 67 | ralrimi 3257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → ∀𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))(𝐹‘𝑗) ≤ 𝑥) |
| 69 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) → (ℤ≥‘𝑘) =
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))) |
| 70 | 69 | raleqdv 3326 |
. . . . . . . . . . 11
⊢ (𝑘 = if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀) → (∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))(𝐹‘𝑗) ≤ 𝑥)) |
| 71 | 70 | rspcev 3622 |
. . . . . . . . . 10
⊢
((if(𝑀 ≤
(⌈‘𝑖),
(⌈‘𝑖), 𝑀) ∈ 𝑍 ∧ ∀𝑗 ∈
(ℤ≥‘if(𝑀 ≤ (⌈‘𝑖), (⌈‘𝑖), 𝑀))(𝐹‘𝑗) ≤ 𝑥) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) |
| 72 | 28, 68, 71 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℝ ∧ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) |
| 73 | 72 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ ℝ → (∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥))) |
| 74 | 73 | rexlimdv 3153 |
. . . . . . 7
⊢ (𝜑 → (∃𝑖 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
| 75 | 74 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑖 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) |
| 76 | 12, 75 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) |
| 77 | 76 | ex 412 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
| 78 | | rexss 4059 |
. . . . . . . 8
⊢ (𝑍 ⊆ ℝ →
(∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 ↔ ∃𝑘 ∈ ℝ (𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥))) |
| 79 | 4, 78 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑘 ∈
𝑍 ∀𝑗 ∈
(ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 ↔ ∃𝑘 ∈ ℝ (𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
| 80 | 79 | biimpi 216 |
. . . . . 6
⊢
(∃𝑘 ∈
𝑍 ∀𝑗 ∈
(ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 → ∃𝑘 ∈ ℝ (𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
| 81 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗 𝑘 ∈ 𝑍 |
| 82 | | nfra1 3284 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 |
| 83 | 81, 82 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) |
| 84 | | simp1r 1199 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) |
| 85 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
| 86 | 2 | eluzelz2 45414 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
| 87 | 86 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → 𝑘 ∈ ℤ) |
| 88 | 2 | eluzelz2 45414 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
| 89 | 88 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ ℤ) |
| 90 | | simp3 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → 𝑘 ≤ 𝑗) |
| 91 | 85, 87, 89, 90 | eluzd 45420 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ (ℤ≥‘𝑘)) |
| 92 | 91 | 3adant1r 1178 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → 𝑗 ∈ (ℤ≥‘𝑘)) |
| 93 | | rspa 3248 |
. . . . . . . . . . . 12
⊢
((∀𝑗 ∈
(ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑗) ≤ 𝑥) |
| 94 | 84, 92, 93 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑥) |
| 95 | 94 | 3exp 1120 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) → (𝑗 ∈ 𝑍 → (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 96 | 83, 95 | ralrimi 3257 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) → ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 97 | 96 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) → ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 98 | 97 | reximdv 3170 |
. . . . . . 7
⊢ (𝜑 → (∃𝑘 ∈ ℝ (𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 99 | 98 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℝ (𝑘 ∈ 𝑍 ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 100 | 80, 99 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
| 101 | 100 | ex 412 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
| 102 | 77, 101 | impbid 212 |
. . 3
⊢ (𝜑 → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
| 103 | 102 | ralbidv 3178 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
| 104 | 7, 103 | bitrd 279 |
1
⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔
∀𝑥 ∈ ℝ
∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |