Step | Hyp | Ref
| Expression |
1 | | sge0isum.z |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | fvex 6201 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ∈ V |
3 | 1, 2 | eqeltri 2697 |
. . . . 5
⊢ 𝑍 ∈ V |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ V) |
5 | | sge0isum.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞)) |
6 | | icossicc 12260 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) |
8 | 5, 7 | fssd 6057 |
. . . 4
⊢ (𝜑 → 𝐹:𝑍⟶(0[,]+∞)) |
9 | 4, 8 | sge0xrcl 40602 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) |
10 | | sge0isum.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | | sge0isum.g |
. . . . . 6
⊢ 𝐺 = seq𝑀( + , 𝐹) |
12 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
13 | | rge0ssre 12280 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
14 | 5 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
15 | 13, 14 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
16 | | 0xr 10086 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ∈
ℝ*) |
18 | | pnfxr 10092 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈
ℝ*) |
20 | | icogelb 12225 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑘)) |
21 | 17, 19, 14, 20 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘)) |
22 | | seqex 12803 |
. . . . . . . . . . 11
⊢ seq𝑀( + , 𝐹) ∈ V |
23 | 11, 22 | eqeltri 2697 |
. . . . . . . . . 10
⊢ 𝐺 ∈ V |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ V) |
25 | | sge0isum.gcnv |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ⇝ 𝐵) |
26 | | climcl 14230 |
. . . . . . . . . 10
⊢ (𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
28 | | breldmg 5330 |
. . . . . . . . 9
⊢ ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺 ⇝ 𝐵) → 𝐺 ∈ dom ⇝ ) |
29 | 24, 27, 25, 28 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ dom ⇝ ) |
30 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐺 = seq𝑀( + , 𝐹)) |
31 | 30 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗)) |
32 | 1 | eleq2i 2693 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
33 | 32 | biimpi 206 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
34 | 33 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
35 | | simpll 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑) |
36 | | elfzuz 12338 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) |
37 | 36, 1 | syl6eleqr 2712 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘 ∈ 𝑍) |
39 | 35, 38, 15 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
40 | | readdcl 10019 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ) |
41 | 40 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ) |
42 | 34, 39, 41 | seqcl 12821 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ) |
43 | 31, 42 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ∈ ℝ) |
44 | 43 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ∈ ℂ) |
45 | 44 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ∈ ℂ) |
46 | 1 | climbdd 14402 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧
∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥) |
47 | 10, 29, 45, 46 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥) |
48 | 43 | ad4ant13 1292 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ∈ ℝ) |
49 | 44 | ad4ant13 1292 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ∈ ℂ) |
50 | 49 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (abs‘(𝐺‘𝑗)) ∈ ℝ) |
51 | | simpllr 799 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ) |
52 | 48 | leabsd 14153 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ≤ (abs‘(𝐺‘𝑗))) |
53 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (abs‘(𝐺‘𝑗)) ≤ 𝑥) |
54 | 48, 50, 51, 52, 53 | letrd 10194 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ≤ 𝑥) |
55 | 54 | ex 450 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → ((abs‘(𝐺‘𝑗)) ≤ 𝑥 → (𝐺‘𝑗) ≤ 𝑥)) |
56 | 55 | ralimdva 2962 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥 → ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥)) |
57 | 56 | reximdva 3017 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥)) |
58 | 47, 57 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) |
59 | 1, 11, 10, 12, 15, 21, 58 | isumsup2 14578 |
. . . . 5
⊢ (𝜑 → 𝐺 ⇝ sup(ran 𝐺, ℝ, < )) |
60 | 1, 10, 59, 43 | climrecl 14314 |
. . . 4
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ∈
ℝ) |
61 | 60 | rexrd 10089 |
. . 3
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ∈
ℝ*) |
62 | 5 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) |
63 | 62 | fveq2d 6195 |
. . . 4
⊢ (𝜑 →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
64 | | mpteq1 4737 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) |
65 | 64 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) =
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘)))) |
66 | | mpt0 6021 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ∅ ↦ (𝐹‘𝑘)) = ∅ |
67 | 66 | fveq2i 6194 |
. . . . . . . . . . . 12
⊢
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) =
(Σ^‘∅) |
68 | | sge00 40593 |
. . . . . . . . . . . 12
⊢
(Σ^‘∅) = 0 |
69 | 67, 68 | eqtri 2644 |
. . . . . . . . . . 11
⊢
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = 0 |
70 | 69 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ →
(Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = 0) |
71 | 65, 70 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑦 = ∅ →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = 0) |
72 | 71 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = 0) |
73 | | 0red 10041 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
74 | 40 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ) |
75 | 1, 10, 15, 74 | seqf 12822 |
. . . . . . . . . . . . 13
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
76 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = seq𝑀( + , 𝐹)) |
77 | 76 | feq1d 6030 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ)) |
78 | 75, 77 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) |
79 | | frn 6053 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑍⟶ℝ → ran 𝐺 ⊆ ℝ) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐺 ⊆ ℝ) |
81 | | ffun 6048 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝑍⟶ℝ → Fun 𝐺) |
82 | 78, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun 𝐺) |
83 | | uzid 11702 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
84 | 10, 83 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
85 | 1 | eqcomi 2631 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) = 𝑍 |
86 | 84, 85 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
87 | | fdm 6051 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝑍⟶ℝ → dom 𝐺 = 𝑍) |
88 | 78, 87 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐺 = 𝑍) |
89 | 88 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 = dom 𝐺) |
90 | 86, 89 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ dom 𝐺) |
91 | | fvelrn 6352 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐺 ∧ 𝑀 ∈ dom 𝐺) → (𝐺‘𝑀) ∈ ran 𝐺) |
92 | 82, 90, 91 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑀) ∈ ran 𝐺) |
93 | 80, 92 | sseldd 3604 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑀) ∈ ℝ) |
94 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ*) |
95 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → +∞ ∈
ℝ*) |
96 | 5, 86 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ (0[,)+∞)) |
97 | | icogelb 12225 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑀) ∈ (0[,)+∞)) → 0 ≤
(𝐹‘𝑀)) |
98 | 94, 95, 96, 97 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (𝐹‘𝑀)) |
99 | 11 | fveq1i 6192 |
. . . . . . . . . . . . 13
⊢ (𝐺‘𝑀) = (seq𝑀( + , 𝐹)‘𝑀) |
100 | 99 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘𝑀) = (seq𝑀( + , 𝐹)‘𝑀)) |
101 | | seq1 12814 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
102 | 10, 101 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) |
103 | 100, 102 | eqtr2d 2657 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝑀) = (𝐺‘𝑀)) |
104 | 98, 103 | breqtrd 4679 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝐺‘𝑀)) |
105 | | ne0i 3921 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑀) ∈ ran 𝐺 → ran 𝐺 ≠ ∅) |
106 | 92, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐺 ≠ ∅) |
107 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺) |
108 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺:𝑍⟶ℝ → 𝐺 Fn 𝑍) |
109 | 78, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺 Fn 𝑍) |
110 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
112 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)) |
113 | 107, 112 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧) |
114 | 113 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧) |
115 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝜑 |
116 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 |
117 | 115, 116 | nfan 1828 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗(𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) |
118 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗 𝑧 ∈ ran 𝐺 |
119 | 117, 118 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) |
120 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗 𝑧 ≤ 𝑥 |
121 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ≤ 𝑥) |
122 | 121 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) ≤ 𝑥) |
123 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧) |
124 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺‘𝑗) = 𝑧 → (𝐺‘𝑗) = 𝑧) |
125 | 124 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺‘𝑗) = 𝑧 → 𝑧 = (𝐺‘𝑗)) |
126 | 125 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 = (𝐺‘𝑗)) |
127 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) ≤ 𝑥) |
128 | 126, 127 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ 𝑥) |
129 | 122, 123,
128 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ 𝑥) |
130 | 129 | 3exp 1264 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑗 ∈
𝑍 (𝐺‘𝑗) ≤ 𝑥 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥))) |
131 | 130 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥))) |
132 | 119, 120,
131 | rexlimd 3026 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥)) |
133 | 114, 132 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤ 𝑥) |
134 | 133 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
135 | 134 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)) |
136 | 135 | reximdv 3016 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)) |
137 | 58, 136 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
138 | | suprub 10984 |
. . . . . . . . . . 11
⊢ (((ran
𝐺 ⊆ ℝ ∧ ran
𝐺 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧ (𝐺‘𝑀) ∈ ran 𝐺) → (𝐺‘𝑀) ≤ sup(ran 𝐺, ℝ, < )) |
139 | 80, 106, 137, 92, 138 | syl31anc 1329 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑀) ≤ sup(ran 𝐺, ℝ, < )) |
140 | 73, 93, 60, 104, 139 | letrd 10194 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, <
)) |
141 | 140 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, <
)) |
142 | 72, 141 | eqbrtrd 4675 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
143 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) |
144 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝜑) |
145 | | elpwinss 39216 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ 𝑍) |
146 | 145 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑍) |
147 | 146 | adantll 750 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑍) |
148 | 6, 14 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
149 | 144, 147,
148 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
150 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) = (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) |
151 | 149, 150 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)):𝑦⟶(0[,]+∞)) |
152 | 143, 151 | sge0xrcl 40602 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ∈
ℝ*) |
153 | 152 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ∈
ℝ*) |
154 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈
Fin) |
155 | | elfzuz 12338 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ≥‘𝑀)) |
156 | 155, 85 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ 𝑍) |
157 | 156, 148 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
158 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)) |
159 | 157, 158 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)):(𝑀...sup(𝑦, ℝ, <
))⟶(0[,]+∞)) |
160 | 159 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)):(𝑀...sup(𝑦, ℝ, <
))⟶(0[,]+∞)) |
161 | 154, 160 | sge0xrcl 40602 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈
ℝ*) |
162 | 161 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈
ℝ*) |
163 | 61 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈
ℝ*) |
164 | 163 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈
ℝ*) |
165 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑) |
166 | 156 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘 ∈ 𝑍) |
167 | 165, 166,
148 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,]+∞)) |
168 | | elinel2 3800 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin) |
169 | 1, 145, 168 | ssuzfz 39565 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < ))) |
170 | 169 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < ))) |
171 | 154, 167,
170 | sge0lessmpt 40616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)))) |
172 | 171 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)))) |
173 | 80 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ) |
174 | 173 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ) |
175 | 106 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅) |
176 | 175 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅) |
177 | 137 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
178 | 177 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) |
179 | 165, 166,
14 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
180 | 154, 179 | sge0fsummpt 40607 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘)) |
181 | 180 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘)) |
182 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
183 | 145, 1 | syl6sseq 3651 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆
(ℤ≥‘𝑀)) |
184 | 183 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆
(ℤ≥‘𝑀)) |
185 | | uzssz 11707 |
. . . . . . . . . . . . . . . . . 18
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
186 | 1, 185 | eqsstri 3635 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑍 ⊆
ℤ |
187 | 145, 186 | syl6ss 3615 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆
ℤ) |
188 | 187 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆
ℤ) |
189 | | neqne 2802 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑦 = ∅ → 𝑦 ≠ ∅) |
190 | 189 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅) |
191 | 168 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin) |
192 | | suprfinzcl 11492 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦) |
193 | 188, 190,
191, 192 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦) |
194 | 184, 193 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈
(ℤ≥‘𝑀)) |
195 | 194 | adantll 750 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈
(ℤ≥‘𝑀)) |
196 | 15 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
197 | 165, 166,
196 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ ℂ) |
198 | 197 | adantlr 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ ℂ) |
199 | 182, 195,
198 | fsumser 14461 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < ))) |
200 | 11 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢ seq𝑀( + , 𝐹) = 𝐺 |
201 | 200 | fveq1i 6192 |
. . . . . . . . . . . 12
⊢ (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )) |
202 | 201 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))) |
203 | 181, 199,
202 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = (𝐺‘sup(𝑦, ℝ, < ))) |
204 | 82 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺) |
205 | 204 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺) |
206 | 195, 85 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍) |
207 | 89 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺) |
208 | 206, 207 | eleqtrd 2703 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺) |
209 | | fvelrn 6352 |
. . . . . . . . . . 11
⊢ ((Fun
𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom
𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺) |
210 | 205, 208,
209 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺) |
211 | 203, 210 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ran 𝐺) |
212 | | suprub 10984 |
. . . . . . . . 9
⊢ (((ran
𝐺 ⊆ ℝ ∧ ran
𝐺 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ran 𝐺) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
213 | 174, 176,
178, 211, 212 | syl31anc 1329 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
214 | 153, 162,
164, 172, 213 | xrletrd 11993 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
215 | 142, 214 | pm2.61dan 832 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) →
(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
216 | 215 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩
Fin)(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
217 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
218 | 217, 4, 148, 61 | sge0lefimpt 40640 |
. . . . 5
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩
Fin)(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))) |
219 | 216, 218 | mpbird 247 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )) |
220 | 63, 219 | eqbrtrd 4675 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) ≤ sup(ran 𝐺, ℝ, < )) |
221 | 37 | ssriv 3607 |
. . . . . . . . . . . . 13
⊢ (𝑀...𝑗) ⊆ 𝑍 |
222 | 221 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀...𝑗) ⊆ 𝑍) |
223 | 4, 148, 222 | sge0lessmpt 40616 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
224 | 223 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
225 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀...𝑗) ∈ Fin) |
226 | 37, 14 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ (0[,)+∞)) |
227 | 225, 226 | sge0fsummpt 40607 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
228 | 227 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘)) |
229 | 35, 38, 12 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
230 | 35, 38, 196 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) |
231 | 229, 34, 230 | fsumser 14461 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) |
232 | 231 | 3adant3 1081 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗)) |
233 | 228, 232 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = (seq𝑀( + , 𝐹)‘𝑗)) |
234 | 200 | fveq1i 6192 |
. . . . . . . . . . . . 13
⊢ (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗) |
235 | 234 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗)) |
236 | | simp3 1063 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧) |
237 | 233, 235,
236 | 3eqtrrd 2661 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 =
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘)))) |
238 | 63 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) →
(Σ^‘𝐹) =
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))) |
239 | 237, 238 | breq12d 4666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝑧 ≤
(Σ^‘𝐹) ↔
(Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤
(Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))) |
240 | 224, 239 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤
(Σ^‘𝐹)) |
241 | 240 | 3exp 1264 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) |
242 | 241 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹)))) |
243 | 242 | rexlimdv 3030 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤
(Σ^‘𝐹))) |
244 | 113, 243 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤
(Σ^‘𝐹)) |
245 | 244 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹)) |
246 | 4, 8 | sge0cl 40598 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
247 | 60 | ltpnfd 11955 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) <
+∞) |
248 | 9, 61, 95, 220, 247 | xrlelttrd 11991 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘𝐹) < +∞) |
249 | 9, 95, 248 | xrgtned 39538 |
. . . . . . 7
⊢ (𝜑 → +∞ ≠
(Σ^‘𝐹)) |
250 | 249 | necomd 2849 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘𝐹) ≠ +∞) |
251 | | ge0xrre 39758 |
. . . . . 6
⊢
(((Σ^‘𝐹) ∈ (0[,]+∞) ∧
(Σ^‘𝐹) ≠ +∞) →
(Σ^‘𝐹) ∈ ℝ) |
252 | 246, 250,
251 | syl2anc 693 |
. . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) ∈ ℝ) |
253 | | suprleub 10989 |
. . . . 5
⊢ (((ran
𝐺 ⊆ ℝ ∧ ran
𝐺 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧
(Σ^‘𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤
(Σ^‘𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹))) |
254 | 80, 106, 137, 252, 253 | syl31anc 1329 |
. . . 4
⊢ (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤
(Σ^‘𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤
(Σ^‘𝐹))) |
255 | 245, 254 | mpbird 247 |
. . 3
⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ≤
(Σ^‘𝐹)) |
256 | 9, 61, 220, 255 | xrletrid 11986 |
. 2
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran 𝐺, ℝ, < )) |
257 | | climuni 14283 |
. . 3
⊢ ((𝐺 ⇝ 𝐵 ∧ 𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < )) |
258 | 25, 59, 257 | syl2anc 693 |
. 2
⊢ (𝜑 → 𝐵 = sup(ran 𝐺, ℝ, < )) |
259 | 256, 258 | eqtr4d 2659 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = 𝐵) |