| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sge0uzfsumgt.p | . . 3
⊢
Ⅎ𝑘𝜑 | 
| 2 |  | sge0uzfsumgt.z | . . . . 5
⊢ 𝑍 =
(ℤ≥‘𝐾) | 
| 3 | 2 | fvexi 6920 | . . . 4
⊢ 𝑍 ∈ V | 
| 4 | 3 | a1i 11 | . . 3
⊢ (𝜑 → 𝑍 ∈ V) | 
| 5 |  | sge0uzfsumgt.b | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) | 
| 6 |  | sge0uzfsumgt.c | . . 3
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 7 |  | sge0uzfsumgt.l | . . 3
⊢ (𝜑 → 𝐶 <
(Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵))) | 
| 8 | 1, 4, 5, 6, 7 | sge0gtfsumgt 46458 | . 2
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝐶 < Σ𝑘 ∈ 𝑥 𝐵) | 
| 9 |  | sge0uzfsumgt.h | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 10 | 9 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → 𝐾 ∈ ℤ) | 
| 11 |  | elpwinss 45054 | . . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → 𝑥 ⊆ 𝑍) | 
| 12 | 11 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → 𝑥 ⊆ 𝑍) | 
| 13 |  | elinel2 4202 | . . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → 𝑥 ∈ Fin) | 
| 14 | 13 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → 𝑥 ∈ Fin) | 
| 15 | 10, 2, 12, 14 | uzfissfz 45337 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑚 ∈ 𝑍 𝑥 ⊆ (𝐾...𝑚)) | 
| 16 | 6 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝐶 ∈ ℝ) | 
| 17 |  | nfv 1914 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑥 ⊆ (𝐾...𝑚) | 
| 18 | 1, 17 | nfan 1899 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) | 
| 19 |  | fzfid 14014 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → (𝐾...𝑚) ∈ Fin) | 
| 20 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝑥 ⊆ (𝐾...𝑚)) | 
| 21 | 19, 20 | ssfid 9301 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝑥 ∈ Fin) | 
| 22 |  | simpll 767 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ 𝑥) → 𝜑) | 
| 23 | 20 | sselda 3983 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ (𝐾...𝑚)) | 
| 24 |  | rge0ssre 13496 | . . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ ℝ | 
| 25 |  | fzssuz 13605 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾...𝑚) ⊆ (ℤ≥‘𝐾) | 
| 26 | 25, 2 | sseqtrri 4033 | . . . . . . . . . . . . . . . 16
⊢ (𝐾...𝑚) ⊆ 𝑍 | 
| 27 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝐾...𝑚) → 𝑘 ∈ (𝐾...𝑚)) | 
| 28 | 26, 27 | sselid 3981 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐾...𝑚) → 𝑘 ∈ 𝑍) | 
| 29 | 28, 5 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 𝐵 ∈ (0[,)+∞)) | 
| 30 | 24, 29 | sselid 3981 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 𝐵 ∈ ℝ) | 
| 31 | 22, 23, 30 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ ℝ) | 
| 32 | 18, 21, 31 | fsumreclf 45591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ∈ ℝ) | 
| 33 | 32 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ∈ ℝ) | 
| 34 |  | fzfid 14014 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐾...𝑚) ∈ Fin) | 
| 35 | 1, 34, 30 | fsumreclf 45591 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (𝐾...𝑚)𝐵 ∈ ℝ) | 
| 36 | 35 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ (𝐾...𝑚)𝐵 ∈ ℝ) | 
| 37 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) | 
| 38 | 30 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ (𝐾...𝑚)) → 𝐵 ∈ ℝ) | 
| 39 |  | 0xr 11308 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ* | 
| 40 | 39 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 0 ∈
ℝ*) | 
| 41 |  | pnfxr 11315 | . . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* | 
| 42 | 41 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → +∞ ∈
ℝ*) | 
| 43 |  | icogelb 13438 | . . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐵 ∈ (0[,)+∞))
→ 0 ≤ 𝐵) | 
| 44 | 40, 42, 29, 43 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 0 ≤ 𝐵) | 
| 45 | 44 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ (𝐾...𝑚)) → 0 ≤ 𝐵) | 
| 46 | 18, 19, 38, 45, 20 | fsumlessf 45592 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ≤ Σ𝑘 ∈ (𝐾...𝑚)𝐵) | 
| 47 | 46 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ≤ Σ𝑘 ∈ (𝐾...𝑚)𝐵) | 
| 48 | 16, 33, 36, 37, 47 | ltletrd 11421 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) | 
| 49 | 48 | ex 412 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → (𝑥 ⊆ (𝐾...𝑚) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) | 
| 50 | 49 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑚 ∈ 𝑍) → (𝑥 ⊆ (𝐾...𝑚) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) | 
| 51 | 50 | 3adantl2 1168 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑚 ∈ 𝑍) → (𝑥 ⊆ (𝐾...𝑚) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) | 
| 52 | 51 | reximdva 3168 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → (∃𝑚 ∈ 𝑍 𝑥 ⊆ (𝐾...𝑚) → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) | 
| 53 | 15, 52 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) | 
| 54 | 53 | 3exp 1120 | . . 3
⊢ (𝜑 → (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → (𝐶 < Σ𝑘 ∈ 𝑥 𝐵 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵))) | 
| 55 | 54 | rexlimdv 3153 | . 2
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝐶 < Σ𝑘 ∈ 𝑥 𝐵 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) | 
| 56 | 8, 55 | mpd 15 | 1
⊢ (𝜑 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) |