| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sge0seq.z | . . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 2 |  | sge0seq.m | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 3 |  | rge0ssre 13496 | . . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ | 
| 4 |  | sge0seq.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) | 
| 5 | 4 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞)) | 
| 6 | 3, 5 | sselid 3981 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) | 
| 7 |  | readdcl 11238 | . . . . . . . 8
⊢ ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ) | 
| 8 | 7 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ) | 
| 9 | 1, 2, 6, 8 | seqf 14064 | . . . . . 6
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) | 
| 10 |  | sge0seq.g | . . . . . . . 8
⊢ 𝐺 = seq𝑀( + , 𝐹) | 
| 11 | 10 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝐺 = seq𝑀( + , 𝐹)) | 
| 12 | 11 | feq1d 6720 | . . . . . 6
⊢ (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ)) | 
| 13 | 9, 12 | mpbird 257 | . . . . 5
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) | 
| 14 | 13 | frnd 6744 | . . . 4
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) | 
| 15 |  | ressxr 11305 | . . . . 5
⊢ ℝ
⊆ ℝ* | 
| 16 | 15 | a1i 11 | . . . 4
⊢ (𝜑 → ℝ ⊆
ℝ*) | 
| 17 | 14, 16 | sstrd 3994 | . . 3
⊢ (𝜑 → ran 𝐺 ⊆
ℝ*) | 
| 18 | 1 | fvexi 6920 | . . . . 5
⊢ 𝑍 ∈ V | 
| 19 | 18 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑍 ∈ V) | 
| 20 |  | icossicc 13476 | . . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) | 
| 21 | 20 | a1i 11 | . . . . 5
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) | 
| 22 | 4, 21 | fssd 6753 | . . . 4
⊢ (𝜑 → 𝐹:𝑍⟶(0[,]+∞)) | 
| 23 | 19, 22 | sge0xrcl 46400 | . . 3
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) | 
| 24 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺) | 
| 25 | 13 | ffnd 6737 | . . . . . . . 8
⊢ (𝜑 → 𝐺 Fn 𝑍) | 
| 26 |  | fvelrnb 6969 | . . . . . . . 8
⊢ (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) | 
| 27 | 25, 26 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) | 
| 28 | 27 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) | 
| 29 | 24, 28 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧) | 
| 30 | 20, 5 | sselid 3981 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,]+∞)) | 
| 31 |  | elfzuz 13560 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) | 
| 32 | 31, 1 | eleqtrrdi 2852 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) | 
| 33 | 32 | ssriv 3987 | . . . . . . . . . . . 12
⊢ (𝑀...𝑗) ⊆ 𝑍 | 
| 34 | 33 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀...𝑗) ⊆ 𝑍) | 
| 35 | 19, 30, 34 | sge0lessmpt 46414 | . . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 36 | 35 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 37 |  | fzfid 14014 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀...𝑗) ∈ Fin) | 
| 38 | 32, 5 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ (0[,)+∞)) | 
| 39 | 37, 38 | sge0fsummpt 46405 | . . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 40 | 39 | 3ad2ant1 1134 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 41 |  | simpll 767 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑) | 
| 42 | 32 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘 ∈ 𝑍) | 
| 43 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 44 | 41, 42, 43 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 45 | 1 | eleq2i 2833 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) | 
| 46 | 45 | biimpi 216 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) | 
| 48 | 6 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) | 
| 49 | 41, 42, 48 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) | 
| 50 | 44, 47, 49 | fsumser 15766 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) | 
| 51 | 50 | 3adant3 1133 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) | 
| 52 | 40, 51 | eqtrd 2777 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = (seq𝑀( + , 𝐹)‘𝑗)) | 
| 53 | 10 | eqcomi 2746 | . . . . . . . . . . . . 13
⊢ seq𝑀( + , 𝐹) = 𝐺 | 
| 54 | 53 | fveq1i 6907 | . . . . . . . . . . . 12
⊢ (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗) | 
| 55 | 54 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗)) | 
| 56 |  | simp3 1139 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧) | 
| 57 | 52, 55, 56 | 3eqtrrd 2782 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 =
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘)))) | 
| 58 | 4 | feqmptd 6977 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) | 
| 59 | 58 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 60 | 59 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 61 | 57, 60 | breq12d 5156 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝑧 ≤
(Σ^‘𝐹) ↔
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))) | 
| 62 | 36, 61 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤
(Σ^‘𝐹)) | 
| 63 | 62 | 3exp 1120 | . . . . . . 7
⊢ (𝜑 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) | 
| 64 | 63 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) | 
| 65 | 64 | rexlimdv 3153 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹))) | 
| 66 | 29, 65 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤
(Σ^‘𝐹)) | 
| 67 | 66 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹)) | 
| 68 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) | 
| 69 | 18 | a1i 11 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑍 ∈ V) | 
| 70 | 5 | ad4ant14 752 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞)) | 
| 71 |  | simplr 769 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 ∈ ℝ) | 
| 72 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 <
(Σ^‘𝐹)) | 
| 73 | 59 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 <
(Σ^‘𝐹)) →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 74 | 72, 73 | breqtrd 5169 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 <
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 75 | 74 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → 𝑧 <
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) | 
| 76 | 68, 69, 70, 71, 75 | sge0gtfsumgt 46458 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → ∃𝑤 ∈ (𝒫 𝑍 ∩ Fin)𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) | 
| 77 | 2 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → 𝑀 ∈ ℤ) | 
| 78 |  | elpwinss 45054 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → 𝑤 ⊆ 𝑍) | 
| 79 | 78 | 3ad2ant2 1135 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → 𝑤 ⊆ 𝑍) | 
| 80 |  | elinel2 4202 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → 𝑤 ∈ Fin) | 
| 81 | 80 | 3ad2ant2 1135 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → 𝑤 ∈ Fin) | 
| 82 | 77, 1, 79, 81 | uzfissfz 45337 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → ∃𝑗 ∈ 𝑍 𝑤 ⊆ (𝑀...𝑗)) | 
| 83 | 82 | 3adant1r 1178 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → ∃𝑗 ∈ 𝑍 𝑤 ⊆ (𝑀...𝑗)) | 
| 84 |  | simpl1r 1226 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑧 ∈ ℝ) | 
| 85 | 80 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑤 ∈ Fin) | 
| 86 | 58, 6 | fmpt3d 7136 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) | 
| 87 | 86 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑤) → 𝐹:𝑍⟶ℝ) | 
| 88 | 78 | sselda 3983 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑤) → 𝑘 ∈ 𝑍) | 
| 89 | 88 | adantll 714 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑤) → 𝑘 ∈ 𝑍) | 
| 90 | 87, 89 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑤) → (𝐹‘𝑘) ∈ ℝ) | 
| 91 | 85, 90 | fsumrecl 15770 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ∈ ℝ) | 
| 92 | 91 | ad4ant13 751 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ∈ ℝ) | 
| 93 | 92 | 3adantl3 1169 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ∈ ℝ) | 
| 94 | 32, 6 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ) | 
| 95 | 37, 94 | fsumrecl 15770 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ℝ) | 
| 96 | 95 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ℝ) | 
| 97 | 96 | 3adantl3 1169 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ℝ) | 
| 98 |  | simpl3 1194 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) | 
| 99 | 37 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) → (𝑀...𝑗) ∈ Fin) | 
| 100 | 94 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ) | 
| 101 |  | 0xr 11308 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ* | 
| 102 | 101 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ∈
ℝ*) | 
| 103 |  | pnfxr 11315 | . . . . . . . . . . . . . . . . . . . . 21
⊢ +∞
∈ ℝ* | 
| 104 | 103 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) | 
| 105 |  | icogelb 13438 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑘)) | 
| 106 | 102, 104,
5, 105 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) | 
| 107 | 32, 106 | sylan2 593 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → 0 ≤ (𝐹‘𝑘)) | 
| 108 | 107 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) ∧ 𝑘 ∈ (𝑀...𝑗)) → 0 ≤ (𝐹‘𝑘)) | 
| 109 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑤 ⊆ (𝑀...𝑗)) | 
| 110 | 99, 100, 108, 109 | fsumless 15832 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ≤ Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 111 | 110 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ≤ Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 112 | 111 | 3ad2antl1 1186 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) ≤ Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 113 | 84, 93, 97, 98, 112 | ltletrd 11421 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) ∧ 𝑤 ⊆ (𝑀...𝑗)) → 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 114 | 113 | ex 412 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → (𝑤 ⊆ (𝑀...𝑗) → 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) | 
| 115 | 114 | reximdv 3170 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → (∃𝑗 ∈ 𝑍 𝑤 ⊆ (𝑀...𝑗) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) | 
| 116 | 83, 115 | mpd 15 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑤 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘)) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 117 | 116 | 3exp 1120 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → (𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)))) | 
| 118 | 117 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → (𝑤 ∈ (𝒫 𝑍 ∩ Fin) → (𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)))) | 
| 119 | 118 | rexlimdv 3153 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → (∃𝑤 ∈ (𝒫 𝑍 ∩ Fin)𝑧 < Σ𝑘 ∈ 𝑤 (𝐹‘𝑘) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) | 
| 120 | 76, 119 | mpd 15 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → ∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 121 | 9 | ffnd 6737 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → seq𝑀( + , 𝐹) Fn 𝑍) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → seq𝑀( + , 𝐹) Fn 𝑍) | 
| 123 | 47, 45 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) | 
| 124 |  | fnfvelrn 7100 | . . . . . . . . . . . . . 14
⊢
((seq𝑀( + , 𝐹) Fn 𝑍 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ran seq𝑀( + , 𝐹)) | 
| 125 | 122, 123,
124 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ran seq𝑀( + , 𝐹)) | 
| 126 | 10 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐺 = seq𝑀( + , 𝐹)) | 
| 127 | 126 | rneqd 5949 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ran 𝐺 = ran seq𝑀( + , 𝐹)) | 
| 128 | 50, 127 | eleq12d 2835 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺 ↔ (seq𝑀( + , 𝐹)‘𝑗) ∈ ran seq𝑀( + , 𝐹))) | 
| 129 | 125, 128 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺) | 
| 130 | 129 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺) | 
| 131 | 130 | 3adant3 1133 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺) | 
| 132 |  | simp3 1139 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) | 
| 133 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑦 = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → (𝑧 < 𝑦 ↔ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))) | 
| 134 | 133 | rspcev 3622 | . . . . . . . . . 10
⊢
((Σ𝑘 ∈
(𝑀...𝑗)(𝐹‘𝑘) ∈ ran 𝐺 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦) | 
| 135 | 131, 132,
134 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑗 ∈ 𝑍 ∧ 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦) | 
| 136 | 135 | 3exp 1120 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑗 ∈ 𝑍 → (𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦))) | 
| 137 | 136 | rexlimdv 3153 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) | 
| 138 | 137 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → (∃𝑗 ∈ 𝑍 𝑧 < Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) | 
| 139 | 120, 138 | mpd 15 | . . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ) ∧ 𝑧 <
(Σ^‘𝐹)) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦) | 
| 140 | 139 | ex 412 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝑧 <
(Σ^‘𝐹) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) | 
| 141 | 140 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑧 ∈ ℝ (𝑧 <
(Σ^‘𝐹) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦)) | 
| 142 |  | supxr2 13356 | . . 3
⊢ (((ran
𝐺 ⊆
ℝ* ∧ (Σ^‘𝐹) ∈ ℝ*)
∧ (∀𝑧 ∈ ran
𝐺 𝑧 ≤
(Σ^‘𝐹) ∧ ∀𝑧 ∈ ℝ (𝑧 <
(Σ^‘𝐹) → ∃𝑦 ∈ ran 𝐺 𝑧 < 𝑦))) → sup(ran 𝐺, ℝ*, < ) =
(Σ^‘𝐹)) | 
| 143 | 17, 23, 67, 141, 142 | syl22anc 839 | . 2
⊢ (𝜑 → sup(ran 𝐺, ℝ*, < ) =
(Σ^‘𝐹)) | 
| 144 | 143 | eqcomd 2743 | 1
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran 𝐺, ℝ*, <
)) |