Proof of Theorem liminflbuz2
| Step | Hyp | Ref
| Expression |
| 1 | | liminflbuz2.1 |
. . . . 5
⊢
Ⅎ𝑗𝜑 |
| 2 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑗 𝑘 ∈ 𝑍 |
| 3 | 1, 2 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ 𝑍) |
| 4 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝜑) |
| 5 | | liminflbuz2.4 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 6 | 5 | uztrn2 12897 |
. . . . . 6
⊢ ((𝑘 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ 𝑍) |
| 7 | 6 | adantll 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ 𝑍) |
| 8 | | liminflbuz2.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
| 9 | 8 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈
ℝ*) |
| 10 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ∈
ℝ*) |
| 11 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → -∞ ∈
ℝ*) |
| 13 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → ¬ -∞ < (𝐹‘𝑗)) |
| 14 | 10, 12, 13 | xrnltled 11329 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) ≤ -∞) |
| 15 | | xlemnf 13209 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑗) ∈ ℝ* → ((𝐹‘𝑗) ≤ -∞ ↔ (𝐹‘𝑗) = -∞)) |
| 16 | 10, 15 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → ((𝐹‘𝑗) ≤ -∞ ↔ (𝐹‘𝑗) = -∞)) |
| 17 | 14, 16 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → (𝐹‘𝑗) = -∞) |
| 18 | | xnegeq 13249 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑗) = -∞ →
-𝑒(𝐹‘𝑗) =
-𝑒-∞) |
| 19 | | xnegmnf 13252 |
. . . . . . . . . 10
⊢
-𝑒-∞ = +∞ |
| 20 | 18, 19 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝐹‘𝑗) = -∞ →
-𝑒(𝐹‘𝑗) = +∞) |
| 21 | 17, 20 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ -∞ < (𝐹‘𝑗)) → -𝑒(𝐹‘𝑗) = +∞) |
| 22 | 21 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -𝑒(𝐹‘𝑗) ≠ +∞) ∧ ¬ -∞ <
(𝐹‘𝑗)) → -𝑒(𝐹‘𝑗) = +∞) |
| 23 | | neneq 2946 |
. . . . . . . 8
⊢
(-𝑒(𝐹‘𝑗) ≠ +∞ → ¬
-𝑒(𝐹‘𝑗) = +∞) |
| 24 | 23 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -𝑒(𝐹‘𝑗) ≠ +∞) ∧ ¬ -∞ <
(𝐹‘𝑗)) → ¬ -𝑒(𝐹‘𝑗) = +∞) |
| 25 | 22, 24 | condan 818 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ -𝑒(𝐹‘𝑗) ≠ +∞) → -∞ < (𝐹‘𝑗)) |
| 26 | 25 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (-𝑒(𝐹‘𝑗) ≠ +∞ → -∞ < (𝐹‘𝑗))) |
| 27 | 4, 7, 26 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
(-𝑒(𝐹‘𝑗) ≠ +∞ → -∞ < (𝐹‘𝑗))) |
| 28 | 3, 27 | ralimdaa 3260 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≠ +∞ → ∀𝑗 ∈
(ℤ≥‘𝑘)-∞ < (𝐹‘𝑗))) |
| 29 | 28 | imp 406 |
. 2
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≠ +∞) → ∀𝑗 ∈
(ℤ≥‘𝑘)-∞ < (𝐹‘𝑗)) |
| 30 | 9 | xnegcld 13342 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → -𝑒(𝐹‘𝑗) ∈
ℝ*) |
| 31 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) →
-𝑒(𝐹‘𝑗) ∈
ℝ*) |
| 32 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) → +∞ ∈
ℝ*) |
| 34 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) = (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) |
| 35 | 34, 30 | fvmpt2d 7029 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) = -𝑒(𝐹‘𝑗)) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) → ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) = -𝑒(𝐹‘𝑗)) |
| 37 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) → ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) |
| 38 | 36, 37 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) →
-𝑒(𝐹‘𝑗) < +∞) |
| 39 | 31, 33, 38 | xrltned 45368 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) →
-𝑒(𝐹‘𝑗) ≠ +∞) |
| 40 | 39 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞ →
-𝑒(𝐹‘𝑗) ≠ +∞)) |
| 41 | 4, 7, 40 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞ →
-𝑒(𝐹‘𝑗) ≠ +∞)) |
| 42 | 3, 41 | ralimdaa 3260 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑗 ∈ (ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞ → ∀𝑗 ∈
(ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≠ +∞)) |
| 43 | 42 | imp 406 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ∀𝑗 ∈ (ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) → ∀𝑗 ∈
(ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≠ +∞) |
| 44 | | nfmpt1 5250 |
. . . 4
⊢
Ⅎ𝑗(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) |
| 45 | | liminflbuz2.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 46 | 1, 30 | fmptd2f 45240 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)):𝑍⟶ℝ*) |
| 47 | 5 | fvexi 6920 |
. . . . . . . . . . 11
⊢ 𝑍 ∈ V |
| 48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ V) |
| 49 | 8, 48 | fexd 7247 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) |
| 50 | 49 | liminfcld 45785 |
. . . . . . . 8
⊢ (𝜑 → (lim inf‘𝐹) ∈
ℝ*) |
| 51 | 50 | xnegnegd 45453 |
. . . . . . 7
⊢ (𝜑 →
-𝑒-𝑒(lim inf‘𝐹) = (lim inf‘𝐹)) |
| 52 | | liminflbuz2.2 |
. . . . . . . 8
⊢
Ⅎ𝑗𝐹 |
| 53 | 1, 52, 45, 5, 8 | liminfvaluz3 45811 |
. . . . . . 7
⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗)))) |
| 54 | 51, 53 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → -𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) =
-𝑒-𝑒(lim inf‘𝐹)) |
| 55 | 48 | mptexd 7244 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗)) ∈ V) |
| 56 | 55 | limsupcld 45705 |
. . . . . . 7
⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) ∈
ℝ*) |
| 57 | 50 | xnegcld 13342 |
. . . . . . 7
⊢ (𝜑 → -𝑒(lim
inf‘𝐹) ∈
ℝ*) |
| 58 | | xneg11 13257 |
. . . . . . 7
⊢ (((lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) ∈ ℝ* ∧
-𝑒(lim inf‘𝐹) ∈ ℝ*) →
(-𝑒(lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) =
-𝑒-𝑒(lim inf‘𝐹) ↔ (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -𝑒(lim
inf‘𝐹))) |
| 59 | 56, 57, 58 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (-𝑒(lim
sup‘(𝑗 ∈ 𝑍 ↦
-𝑒(𝐹‘𝑗))) =
-𝑒-𝑒(lim inf‘𝐹) ↔ (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -𝑒(lim
inf‘𝐹))) |
| 60 | 54, 59 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) = -𝑒(lim
inf‘𝐹)) |
| 61 | | nne 2944 |
. . . . . . 7
⊢ (¬
-𝑒(lim inf‘𝐹) ≠ +∞ ↔
-𝑒(lim inf‘𝐹) = +∞) |
| 62 | 51 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → (lim inf‘𝐹) =
-𝑒-𝑒(lim inf‘𝐹)) |
| 63 | 62 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑒(lim
inf‘𝐹) = +∞)
→ (lim inf‘𝐹) =
-𝑒-𝑒(lim inf‘𝐹)) |
| 64 | | xnegeq 13249 |
. . . . . . . . 9
⊢
(-𝑒(lim inf‘𝐹) = +∞ →
-𝑒-𝑒(lim inf‘𝐹) =
-𝑒+∞) |
| 65 | 64 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑒(lim
inf‘𝐹) = +∞)
→ -𝑒-𝑒(lim inf‘𝐹) =
-𝑒+∞) |
| 66 | | xnegpnf 13251 |
. . . . . . . . 9
⊢
-𝑒+∞ = -∞ |
| 67 | 66 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑒(lim
inf‘𝐹) = +∞)
→ -𝑒+∞ = -∞) |
| 68 | 63, 65, 67 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑒(lim
inf‘𝐹) = +∞)
→ (lim inf‘𝐹) =
-∞) |
| 69 | 61, 68 | sylan2b 594 |
. . . . . 6
⊢ ((𝜑 ∧ ¬
-𝑒(lim inf‘𝐹) ≠ +∞) → (lim inf‘𝐹) = -∞) |
| 70 | | liminflbuz2.6 |
. . . . . . . 8
⊢ (𝜑 → (lim inf‘𝐹) ≠
-∞) |
| 71 | 70 | neneqd 2945 |
. . . . . . 7
⊢ (𝜑 → ¬ (lim inf‘𝐹) = -∞) |
| 72 | 71 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬
-𝑒(lim inf‘𝐹) ≠ +∞) → ¬ (lim
inf‘𝐹) =
-∞) |
| 73 | 69, 72 | condan 818 |
. . . . 5
⊢ (𝜑 → -𝑒(lim
inf‘𝐹) ≠
+∞) |
| 74 | 60, 73 | eqnetrd 3008 |
. . . 4
⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))) ≠ +∞) |
| 75 | 1, 44, 45, 5, 46, 74 | limsupubuz2 45828 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)((𝑗 ∈ 𝑍 ↦ -𝑒(𝐹‘𝑗))‘𝑗) < +∞) |
| 76 | 43, 75 | reximddv3 3172 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-𝑒(𝐹‘𝑗) ≠ +∞) |
| 77 | 29, 76 | reximddv3 3172 |
1
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)-∞ < (𝐹‘𝑗)) |