Step | Hyp | Ref
| Expression |
1 | | sge0uzfsumgt.p |
. . 3
⊢
Ⅎ𝑘𝜑 |
2 | | sge0uzfsumgt.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝐾) |
3 | | fvex 6113 |
. . . . 5
⊢
(ℤ≥‘𝐾) ∈ V |
4 | 2, 3 | eqeltri 2684 |
. . . 4
⊢ 𝑍 ∈ V |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑍 ∈ V) |
6 | | sge0uzfsumgt.b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ (0[,)+∞)) |
7 | | sge0uzfsumgt.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℝ) |
8 | | sge0uzfsumgt.l |
. . 3
⊢ (𝜑 → 𝐶 <
(Σ^‘(𝑘 ∈ 𝑍 ↦ 𝐵))) |
9 | 1, 5, 6, 7, 8 | sge0gtfsumgt 39336 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝐶 < Σ𝑘 ∈ 𝑥 𝐵) |
10 | | sge0uzfsumgt.h |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℤ) |
11 | 10 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → 𝐾 ∈ ℤ) |
12 | | elpwinss 38241 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → 𝑥 ⊆ 𝑍) |
13 | 12 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → 𝑥 ⊆ 𝑍) |
14 | | elinel2 3762 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → 𝑥 ∈ Fin) |
15 | 14 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → 𝑥 ∈ Fin) |
16 | 11, 2, 13, 15 | uzfissfz 38483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑚 ∈ 𝑍 𝑥 ⊆ (𝐾...𝑚)) |
17 | 7 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝐶 ∈ ℝ) |
18 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑥 ⊆ (𝐾...𝑚) |
19 | 1, 18 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) |
20 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → (𝐾...𝑚) ∈ Fin) |
21 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝑥 ⊆ (𝐾...𝑚)) |
22 | 20, 21 | ssfid 8068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝑥 ∈ Fin) |
23 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ 𝑥) → 𝜑) |
24 | 21 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ (𝐾...𝑚)) |
25 | | rge0ssre 12151 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ ℝ |
26 | | fzssuz 12253 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾...𝑚) ⊆ (ℤ≥‘𝐾) |
27 | 26, 2 | sseqtr4i 3601 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾...𝑚) ⊆ 𝑍 |
28 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝐾...𝑚) → 𝑘 ∈ (𝐾...𝑚)) |
29 | 27, 28 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐾...𝑚) → 𝑘 ∈ 𝑍) |
30 | 29, 6 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 𝐵 ∈ (0[,)+∞)) |
31 | 25, 30 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 𝐵 ∈ ℝ) |
32 | 23, 24, 31 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ ℝ) |
33 | 19, 22, 32 | fsumreclf 38643 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ∈ ℝ) |
34 | 33 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ∈ ℝ) |
35 | | fzfid 12634 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾...𝑚) ∈ Fin) |
36 | 1, 35, 31 | fsumreclf 38643 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (𝐾...𝑚)𝐵 ∈ ℝ) |
37 | 36 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ (𝐾...𝑚)𝐵 ∈ ℝ) |
38 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) |
39 | 31 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ (𝐾...𝑚)) → 𝐵 ∈ ℝ) |
40 | | 0xr 9965 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ* |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 0 ∈
ℝ*) |
42 | | pnfxr 9971 |
. . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → +∞ ∈
ℝ*) |
44 | | icogelb 12096 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐵 ∈ (0[,)+∞))
→ 0 ≤ 𝐵) |
45 | 41, 43, 30, 44 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑚)) → 0 ≤ 𝐵) |
46 | 45 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) ∧ 𝑘 ∈ (𝐾...𝑚)) → 0 ≤ 𝐵) |
47 | 19, 20, 39, 46, 21 | fsumlessf 38644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ≤ Σ𝑘 ∈ (𝐾...𝑚)𝐵) |
48 | 47 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → Σ𝑘 ∈ 𝑥 𝐵 ≤ Σ𝑘 ∈ (𝐾...𝑚)𝐵) |
49 | 17, 34, 37, 38, 48 | ltletrd 10076 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑥 ⊆ (𝐾...𝑚)) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) |
50 | 49 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → (𝑥 ⊆ (𝐾...𝑚) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) |
51 | 50 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑚 ∈ 𝑍) → (𝑥 ⊆ (𝐾...𝑚) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) |
52 | 51 | 3adantl2 1211 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) ∧ 𝑚 ∈ 𝑍) → (𝑥 ⊆ (𝐾...𝑚) → 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) |
53 | 52 | reximdva 3000 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → (∃𝑚 ∈ 𝑍 𝑥 ⊆ (𝐾...𝑚) → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) |
54 | 16, 53 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝐶 < Σ𝑘 ∈ 𝑥 𝐵) → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) |
55 | 54 | 3exp 1256 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝒫 𝑍 ∩ Fin) → (𝐶 < Σ𝑘 ∈ 𝑥 𝐵 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵))) |
56 | 55 | rexlimdv 3012 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 𝑍 ∩ Fin)𝐶 < Σ𝑘 ∈ 𝑥 𝐵 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵)) |
57 | 9, 56 | mpd 15 |
1
⊢ (𝜑 → ∃𝑚 ∈ 𝑍 𝐶 < Σ𝑘 ∈ (𝐾...𝑚)𝐵) |