| Step | Hyp | Ref
| Expression |
| 1 | | sge0isum.z |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | 1 | fvexi 6920 |
. . . . 5
⊢ 𝑍 ∈ V |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ V) |
| 4 | | sge0isum.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) |
| 5 | | icossicc 13476 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) |
| 7 | 4, 6 | fssd 6753 |
. . . 4
⊢ (𝜑 → 𝐹:𝑍⟶(0[,]+∞)) |
| 8 | 3, 7 | sge0xrcl 46400 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) |
| 9 | | sge0isum.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 10 | | sge0isum.g |
. . . . . 6
⊢ 𝐺 = seq𝑀( + , 𝐹) |
| 11 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 12 | | rge0ssre 13496 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
| 13 | 4 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
| 14 | 12, 13 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
| 15 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 16 | 15 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ∈
ℝ*) |
| 17 | | pnfxr 11315 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
| 18 | 17 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
| 19 | | icogelb 13438 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑘)) |
| 20 | 16, 18, 13, 19 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) |
| 21 | | seqex 14044 |
. . . . . . . . . . 11
⊢ seq𝑀( + , 𝐹) ∈ V |
| 22 | 10, 21 | eqeltri 2837 |
. . . . . . . . . 10
⊢ 𝐺 ∈ V |
| 23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ V) |
| 24 | | sge0isum.gcnv |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ⇝ 𝐵) |
| 25 | | climcl 15535 |
. . . . . . . . . 10
⊢ (𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 27 | | breldmg 5920 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺 ⇝ 𝐵) → 𝐺 ∈ dom ⇝ ) |
| 28 | 23, 26, 24, 27 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ dom ⇝ ) |
| 29 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐺 = seq𝑀( + , 𝐹)) |
| 30 | 29 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗)) |
| 31 | 1 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
| 32 | 31 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 34 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑) |
| 35 | | elfzuz 13560 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 36 | 35, 1 | eleqtrrdi 2852 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘 ∈ 𝑍) |
| 38 | 34, 37, 14 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
| 39 | | readdcl 11238 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ) |
| 41 | 33, 38, 40 | seqcl 14063 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ) |
| 42 | 30, 41 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ∈ ℝ) |
| 43 | 42 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ∈ ℂ) |
| 44 | 43 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ∈ ℂ) |
| 45 | 1 | climbdd 15708 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧
∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥) |
| 46 | 9, 28, 44, 45 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥) |
| 47 | 42 | ad4ant13 751 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ∈ ℝ) |
| 48 | 43 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ∈ ℂ) |
| 49 | 48 | abscld 15475 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (abs‘(𝐺‘𝑗)) ∈ ℝ) |
| 50 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ) |
| 51 | 47 | leabsd 15453 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ≤ (abs‘(𝐺‘𝑗))) |
| 52 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (abs‘(𝐺‘𝑗)) ≤ 𝑥) |
| 53 | 47, 49, 50, 51, 52 | letrd 11418 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ≤ 𝑥) |
| 54 | 53 | ex 412 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → ((abs‘(𝐺‘𝑗)) ≤ 𝑥 → (𝐺‘𝑗) ≤ 𝑥)) |
| 55 | 54 | ralimdva 3167 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥 → ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥)) |
| 56 | 55 | reximdva 3168 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥)) |
| 57 | 46, 56 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) |
| 58 | 1, 10, 9, 11, 14, 20, 57 | isumsup2 15882 |
. . . . 5
⊢ (𝜑 → 𝐺 ⇝ sup(ran 𝐺, ℝ, < )) |
| 59 | 1, 9, 58, 42 | climrecl 15619 |
. . . 4
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ∈
ℝ) |
| 60 | 59 | rexrd 11311 |
. . 3
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ∈
ℝ*) |
| 61 | 4 | feqmptd 6977 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) |
| 62 | 61 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
| 63 | | mpteq1 5235 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) =
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘)))) |
| 65 | | mpt0 6710 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ∅ ↦ (𝐹‘𝑘)) = ∅ |
| 66 | 65 | fveq2i 6909 |
. . . . . . . . . . . 12
⊢
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) =
(Σ^‘∅) |
| 67 | | sge00 46391 |
. . . . . . . . . . . 12
⊢
(Σ^‘∅) = 0 |
| 68 | 66, 67 | eqtri 2765 |
. . . . . . . . . . 11
⊢
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = 0 |
| 69 | 68 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ →
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = 0) |
| 70 | 64, 69 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑦 = ∅ →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = 0) |
| 71 | 70 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = 0) |
| 72 | | 0red 11264 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
| 73 | 39 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ) |
| 74 | 1, 9, 14, 73 | seqf 14064 |
. . . . . . . . . . . . 13
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
| 75 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = seq𝑀( + , 𝐹)) |
| 76 | 75 | feq1d 6720 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ)) |
| 77 | 74, 76 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) |
| 78 | 77 | frnd 6744 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
| 79 | 77 | ffund 6740 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun 𝐺) |
| 80 | | uzid 12893 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
| 81 | 9, 80 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
| 82 | 1 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) = 𝑍 |
| 83 | 81, 82 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
| 84 | 77 | fdmd 6746 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐺 = 𝑍) |
| 85 | 84 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 = dom 𝐺) |
| 86 | 83, 85 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ dom 𝐺) |
| 87 | | fvelrn 7096 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐺 ∧ 𝑀 ∈ dom 𝐺) → (𝐺‘𝑀) ∈ ran 𝐺) |
| 88 | 79, 86, 87 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑀) ∈ ran 𝐺) |
| 89 | 78, 88 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑀) ∈ ℝ) |
| 90 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ*) |
| 91 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 92 | 4, 83 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ (0[,)+∞)) |
| 93 | | icogelb 13438 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑀) ∈ (0[,)+∞)) → 0 ≤
(𝐹‘𝑀)) |
| 94 | 90, 91, 92, 93 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (𝐹‘𝑀)) |
| 95 | 10 | fveq1i 6907 |
. . . . . . . . . . . . 13
⊢ (𝐺‘𝑀) = (seq𝑀( + , 𝐹)‘𝑀) |
| 96 | 95 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘𝑀) = (seq𝑀( + , 𝐹)‘𝑀)) |
| 97 | | seq1 14055 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
| 98 | 9, 97 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
| 99 | 96, 98 | eqtr2d 2778 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑀) = (𝐺‘𝑀)) |
| 100 | 94, 99 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝐺‘𝑀)) |
| 101 | 88 | ne0d 4342 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐺 ≠ ∅) |
| 102 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺) |
| 103 | 77 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺 Fn 𝑍) |
| 104 | | fvelrnb 6969 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
| 107 | 102, 106 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧) |
| 108 | 107 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧) |
| 109 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝜑 |
| 110 | | nfra1 3284 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 |
| 111 | 109, 110 | nfan 1899 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗(𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) |
| 112 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗 𝑧 ∈ ran 𝐺 |
| 113 | 111, 112 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) |
| 114 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗 𝑧 ≤ 𝑥 |
| 115 | | rspa 3248 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ≤ 𝑥) |
| 116 | 115 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) ≤ 𝑥) |
| 117 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧) |
| 118 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺‘𝑗) = 𝑧 → (𝐺‘𝑗) = 𝑧) |
| 119 | 118 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺‘𝑗) = 𝑧 → 𝑧 = (𝐺‘𝑗)) |
| 120 | 119 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 = (𝐺‘𝑗)) |
| 121 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) ≤ 𝑥) |
| 122 | 120, 121 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ 𝑥) |
| 123 | 116, 117,
122 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ 𝑥) |
| 124 | 123 | 3exp 1120 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥))) |
| 125 | 124 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥))) |
| 126 | 113, 114,
125 | rexlimd 3266 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥)) |
| 127 | 108, 126 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤ 𝑥) |
| 128 | 127 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
| 129 | 128 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)) |
| 130 | 129 | reximdv 3170 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)) |
| 131 | 57, 130 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
| 132 | | suprub 12229 |
. . . . . . . . . . 11
⊢ (((ran
𝐺 ⊆ ℝ ∧ ran
𝐺 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧ (𝐺‘𝑀) ∈ ran 𝐺) → (𝐺‘𝑀) ≤ sup(ran 𝐺, ℝ, < )) |
| 133 | 78, 101, 131, 88, 132 | syl31anc 1375 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑀) ≤ sup(ran 𝐺, ℝ, < )) |
| 134 | 72, 89, 59, 100, 133 | letrd 11418 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, <
)) |
| 135 | 134 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, <
)) |
| 136 | 71, 135 | eqbrtrd 5165 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 137 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) |
| 138 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
| 139 | | elpwinss 45054 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ 𝑍) |
| 140 | 139 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑍) |
| 141 | 140 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑍) |
| 142 | 5, 13 | sselid 3981 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 143 | 138, 141,
142 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 144 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) = (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) |
| 145 | 143, 144 | fmptd 7134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)):𝑦⟶(0[,]+∞)) |
| 146 | 137, 145 | sge0xrcl 46400 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ∈
ℝ*) |
| 147 | 146 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ∈
ℝ*) |
| 148 | | fzfid 14014 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈
Fin) |
| 149 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 150 | 149, 82 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ 𝑍) |
| 151 | 150, 142 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 152 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)) |
| 153 | 151, 152 | fmptd 7134 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)):(𝑀...sup(𝑦, ℝ, <
))⟶(0[,]+∞)) |
| 154 | 153 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)):(𝑀...sup(𝑦, ℝ, <
))⟶(0[,]+∞)) |
| 155 | 148, 154 | sge0xrcl 46400 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈
ℝ*) |
| 156 | 155 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈
ℝ*) |
| 157 | 60 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈
ℝ*) |
| 158 | 157 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈
ℝ*) |
| 159 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑) |
| 160 | 150 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘 ∈ 𝑍) |
| 161 | 159, 160,
142 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
| 162 | | elinel2 4202 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin) |
| 163 | 1, 139, 162 | ssuzfz 45360 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < ))) |
| 164 | 163 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < ))) |
| 165 | 148, 161,
164 | sge0lessmpt 46414 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)))) |
| 166 | 165 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)))) |
| 167 | 78 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ) |
| 168 | 167 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ) |
| 169 | 101 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅) |
| 170 | 169 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅) |
| 171 | 131 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
| 172 | 171 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
| 173 | 159, 160,
13 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
| 174 | 148, 173 | sge0fsummpt 46405 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘)) |
| 175 | 174 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘)) |
| 176 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 177 | 139, 1 | sseqtrdi 4024 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆
(ℤ≥‘𝑀)) |
| 178 | 177 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆
(ℤ≥‘𝑀)) |
| 179 | | uzssz 12899 |
. . . . . . . . . . . . . . . . . 18
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 180 | 1, 179 | eqsstri 4030 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑍 ⊆
ℤ |
| 181 | 139, 180 | sstrdi 3996 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆
ℤ) |
| 182 | 181 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆
ℤ) |
| 183 | | neqne 2948 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑦 = ∅ → 𝑦 ≠ ∅) |
| 184 | 183 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅) |
| 185 | 162 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin) |
| 186 | | suprfinzcl 12732 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦) |
| 187 | 182, 184,
185, 186 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦) |
| 188 | 178, 187 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈
(ℤ≥‘𝑀)) |
| 189 | 188 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈
(ℤ≥‘𝑀)) |
| 190 | 14 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
| 191 | 159, 160,
190 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ ℂ) |
| 192 | 191 | adantlr 715 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ ℂ) |
| 193 | 176, 189,
192 | fsumser 15766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < ))) |
| 194 | 10 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ seq𝑀( + , 𝐹) = 𝐺 |
| 195 | 194 | fveq1i 6907 |
. . . . . . . . . . . 12
⊢ (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )) |
| 196 | 195 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))) |
| 197 | 175, 193,
196 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = (𝐺‘sup(𝑦, ℝ, < ))) |
| 198 | 79 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺) |
| 199 | 198 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺) |
| 200 | 189, 82 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍) |
| 201 | 85 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺) |
| 202 | 200, 201 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺) |
| 203 | | fvelrn 7096 |
. . . . . . . . . . 11
⊢ ((Fun
𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom
𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺) |
| 204 | 199, 202,
203 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺) |
| 205 | 197, 204 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ran 𝐺) |
| 206 | | suprub 12229 |
. . . . . . . . 9
⊢ (((ran
𝐺 ⊆ ℝ ∧ ran
𝐺 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ran 𝐺) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 207 | 168, 170,
172, 205, 206 | syl31anc 1375 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 208 | 147, 156,
158, 166, 207 | xrletrd 13204 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 209 | 136, 208 | pm2.61dan 813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 210 | 209 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩
Fin)(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 211 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
| 212 | 211, 3, 142, 60 | sge0lefimpt 46438 |
. . . . 5
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩
Fin)(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))) |
| 213 | 210, 212 | mpbird 257 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
| 214 | 62, 213 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) ≤ sup(ran 𝐺, ℝ, < )) |
| 215 | 36 | ssriv 3987 |
. . . . . . . . . . . . 13
⊢ (𝑀...𝑗) ⊆ 𝑍 |
| 216 | 215 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀...𝑗) ⊆ 𝑍) |
| 217 | 3, 142, 216 | sge0lessmpt 46414 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
| 218 | 217 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
| 219 | | fzfid 14014 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀...𝑗) ∈ Fin) |
| 220 | 36, 13 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
| 221 | 219, 220 | sge0fsummpt 46405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
| 222 | 221 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
| 223 | 34, 37, 11 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 224 | 34, 37, 190 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
| 225 | 223, 33, 224 | fsumser 15766 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) |
| 226 | 225 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) |
| 227 | 222, 226 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = (seq𝑀( + , 𝐹)‘𝑗)) |
| 228 | 194 | fveq1i 6907 |
. . . . . . . . . . . . 13
⊢ (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗) |
| 229 | 228 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗)) |
| 230 | | simp3 1139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧) |
| 231 | 227, 229,
230 | 3eqtrrd 2782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 =
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘)))) |
| 232 | 62 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
| 233 | 231, 232 | breq12d 5156 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝑧 ≤
(Σ^‘𝐹) ↔
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))) |
| 234 | 218, 233 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤
(Σ^‘𝐹)) |
| 235 | 234 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) |
| 236 | 235 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) |
| 237 | 236 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹))) |
| 238 | 107, 237 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤
(Σ^‘𝐹)) |
| 239 | 238 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹)) |
| 240 | 3, 7 | sge0cl 46396 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
| 241 | 59 | ltpnfd 13163 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) <
+∞) |
| 242 | 8, 60, 91, 214, 241 | xrlelttrd 13202 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘𝐹) < +∞) |
| 243 | 8, 91, 242 | xrgtned 45333 |
. . . . . . 7
⊢ (𝜑 → +∞ ≠
(Σ^‘𝐹)) |
| 244 | 243 | necomd 2996 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘𝐹) ≠ +∞) |
| 245 | | ge0xrre 45544 |
. . . . . 6
⊢
(((Σ^‘𝐹) ∈ (0[,]+∞) ∧
(Σ^‘𝐹) ≠ +∞) →
(Σ^‘𝐹) ∈ ℝ) |
| 246 | 240, 244,
245 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) ∈ ℝ) |
| 247 | | suprleub 12234 |
. . . . 5
⊢ (((ran
𝐺 ⊆ ℝ ∧ ran
𝐺 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧
(Σ^‘𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤
(Σ^‘𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹))) |
| 248 | 78, 101, 131, 246, 247 | syl31anc 1375 |
. . . 4
⊢ (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤
(Σ^‘𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹))) |
| 249 | 239, 248 | mpbird 257 |
. . 3
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ≤
(Σ^‘𝐹)) |
| 250 | 8, 60, 214, 249 | xrletrid 13197 |
. 2
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran 𝐺, ℝ, < )) |
| 251 | | climuni 15588 |
. . 3
⊢ ((𝐺 ⇝ 𝐵 ∧ 𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < )) |
| 252 | 24, 58, 251 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝐵 = sup(ran 𝐺, ℝ, < )) |
| 253 | 250, 252 | eqtr4d 2780 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = 𝐵) |