Step | Hyp | Ref
| Expression |
1 | | sge0seq.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | sge0seq.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | rge0ssre 12151 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
4 | | sge0seq.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) |
5 | 4 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
6 | 3, 5 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
7 | | readdcl 9898 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ) |
9 | 1, 2, 6, 8 | seqf 12684 |
. . . . . 6
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
10 | | sge0seq.g |
. . . . . . . 8
⊢ 𝐺 = seq𝑀( + , 𝐹) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = seq𝑀( + , 𝐹)) |
12 | 11 | feq1d 5943 |
. . . . . 6
⊢ (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ)) |
13 | 9, 12 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) |
14 | | frn 5966 |
. . . . 5
⊢ (𝐺:𝑍⟶ℝ → ran 𝐺 ⊆ ℝ) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
16 | | ressxr 9962 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ⊆
ℝ*) |
18 | 15, 17 | sstrd 3578 |
. . 3
⊢ (𝜑 → ran 𝐺 ⊆
ℝ*) |
19 | | fvex 6113 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ∈ V |
20 | 1, 19 | eqeltri 2684 |
. . . . 5
⊢ 𝑍 ∈ V |
21 | 20 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ V) |
22 | | icossicc 12131 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) |
24 | 4, 23 | fssd 5970 |
. . . 4
⊢ (𝜑 → 𝐹:𝑍⟶(0[,]+∞)) |
25 | 21, 24 | sge0xrcl 39278 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) |
26 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺) |
27 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐺:𝑍⟶ℝ → 𝐺 Fn 𝑍) |
28 | 13, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Fn 𝑍) |
29 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
32 | 26, 31 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧) |
33 | 22, 5 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
34 | | elfzuz 12209 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) |
35 | 34, 1 | syl6eleqr 2699 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) |
36 | 35 | ssriv 3572 |
. . . . . . . . . . . 12
⊢ (𝑀...𝑗) ⊆ 𝑍 |
37 | 36 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀...𝑗) ⊆ 𝑍) |
38 | 21, 33, 37 | sge0lessmpt 39292 |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
39 | 38 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
40 | | fzfid 12634 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...𝑗) ∈ Fin) |
41 | 35, 5 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
42 | 40, 41 | sge0fsummpt 39283 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
43 | 42 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
44 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑) |
45 | 35 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘 ∈ 𝑍) |
46 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
47 | 44, 45, 46 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
48 | 1 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
49 | 48 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
51 | 6 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
52 | 44, 45, 51 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
53 | 47, 50, 52 | fsumser 14308 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) |
54 | 53 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) |
55 | 43, 54 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = (seq𝑀( + , 𝐹)‘𝑗)) |
56 | 10 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ seq𝑀( + , 𝐹) = 𝐺 |
57 | 56 | fveq1i 6104 |
. . . . . . . . . . . 12
⊢ (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗) |
58 | 57 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗)) |
59 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧) |
60 | 55, 58, 59 | 3eqtrrd 2649 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 =
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘)))) |
61 | 4 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
63 | 62 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
64 | 60, 63 | breq12d 4596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝑧 ≤
(Σ^‘𝐹) ↔
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))) |
65 | 39, 64 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤
(Σ^‘𝐹)) |
66 | 65 | 3exp 1256 |
. . . . . . 7
⊢ (𝜑 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) |
67 | 66 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) |
68 | 67 | rexlimdv 3012 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹))) |
69 | 32, 68 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤
(Σ^‘𝐹)) |
70 | 69 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹)) |
71 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) |
72 | 20 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑍 ∈ V) |
73 | 5 | ad4ant14 1285 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
74 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 ∈ ℝ) |
75 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 <
(Σ^‘𝐹)) |
76 | 62 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 <
(Σ^‘𝐹)) →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
77 | 75, 76 | breqtrd 4609 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 <
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
78 | 77 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 <
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
79 | 71, 72, 73, 74, 78 | sge0gtfsumgt 39336 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → ∃𝑤 ∈ (𝒫 𝑍 ∩ Fin)𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) |
80 | 2 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → 𝑀 ∈ ℤ) |
81 | | elpwinss 38241 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → 𝑤 ⊆ 𝑍) |
82 | 81 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → 𝑤 ⊆ 𝑍) |
83 | | elinel2 3762 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → 𝑤 ∈ Fin) |
84 | 83 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → 𝑤 ∈ Fin) |
85 | 80, 1, 82, 84 | uzfissfz 38483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → ∃𝑗 ∈ 𝑍 𝑤 ⊆ (𝑀...𝑗)) |
86 | 85 | 3adant1r 1311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → ∃𝑗 ∈ 𝑍 𝑤 ⊆ (𝑀...𝑗)) |
87 | | simpl1r 1106 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑧 ∈ ℝ) |
88 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑤 ∈ Fin) |
89 | 61, 6 | fmpt3d 6293 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
90 | 89 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑤) → 𝐹:𝑍⟶ℝ) |
91 | 81 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑤) → 𝑘 ∈ 𝑍) |
92 | 91 | adantll 746 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑤) → 𝑘 ∈ 𝑍) |
93 | 90, 92 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑤) → (𝐹‘𝑘) ∈ ℝ) |
94 | 88, 93 | fsumrecl 14312 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ∈ ℝ) |
95 | 94 | ad4ant13 1284 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ∈ ℝ) |
96 | 95 | 3adantl3 1212 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ∈ ℝ) |
97 | 35, 6 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
98 | 40, 97 | fsumrecl 14312 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ℝ) |
99 | 98 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ℝ) |
100 | 99 | 3adantl3 1212 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ℝ) |
101 | | simpl3 1059 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) |
102 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) → (𝑀...𝑗) ∈ Fin) |
103 | 97 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
104 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ* |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ∈
ℝ*) |
106 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ +∞
∈ ℝ* |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
108 | | icogelb 12096 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑘)) |
109 | 105, 107,
5, 108 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) |
110 | 35, 109 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → 0 ≤ (𝐹‘𝑘)) |
111 | 110 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) ∧ 𝑘 ∈ (𝑀...𝑗)) → 0 ≤ (𝐹‘𝑘)) |
112 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑤 ⊆ (𝑀...𝑗)) |
113 | 102, 103,
111, 112 | fsumless 14369 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ≤ Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
114 | 113 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ≤ Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
115 | 114 | 3ad2antl1 1216 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ≤ Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
116 | 87, 96, 100, 101, 115 | ltletrd 10076 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
117 | 116 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → (𝑤 ⊆ (𝑀...𝑗) → 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) |
118 | 117 | reximdv 2999 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → (∃𝑗 ∈ 𝑍 𝑤 ⊆ (𝑀...𝑗) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) |
119 | 86, 118 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
120 | 119 | 3exp 1256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → (𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)))) |
121 | 120 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → (𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)))) |
122 | 121 | rexlimdv 3012 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → (∃𝑤 ∈ (𝒫 𝑍 ∩ Fin)𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) |
123 | 79, 122 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
124 | 9 | ffnd 5959 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → seq𝑀( + , 𝐹) Fn 𝑍) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → seq𝑀( + , 𝐹) Fn 𝑍) |
126 | 50, 48 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
127 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢
((seq𝑀( + , 𝐹) Fn 𝑍 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ran seq𝑀( + , 𝐹)) |
128 | 125, 126,
127 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ran seq𝑀( + , 𝐹)) |
129 | 10 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐺 = seq𝑀( + , 𝐹)) |
130 | 129 | rneqd 5274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ran 𝐺 = ran seq𝑀( + , 𝐹)) |
131 | 53, 130 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺 ↔ (seq𝑀( + , 𝐹)‘𝑗) ∈ ran seq𝑀( + , 𝐹))) |
132 | 128, 131 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺) |
133 | 132 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺) |
134 | 133 | 3adant3 1074 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺) |
135 | | simp3 1056 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
136 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → (𝑧 < 𝑦 ↔ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) |
137 | 136 | rspcev 3282 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
(𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦) |
138 | 134, 135,
137 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦) |
139 | 138 | 3exp 1256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑗 ∈ 𝑍 → (𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦))) |
140 | 139 | rexlimdv 3012 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) |
141 | 140 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → (∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) |
142 | 123, 141 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦) |
143 | 142 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑧 <
(Σ^‘𝐹) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) |
144 | 143 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 <
(Σ^‘𝐹) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) |
145 | | supxr2 12016 |
. . 3
⊢ (((ran
𝐺 ⊆
ℝ* ∧ (Σ^‘𝐹) ∈ ℝ*)
∧ (∀𝑧 ∈ ran
𝐺 𝑧 ≤
(Σ^‘𝐹) ∧ ∀𝑧 ∈ ℝ (𝑧 <
(Σ^‘𝐹) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦))) → sup(ran 𝐺, ℝ*, < ) =
(Σ^‘𝐹)) |
146 | 18, 25, 70, 144, 145 | syl22anc 1319 |
. 2
⊢ (𝜑 → sup(ran 𝐺, ℝ*, < ) =
(Σ^‘𝐹)) |
147 | 146 | eqcomd 2616 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran 𝐺, ℝ*, <
)) |