Proof of Theorem liminfltlem
| Step | Hyp | Ref
| Expression |
| 1 | | nfmpt1 5250 |
. . 3
⊢
Ⅎ𝑘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) |
| 2 | | liminfltlem.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 3 | | liminfltlem.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 4 | | liminfltlem.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
| 5 | 4 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
| 6 | 5 | renegcld 11690 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -(𝐹‘𝑘) ∈ ℝ) |
| 7 | 6 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)):𝑍⟶ℝ) |
| 8 | 3 | fvexi 6920 |
. . . . . . 7
⊢ 𝑍 ∈ V |
| 9 | 8 | mptex 7243 |
. . . . . 6
⊢ (𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)) ∈ V |
| 10 | 9 | limsupcli 45772 |
. . . . 5
⊢ (lim
sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ∈
ℝ* |
| 11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ∈
ℝ*) |
| 12 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
| 13 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑘𝐹 |
| 14 | 12, 13, 2, 3, 4 | liminfvaluz4 45814 |
. . . . 5
⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim
sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)))) |
| 15 | | liminfltlem.r |
. . . . 5
⊢ (𝜑 → (lim inf‘𝐹) ∈
ℝ) |
| 16 | 14, 15 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → -𝑒(lim
sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ∈ ℝ) |
| 17 | 11, 16 | xnegrecl2d 45478 |
. . 3
⊢ (𝜑 → (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ∈ ℝ) |
| 18 | | liminfltlem.x |
. . 3
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
| 19 | 1, 2, 3, 7, 17, 18 | limsupgt 45793 |
. 2
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) < (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)))) |
| 20 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
| 21 | 3 | uztrn2 12897 |
. . . . . 6
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 22 | 21 | adantll 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 23 | | negex 11506 |
. . . . . . . . . . 11
⊢ -(𝐹‘𝑘) ∈ V |
| 24 | | fvmpt4 45244 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ 𝑍 ∧ -(𝐹‘𝑘) ∈ V) → ((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) = -(𝐹‘𝑘)) |
| 25 | 23, 24 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) = -(𝐹‘𝑘)) |
| 26 | 25 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) = -(𝐹‘𝑘)) |
| 27 | 26 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) = (-(𝐹‘𝑘) − 𝑋)) |
| 28 | 5 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
| 29 | 18 | rpred 13077 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑋 ∈ ℝ) |
| 31 | 30 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑋 ∈ ℂ) |
| 32 | 28, 31 | negdi2d 11634 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -((𝐹‘𝑘) + 𝑋) = (-(𝐹‘𝑘) − 𝑋)) |
| 33 | 27, 32 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) = -((𝐹‘𝑘) + 𝑋)) |
| 34 | 17 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ∈ ℂ) |
| 35 | 17 | rexnegd 45148 |
. . . . . . . . . . 11
⊢ (𝜑 → -𝑒(lim
sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) = -(lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)))) |
| 36 | 14, 35 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ (𝜑 → -(lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) = (lim inf‘𝐹)) |
| 37 | 34, 36 | negcon1ad 11615 |
. . . . . . . . 9
⊢ (𝜑 → -(lim inf‘𝐹) = (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘)))) |
| 38 | 37 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) = -(lim inf‘𝐹)) |
| 39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) = -(lim inf‘𝐹)) |
| 40 | 33, 39 | breq12d 5156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) < (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ↔ -((𝐹‘𝑘) + 𝑋) < -(lim inf‘𝐹))) |
| 41 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (lim inf‘𝐹) ∈ ℝ) |
| 42 | 5, 30 | readdcld 11290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) + 𝑋) ∈ ℝ) |
| 43 | 41, 42 | ltnegd 11841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋) ↔ -((𝐹‘𝑘) + 𝑋) < -(lim inf‘𝐹))) |
| 44 | 40, 43 | bitr4d 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) < (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ↔ (lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋))) |
| 45 | 20, 22, 44 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) < (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ↔ (lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋))) |
| 46 | 45 | ralbidva 3176 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) < (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋))) |
| 47 | 46 | rexbidva 3177 |
. 2
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))‘𝑘) − 𝑋) < (lim sup‘(𝑘 ∈ 𝑍 ↦ -(𝐹‘𝑘))) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋))) |
| 48 | 19, 47 | mpbid 232 |
1
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(lim inf‘𝐹) < ((𝐹‘𝑘) + 𝑋)) |