Step | Hyp | Ref
| Expression |
1 | | pserulm.y |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 0) → 𝑆 ⊆ (◡abs “ (0[,]𝑀))) |
3 | | 0xr 10086 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
4 | | pserulm.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
5 | 4 | rexrd 10089 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
6 | | icc0 12223 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 𝑀 ∈ ℝ*) →
((0[,]𝑀) = ∅ ↔
𝑀 < 0)) |
7 | 3, 5, 6 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]𝑀) = ∅ ↔ 𝑀 < 0)) |
8 | 7 | biimpar 502 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 < 0) → (0[,]𝑀) = ∅) |
9 | 8 | imaeq2d 5466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 < 0) → (◡abs “ (0[,]𝑀)) = (◡abs “ ∅)) |
10 | | ima0 5481 |
. . . . . 6
⊢ (◡abs “ ∅) =
∅ |
11 | 9, 10 | syl6eq 2672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 0) → (◡abs “ (0[,]𝑀)) = ∅) |
12 | 2, 11 | sseqtrd 3641 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 < 0) → 𝑆 ⊆ ∅) |
13 | | ss0 3974 |
. . . 4
⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 0) → 𝑆 = ∅) |
15 | | nn0uz 11722 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
16 | | 0zd 11389 |
. . . 4
⊢ (𝜑 → 0 ∈
ℤ) |
17 | | 0zd 11389 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 0 ∈ ℤ) |
18 | | pserf.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
19 | | pserf.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) |
21 | | cnvimass 5485 |
. . . . . . . . . . . . . . 15
⊢ (◡abs “ (0[,]𝑀)) ⊆ dom abs |
22 | | absf 14077 |
. . . . . . . . . . . . . . . 16
⊢
abs:ℂ⟶ℝ |
23 | 22 | fdmi 6052 |
. . . . . . . . . . . . . . 15
⊢ dom abs =
ℂ |
24 | 21, 23 | sseqtri 3637 |
. . . . . . . . . . . . . 14
⊢ (◡abs “ (0[,]𝑀)) ⊆ ℂ |
25 | 1, 24 | syl6ss 3615 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
26 | 25 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
27 | 18, 20, 26 | psergf 24166 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑦):ℕ0⟶ℂ) |
28 | 27 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑦)‘𝑗) ∈ ℂ) |
29 | 15, 17, 28 | serf 12829 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → seq0( + , (𝐺‘𝑦)):ℕ0⟶ℂ) |
30 | 29 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝐺‘𝑦))‘𝑖) ∈ ℂ) |
31 | 30 | an32s 846 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑦 ∈ 𝑆) → (seq0( + , (𝐺‘𝑦))‘𝑖) ∈ ℂ) |
32 | | eqid 2622 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) = (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) |
33 | 31, 32 | fmptd 6385 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)):𝑆⟶ℂ) |
34 | | cnex 10017 |
. . . . . . 7
⊢ ℂ
∈ V |
35 | | ssexg 4804 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
∈ V) → 𝑆 ∈
V) |
36 | 25, 34, 35 | sylancl 694 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ V) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑆 ∈ V) |
38 | | elmapg 7870 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝑆 ∈ V)
→ ((𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) ∈ (ℂ ↑𝑚
𝑆) ↔ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)):𝑆⟶ℂ)) |
39 | 34, 37, 38 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) ∈ (ℂ ↑𝑚
𝑆) ↔ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)):𝑆⟶ℂ)) |
40 | 33, 39 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) ∈ (ℂ ↑𝑚
𝑆)) |
41 | | pserulm.h |
. . . . 5
⊢ 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) |
42 | 40, 41 | fmptd 6385 |
. . . 4
⊢ (𝜑 → 𝐻:ℕ0⟶(ℂ
↑𝑚 𝑆)) |
43 | | eqidd 2623 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑦)‘𝑗) = ((𝐺‘𝑦)‘𝑗)) |
44 | | pserf.r |
. . . . . . 7
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
45 | 1 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (◡abs “ (0[,]𝑀))) |
46 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
47 | | elpreima 6337 |
. . . . . . . . . . . . . 14
⊢ (abs Fn
ℂ → (𝑦 ∈
(◡abs “ (0[,]𝑀)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀)))) |
48 | 22, 46, 47 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (◡abs “ (0[,]𝑀)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀))) |
49 | 45, 48 | sylib 208 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀))) |
50 | 49 | simprd 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘𝑦) ∈ (0[,]𝑀)) |
51 | | 0re 10040 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
52 | 4 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑀 ∈ ℝ) |
53 | | elicc2 12238 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ) → ((abs‘𝑦) ∈ (0[,]𝑀) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) ≤ 𝑀))) |
54 | 51, 52, 53 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((abs‘𝑦) ∈ (0[,]𝑀) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) ≤ 𝑀))) |
55 | 50, 54 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((abs‘𝑦) ∈ ℝ ∧ 0 ≤
(abs‘𝑦) ∧
(abs‘𝑦) ≤ 𝑀)) |
56 | 55 | simp1d 1073 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘𝑦) ∈ ℝ) |
57 | 56 | rexrd 10089 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘𝑦) ∈
ℝ*) |
58 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑀 ∈
ℝ*) |
59 | | iccssxr 12256 |
. . . . . . . . . 10
⊢
(0[,]+∞) ⊆ ℝ* |
60 | 18, 19, 44 | radcnvcl 24171 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
61 | 59, 60 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
62 | 61 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑅 ∈
ℝ*) |
63 | 55 | simp3d 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘𝑦) ≤ 𝑀) |
64 | | pserulm.l |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 < 𝑅) |
65 | 64 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝑀 < 𝑅) |
66 | 57, 58, 62, 63, 65 | xrlelttrd 11991 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘𝑦) < 𝑅) |
67 | 18, 20, 44, 26, 66 | radcnvlt2 24173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ ) |
68 | 15, 17, 43, 28, 67 | isumcl 14492 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) ∈ ℂ) |
69 | | pserf.f |
. . . . 5
⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) |
70 | 68, 69 | fmptd 6385 |
. . . 4
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
71 | 15, 16, 42, 70 | ulm0 24145 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = ∅) → 𝐻(⇝𝑢‘𝑆)𝐹) |
72 | 14, 71 | syldan 487 |
. 2
⊢ ((𝜑 ∧ 𝑀 < 0) → 𝐻(⇝𝑢‘𝑆)𝐹) |
73 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
74 | 73, 15 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
(ℤ≥‘0)) |
75 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑖) → 𝑘 ∈ ℕ0) |
76 | 75 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → 𝑘 ∈ ℕ0) |
77 | 36 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → 𝑆 ∈ V) |
78 | | mptexg 6484 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ V → (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘)) ∈ V) |
79 | 77, 78 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘)) ∈ V) |
80 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑦 → (𝐺‘𝑤) = (𝐺‘𝑦)) |
81 | 80 | fveq1d 6193 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → ((𝐺‘𝑤)‘𝑚) = ((𝐺‘𝑦)‘𝑚)) |
82 | 81 | cbvmptv 4750 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑚)) |
83 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑘 → ((𝐺‘𝑦)‘𝑚) = ((𝐺‘𝑦)‘𝑘)) |
84 | 83 | mpteq2dv 4745 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑚)) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))) |
85 | 82, 84 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))) |
86 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))) |
87 | 85, 86 | fvmptg 6280 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘)) ∈ V) → ((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))) |
88 | 76, 79, 87 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → ((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))) |
89 | 37, 74, 88 | seqof 12858 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))‘𝑖) = (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) |
90 | 89 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) = (seq0( ∘𝑓 + ,
(𝑚 ∈
ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))‘𝑖)) |
91 | 90 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) = (𝑖 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))‘𝑖))) |
92 | | 0z 11388 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
93 | | seqfn 12813 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → seq0( ∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) Fn
(ℤ≥‘0)) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . 8
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) Fn
(ℤ≥‘0) |
95 | 15 | fneq2i 5986 |
. . . . . . . 8
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) Fn
(ℤ≥‘0)) |
96 | 94, 95 | mpbir 221 |
. . . . . . 7
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) Fn ℕ0 |
97 | | dffn5 6241 |
. . . . . . 7
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) Fn ℕ0 ↔ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) = (𝑖 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))‘𝑖))) |
98 | 96, 97 | mpbi 220 |
. . . . . 6
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) = (𝑖 ∈ ℕ0 ↦ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))‘𝑖)) |
99 | 91, 41, 98 | 3eqtr4g 2681 |
. . . . 5
⊢ (𝜑 → 𝐻 = seq0( ∘𝑓 + ,
(𝑚 ∈
ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))) |
100 | 99 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻 = seq0( ∘𝑓 + ,
(𝑚 ∈
ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))))) |
101 | | 0zd 11389 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 0 ∈ ℤ) |
102 | 36 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝑆 ∈ V) |
103 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) |
104 | 25 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → 𝑤 ∈ ℂ) |
105 | 18, 103, 104 | psergf 24166 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑆) → (𝐺‘𝑤):ℕ0⟶ℂ) |
106 | 105 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝐺‘𝑤)‘𝑚) ∈ ℂ) |
107 | 106 | an32s 846 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑤 ∈ 𝑆) → ((𝐺‘𝑤)‘𝑚) ∈ ℂ) |
108 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) = (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) |
109 | 107, 108 | fmptd 6385 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)):𝑆⟶ℂ) |
110 | 36 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑆 ∈ V) |
111 | | elmapg 7870 |
. . . . . . . . 9
⊢ ((ℂ
∈ V ∧ 𝑆 ∈ V)
→ ((𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) ∈ (ℂ ↑𝑚
𝑆) ↔ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)):𝑆⟶ℂ)) |
112 | 34, 110, 111 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) ∈ (ℂ ↑𝑚
𝑆) ↔ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)):𝑆⟶ℂ)) |
113 | 109, 112 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)) ∈ (ℂ ↑𝑚
𝑆)) |
114 | 113, 86 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))):ℕ0⟶(ℂ
↑𝑚 𝑆)) |
115 | 114 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚))):ℕ0⟶(ℂ
↑𝑚 𝑆)) |
116 | | fex 6490 |
. . . . . . . 8
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) |
117 | 22, 34, 116 | mp2an 708 |
. . . . . . 7
⊢ abs
∈ V |
118 | | fvex 6201 |
. . . . . . 7
⊢ (𝐺‘𝑀) ∈ V |
119 | 117, 118 | coex 7118 |
. . . . . 6
⊢ (abs
∘ (𝐺‘𝑀)) ∈ V |
120 | 119 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (abs ∘ (𝐺‘𝑀)) ∈ V) |
121 | 19 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝐴:ℕ0⟶ℂ) |
122 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ) |
123 | 122 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ) |
124 | 18, 121, 123 | psergf 24166 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (𝐺‘𝑀):ℕ0⟶ℂ) |
125 | | fco 6058 |
. . . . . . 7
⊢
((abs:ℂ⟶ℝ ∧ (𝐺‘𝑀):ℕ0⟶ℂ) →
(abs ∘ (𝐺‘𝑀)):ℕ0⟶ℝ) |
126 | 22, 124, 125 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (abs ∘ (𝐺‘𝑀)):ℕ0⟶ℝ) |
127 | 126 | ffvelrnda 6359 |
. . . . 5
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ 𝑘 ∈ ℕ0) → ((abs
∘ (𝐺‘𝑀))‘𝑘) ∈ ℝ) |
128 | 25 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑆 ⊆ ℂ) |
129 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ 𝑆) |
130 | 128, 129 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ ℂ) |
131 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑘 ∈ ℕ0) |
132 | 130, 131 | expcld 13008 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (𝑧↑𝑘) ∈ ℂ) |
133 | 132 | abscld 14175 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝑧↑𝑘)) ∈ ℝ) |
134 | 123 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑀 ∈ ℂ) |
135 | 134, 131 | expcld 13008 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (𝑀↑𝑘) ∈ ℂ) |
136 | 135 | abscld 14175 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝑀↑𝑘)) ∈ ℝ) |
137 | 19 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝐴:ℕ0⟶ℂ) |
138 | 137, 131 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (𝐴‘𝑘) ∈ ℂ) |
139 | 138 | abscld 14175 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝐴‘𝑘)) ∈ ℝ) |
140 | 138 | absge0d 14183 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 0 ≤ (abs‘(𝐴‘𝑘))) |
141 | 130 | abscld 14175 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘𝑧) ∈ ℝ) |
142 | 4 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑀 ∈ ℝ) |
143 | 130 | absge0d 14183 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 0 ≤ (abs‘𝑧)) |
144 | 63 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (abs‘𝑦) ≤ 𝑀) |
145 | 144 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ∀𝑦 ∈ 𝑆 (abs‘𝑦) ≤ 𝑀) |
146 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (abs‘𝑦) = (abs‘𝑧)) |
147 | 146 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → ((abs‘𝑦) ≤ 𝑀 ↔ (abs‘𝑧) ≤ 𝑀)) |
148 | 147 | rspcv 3305 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑆 → (∀𝑦 ∈ 𝑆 (abs‘𝑦) ≤ 𝑀 → (abs‘𝑧) ≤ 𝑀)) |
149 | 129, 145,
148 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘𝑧) ≤ 𝑀) |
150 | | leexp1a 12919 |
. . . . . . . . . 10
⊢
((((abs‘𝑧)
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑘
∈ ℕ0) ∧ (0 ≤ (abs‘𝑧) ∧ (abs‘𝑧) ≤ 𝑀)) → ((abs‘𝑧)↑𝑘) ≤ (𝑀↑𝑘)) |
151 | 141, 142,
131, 143, 149, 150 | syl32anc 1334 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((abs‘𝑧)↑𝑘) ≤ (𝑀↑𝑘)) |
152 | 130, 131 | absexpd 14191 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝑧↑𝑘)) = ((abs‘𝑧)↑𝑘)) |
153 | 134, 131 | absexpd 14191 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝑀↑𝑘)) = ((abs‘𝑀)↑𝑘)) |
154 | | absid 14036 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) → (abs‘𝑀) = 𝑀) |
155 | 4, 154 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (abs‘𝑀) = 𝑀) |
156 | 155 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘𝑀) = 𝑀) |
157 | 156 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((abs‘𝑀)↑𝑘) = (𝑀↑𝑘)) |
158 | 153, 157 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝑀↑𝑘)) = (𝑀↑𝑘)) |
159 | 151, 152,
158 | 3brtr4d 4685 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(𝑧↑𝑘)) ≤ (abs‘(𝑀↑𝑘))) |
160 | 133, 136,
139, 140, 159 | lemul2ad 10964 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((abs‘(𝐴‘𝑘)) · (abs‘(𝑧↑𝑘))) ≤ ((abs‘(𝐴‘𝑘)) · (abs‘(𝑀↑𝑘)))) |
161 | 138, 132 | absmuld 14193 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐴‘𝑘) · (𝑧↑𝑘))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑧↑𝑘)))) |
162 | 138, 135 | absmuld 14193 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐴‘𝑘) · (𝑀↑𝑘))) = ((abs‘(𝐴‘𝑘)) · (abs‘(𝑀↑𝑘)))) |
163 | 160, 161,
162 | 3brtr4d 4685 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐴‘𝑘) · (𝑧↑𝑘))) ≤ (abs‘((𝐴‘𝑘) · (𝑀↑𝑘)))) |
164 | 36 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → 𝑆 ∈ V) |
165 | 164, 78 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘)) ∈ V) |
166 | 131, 165,
87 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))) |
167 | 166 | fveq1d 6193 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘)‘𝑧) = ((𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))‘𝑧)) |
168 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐺‘𝑦) = (𝐺‘𝑧)) |
169 | 168 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑘) = ((𝐺‘𝑧)‘𝑘)) |
170 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘)) = (𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘)) |
171 | | fvex 6201 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑧)‘𝑘) ∈ V |
172 | 169, 170,
171 | fvmpt 6282 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑆 → ((𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))‘𝑧) = ((𝐺‘𝑧)‘𝑘)) |
173 | 172 | ad2antll 765 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((𝑦 ∈ 𝑆 ↦ ((𝐺‘𝑦)‘𝑘))‘𝑧) = ((𝐺‘𝑧)‘𝑘)) |
174 | 18 | pserval2 24165 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐺‘𝑧)‘𝑘) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
175 | 130, 131,
174 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((𝐺‘𝑧)‘𝑘) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
176 | 167, 173,
175 | 3eqtrd 2660 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘)‘𝑧) = ((𝐴‘𝑘) · (𝑧↑𝑘))) |
177 | 176 | fveq2d 6195 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘)‘𝑧)) = (abs‘((𝐴‘𝑘) · (𝑧↑𝑘)))) |
178 | 124 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (𝐺‘𝑀):ℕ0⟶ℂ) |
179 | | fvco3 6275 |
. . . . . . . 8
⊢ (((𝐺‘𝑀):ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((abs ∘ (𝐺‘𝑀))‘𝑘) = (abs‘((𝐺‘𝑀)‘𝑘))) |
180 | 178, 131,
179 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((abs ∘ (𝐺‘𝑀))‘𝑘) = (abs‘((𝐺‘𝑀)‘𝑘))) |
181 | 18 | pserval2 24165 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐺‘𝑀)‘𝑘) = ((𝐴‘𝑘) · (𝑀↑𝑘))) |
182 | 134, 131,
181 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((𝐺‘𝑀)‘𝑘) = ((𝐴‘𝑘) · (𝑀↑𝑘))) |
183 | 182 | fveq2d 6195 |
. . . . . . 7
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐺‘𝑀)‘𝑘)) = (abs‘((𝐴‘𝑘) · (𝑀↑𝑘)))) |
184 | 180, 183 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → ((abs ∘ (𝐺‘𝑀))‘𝑘) = (abs‘((𝐴‘𝑘) · (𝑀↑𝑘)))) |
185 | 163, 177,
184 | 3brtr4d 4685 |
. . . . 5
⊢ (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆)) → (abs‘(((𝑚 ∈ ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))‘𝑘)‘𝑧)) ≤ ((abs ∘ (𝐺‘𝑀))‘𝑘)) |
186 | 64 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 < 𝑅) |
187 | 155, 186 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (abs‘𝑀) < 𝑅) |
188 | | id 22 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → 𝑖 = 𝑚) |
189 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑚 → ((𝐺‘𝑀)‘𝑖) = ((𝐺‘𝑀)‘𝑚)) |
190 | 189 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑖 = 𝑚 → (abs‘((𝐺‘𝑀)‘𝑖)) = (abs‘((𝐺‘𝑀)‘𝑚))) |
191 | 188, 190 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → (𝑖 · (abs‘((𝐺‘𝑀)‘𝑖))) = (𝑚 · (abs‘((𝐺‘𝑀)‘𝑚)))) |
192 | 191 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑀)‘𝑖)))) = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑀)‘𝑚)))) |
193 | 18, 121, 44, 123, 187, 192 | radcnvlt1 24172 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑀)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs
∘ (𝐺‘𝑀))) ∈ dom ⇝
)) |
194 | 193 | simprd 479 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → seq0( + , (abs ∘ (𝐺‘𝑀))) ∈ dom ⇝ ) |
195 | 15, 101, 102, 115, 120, 127, 185, 194 | mtest 24158 |
. . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → seq0( ∘𝑓 +
, (𝑚 ∈
ℕ0 ↦ (𝑤 ∈ 𝑆 ↦ ((𝐺‘𝑤)‘𝑚)))) ∈ dom
(⇝𝑢‘𝑆)) |
196 | 100, 195 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻 ∈ dom
(⇝𝑢‘𝑆)) |
197 | | eldmg 5319 |
. . . . . 6
⊢ (𝐻 ∈ dom
(⇝𝑢‘𝑆) → (𝐻 ∈ dom
(⇝𝑢‘𝑆) ↔ ∃𝑓 𝐻(⇝𝑢‘𝑆)𝑓)) |
198 | 197 | ibi 256 |
. . . . 5
⊢ (𝐻 ∈ dom
(⇝𝑢‘𝑆) → ∃𝑓 𝐻(⇝𝑢‘𝑆)𝑓) |
199 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → 𝐻(⇝𝑢‘𝑆)𝑓) |
200 | | ulmcl 24135 |
. . . . . . . . . . 11
⊢ (𝐻(⇝𝑢‘𝑆)𝑓 → 𝑓:𝑆⟶ℂ) |
201 | 200 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → 𝑓:𝑆⟶ℂ) |
202 | 201 | feqmptd 6249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → 𝑓 = (𝑦 ∈ 𝑆 ↦ (𝑓‘𝑦))) |
203 | | 0zd 11389 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → 0 ∈ ℤ) |
204 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑦)‘𝑗) = ((𝐺‘𝑦)‘𝑗)) |
205 | 27 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑦):ℕ0⟶ℂ) |
206 | 205 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑦)‘𝑗) ∈ ℂ) |
207 | 42 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → 𝐻:ℕ0⟶(ℂ
↑𝑚 𝑆)) |
208 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
209 | | seqex 12803 |
. . . . . . . . . . . . . 14
⊢ seq0( + ,
(𝐺‘𝑦)) ∈ V |
210 | 209 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → seq0( + , (𝐺‘𝑦)) ∈ V) |
211 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
212 | 36 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑆 ∈ V) |
213 | | mptexg 6484 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ V → (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) ∈ V) |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) ∈ V) |
215 | 41 | fvmpt2 6291 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℕ0
∧ (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖)) ∈ V) → (𝐻‘𝑖) = (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) |
216 | 211, 214,
215 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → (𝐻‘𝑖) = (𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))) |
217 | 216 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐻‘𝑖)‘𝑦) = ((𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))‘𝑦)) |
218 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑦 ∈ 𝑆) |
219 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (seq0( +
, (𝐺‘𝑦))‘𝑖) ∈ V |
220 | 32 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑆 ∧ (seq0( + , (𝐺‘𝑦))‘𝑖) ∈ V) → ((𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))‘𝑦) = (seq0( + , (𝐺‘𝑦))‘𝑖)) |
221 | 218, 219,
220 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑦 ∈ 𝑆 ↦ (seq0( + , (𝐺‘𝑦))‘𝑖))‘𝑦) = (seq0( + , (𝐺‘𝑦))‘𝑖)) |
222 | 217, 221 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐻‘𝑖)‘𝑦) = (seq0( + , (𝐺‘𝑦))‘𝑖)) |
223 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → 𝐻(⇝𝑢‘𝑆)𝑓) |
224 | 15, 203, 207, 208, 210, 222, 223 | ulmclm 24141 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → seq0( + , (𝐺‘𝑦)) ⇝ (𝑓‘𝑦)) |
225 | 15, 203, 204, 206, 224 | isumclim 14488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) ∧ 𝑦 ∈ 𝑆) → Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) = (𝑓‘𝑦)) |
226 | 225 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) = (𝑦 ∈ 𝑆 ↦ (𝑓‘𝑦))) |
227 | 69, 226 | syl5eq 2668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → 𝐹 = (𝑦 ∈ 𝑆 ↦ (𝑓‘𝑦))) |
228 | 202, 227 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → 𝑓 = 𝐹) |
229 | 199, 228 | breqtrd 4679 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐻(⇝𝑢‘𝑆)𝑓) → 𝐻(⇝𝑢‘𝑆)𝐹) |
230 | 229 | ex 450 |
. . . . . 6
⊢ (𝜑 → (𝐻(⇝𝑢‘𝑆)𝑓 → 𝐻(⇝𝑢‘𝑆)𝐹)) |
231 | 230 | exlimdv 1861 |
. . . . 5
⊢ (𝜑 → (∃𝑓 𝐻(⇝𝑢‘𝑆)𝑓 → 𝐻(⇝𝑢‘𝑆)𝐹)) |
232 | 198, 231 | syl5 34 |
. . . 4
⊢ (𝜑 → (𝐻 ∈ dom
(⇝𝑢‘𝑆) → 𝐻(⇝𝑢‘𝑆)𝐹)) |
233 | 232 | imp 445 |
. . 3
⊢ ((𝜑 ∧ 𝐻 ∈ dom
(⇝𝑢‘𝑆)) → 𝐻(⇝𝑢‘𝑆)𝐹) |
234 | 196, 233 | syldan 487 |
. 2
⊢ ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻(⇝𝑢‘𝑆)𝐹) |
235 | | 0red 10041 |
. 2
⊢ (𝜑 → 0 ∈
ℝ) |
236 | 72, 234, 4, 235 | ltlecasei 10145 |
1
⊢ (𝜑 → 𝐻(⇝𝑢‘𝑆)𝐹) |