| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑙𝜑 |
| 2 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑙𝐹 |
| 3 | | liminfpnfuz.2 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 4 | | liminfpnfuz.3 |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 5 | | liminfpnfuz.4 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
| 6 | 1, 2, 3, 4, 5 | liminfvaluz3 45811 |
. . . 4
⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim
sup‘(𝑙 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑙)))) |
| 7 | | liminfpnfuz.1 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝐹 |
| 8 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑙 |
| 9 | 7, 8 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝐹‘𝑙) |
| 10 | 9 | nfxneg 45472 |
. . . . . . 7
⊢
Ⅎ𝑗-𝑒(𝐹‘𝑙) |
| 11 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑙-𝑒(𝐹‘𝑗) |
| 12 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑙 = 𝑗 → (𝐹‘𝑙) = (𝐹‘𝑗)) |
| 13 | 12 | xnegeqd 45448 |
. . . . . . 7
⊢ (𝑙 = 𝑗 → -𝑒(𝐹‘𝑙) = -𝑒(𝐹‘𝑗)) |
| 14 | 10, 11, 13 | cbvmpt 5253 |
. . . . . 6
⊢ (𝑙 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑙)) = (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) |
| 15 | 14 | fveq2i 6909 |
. . . . 5
⊢ (lim
sup‘(𝑙 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑙))) = (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) |
| 16 | 15 | xnegeqi 45451 |
. . . 4
⊢
-𝑒(lim sup‘(𝑙 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑙))) = -𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) |
| 17 | 6, 16 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗)))) |
| 18 | 17 | eqeq1d 2739 |
. 2
⊢ (𝜑 → ((lim inf‘𝐹) = +∞ ↔
-𝑒(lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = +∞)) |
| 19 | | xnegmnf 13252 |
. . . . . 6
⊢
-𝑒-∞ = +∞ |
| 20 | 19 | eqcomi 2746 |
. . . . 5
⊢ +∞
= -𝑒-∞ |
| 21 | 20 | a1i 11 |
. . . 4
⊢ (𝜑 → +∞ =
-𝑒-∞) |
| 22 | 21 | eqeq2d 2748 |
. . 3
⊢ (𝜑 → (-𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) = +∞ ↔
-𝑒(lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) =
-𝑒-∞)) |
| 23 | 4 | fvexi 6920 |
. . . . . . 7
⊢ 𝑍 ∈ V |
| 24 | 23 | mptex 7243 |
. . . . . 6
⊢ (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) ∈ V |
| 25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) ∈ V) |
| 26 | 25 | limsupcld 45705 |
. . . 4
⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) ∈
ℝ*) |
| 27 | | mnfxr 11318 |
. . . 4
⊢ -∞
∈ ℝ* |
| 28 | | xneg11 13257 |
. . . 4
⊢ (((lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) ∈ ℝ* ∧ -∞
∈ ℝ*) → (-𝑒(lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -𝑒-∞ ↔
(lim sup‘(𝑗 ∈
𝑍 ↦
-𝑒(𝐹‘𝑗))) = -∞)) |
| 29 | 26, 27, 28 | sylancl 586 |
. . 3
⊢ (𝜑 → (-𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) = -𝑒-∞ ↔
(lim sup‘(𝑗 ∈
𝑍 ↦
-𝑒(𝐹‘𝑗))) = -∞)) |
| 30 | 22, 29 | bitrd 279 |
. 2
⊢ (𝜑 → (-𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) = +∞ ↔ (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -∞)) |
| 31 | 4 | uztrn2 12897 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ 𝑍) |
| 32 | | xnegex 13250 |
. . . . . . . . 9
⊢
-𝑒(𝐹‘𝑗) ∈ V |
| 33 | | fvmpt4 45244 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑍 ∧ -𝑒(𝐹‘𝑗) ∈ V) → ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) = -𝑒(𝐹‘𝑗)) |
| 34 | 31, 32, 33 | sylancl 586 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) = -𝑒(𝐹‘𝑗)) |
| 35 | 34 | breq1d 5153 |
. . . . . . 7
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) ≤ 𝑥 ↔ -𝑒(𝐹‘𝑗) ≤ 𝑥)) |
| 36 | 35 | ralbidva 3176 |
. . . . . 6
⊢ (𝑘 ∈ 𝑍 → (∀𝑗 ∈ (ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥)) |
| 37 | 36 | rexbiia 3092 |
. . . . 5
⊢
(∃𝑘 ∈
𝑍 ∀𝑗 ∈
(ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) ≤ 𝑥 ↔ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥) |
| 38 | 37 | ralbii 3093 |
. . . 4
⊢
(∀𝑥 ∈
ℝ ∃𝑘 ∈
𝑍 ∀𝑗 ∈
(ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥) |
| 39 | 38 | a1i 11 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) ≤ 𝑥 ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥)) |
| 40 | | nfmpt1 5250 |
. . . 4
⊢
Ⅎ𝑗(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) |
| 41 | 5 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑙 ∈ 𝑍) → (𝐹‘𝑙) ∈
ℝ*) |
| 42 | 41 | xnegcld 13342 |
. . . . 5
⊢ ((𝜑 ∧ 𝑙 ∈ 𝑍) → -𝑒(𝐹‘𝑙) ∈
ℝ*) |
| 43 | 14 | eqcomi 2746 |
. . . . 5
⊢ (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) = (𝑙 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑙)) |
| 44 | 42, 43 | fmptd 7134 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)):𝑍⟶ℝ*) |
| 45 | 40, 3, 4, 44 | limsupmnfuz 45742 |
. . 3
⊢ (𝜑 → ((lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) ≤ 𝑥)) |
| 46 | 7, 4, 5 | xlimpnfxnegmnf 45829 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≤ 𝑥)) |
| 47 | 39, 45, 46 | 3bitr4d 311 |
. 2
⊢ (𝜑 → ((lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗))) |
| 48 | 18, 30, 47 | 3bitrd 305 |
1
⊢ (𝜑 → ((lim inf‘𝐹) = +∞ ↔
∀𝑥 ∈ ℝ
∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗))) |