| Step | Hyp | Ref
| Expression |
| 1 | | nn0uz 12920 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
| 2 | | cnelprrecn 11248 |
. . 3
⊢ ℂ
∈ {ℝ, ℂ} |
| 3 | 2 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ℂ ∈ {ℝ,
ℂ}) |
| 4 | | 0zd 12625 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℤ) |
| 5 | | fzfid 14014 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (0...𝑘) ∈ Fin) |
| 6 | | pserf.g |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
| 7 | | pserf.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
| 8 | 7 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
| 9 | | pserdv.b |
. . . . . . . . . . 11
⊢ 𝐵 = (0(ball‘(abs ∘
− ))(((abs‘𝑎) +
𝑀) / 2)) |
| 10 | | cnxmet 24793 |
. . . . . . . . . . . 12
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 11 | | 0cnd 11254 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℂ) |
| 12 | | pserf.f |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) |
| 13 | | pserf.r |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
| 14 | | psercn.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (◡abs “ (0[,)𝑅)) |
| 15 | | psercn.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) |
| 16 | 6, 12, 7, 13, 14, 15 | pserdvlem1 26471 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧
(abs‘𝑎) <
(((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅)) |
| 17 | 16 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ+) |
| 18 | 17 | rpxrd 13078 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
| 19 | | blssm 24428 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
| 20 | 10, 11, 18, 19 | mp3an2i 1468 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
| 21 | 9, 20 | eqsstrid 4022 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ ℂ) |
| 22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆
ℂ) |
| 23 | 22 | sselda 3983 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 24 | 6, 8, 23 | psergf 26455 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦):ℕ0⟶ℂ) |
| 25 | | elfznn0 13660 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℕ0) |
| 26 | | ffvelcdm 7101 |
. . . . . . 7
⊢ (((𝐺‘𝑦):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
| 27 | 24, 25, 26 | syl2an 596 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (0...𝑘)) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
| 28 | 5, 27 | fsumcl 15769 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
| 29 | 28 | fmpttd 7135 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)):𝐵⟶ℂ) |
| 30 | | cnex 11236 |
. . . . 5
⊢ ℂ
∈ V |
| 31 | 9 | ovexi 7465 |
. . . . 5
⊢ 𝐵 ∈ V |
| 32 | 30, 31 | elmap 8911 |
. . . 4
⊢ ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)):𝐵⟶ℂ) |
| 33 | 29, 32 | sylibr 234 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) ∈ (ℂ ↑m 𝐵)) |
| 34 | 33 | fmpttd 7135 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑘 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))):ℕ0⟶(ℂ
↑m 𝐵)) |
| 35 | 6, 12, 7, 13, 14, 15 | psercn 26470 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |
| 36 | | cncff 24919 |
. . . . 5
⊢ (𝐹 ∈ (𝑆–cn→ℂ) → 𝐹:𝑆⟶ℂ) |
| 37 | 35, 36 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
| 38 | 37 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
| 39 | 6, 12, 7, 13, 14, 16 | psercnlem2 26468 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs
∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)) |
| 40 | 39 | simp2d 1144 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2)))) |
| 41 | 9, 40 | eqsstrid 4022 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2)))) |
| 42 | 39 | simp3d 1145 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆) |
| 43 | 41, 42 | sstrd 3994 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ 𝑆) |
| 44 | 38, 43 | fssresd 6775 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ 𝐵):𝐵⟶ℂ) |
| 45 | | 0zd 12625 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 0 ∈ ℤ) |
| 46 | | eqidd 2738 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑧)‘𝑗) = ((𝐺‘𝑧)‘𝑗)) |
| 47 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
| 48 | 21 | sselda 3983 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ℂ) |
| 49 | 6, 47, 48 | psergf 26455 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧):ℕ0⟶ℂ) |
| 50 | 49 | ffvelcdmda 7104 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑧)‘𝑗) ∈ ℂ) |
| 51 | 48 | abscld 15475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) ∈ ℝ) |
| 52 | 51 | rexrd 11311 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) ∈
ℝ*) |
| 53 | 18 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
| 54 | | iccssxr 13470 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
| 55 | 6, 7, 13 | radcnvcl 26460 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
| 56 | 54, 55 | sselid 3981 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
| 57 | 56 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑅 ∈
ℝ*) |
| 58 | | 0cn 11253 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
| 59 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 60 | 59 | cnmetdval 24791 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑧(abs
∘ − )0) = (abs‘(𝑧 − 0))) |
| 61 | 48, 58, 60 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0))) |
| 62 | 48 | subid1d 11609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧 − 0) = 𝑧) |
| 63 | 62 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘(𝑧 − 0)) = (abs‘𝑧)) |
| 64 | 61, 63 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) = (abs‘𝑧)) |
| 65 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
| 66 | 65, 9 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2))) |
| 67 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
| 68 | | 0cnd 11254 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 0 ∈ ℂ) |
| 69 | | elbl3 24402 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) ∧ (0
∈ ℂ ∧ 𝑧
∈ ℂ)) → (𝑧
∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2))) |
| 70 | 67, 53, 68, 48, 69 | syl22anc 839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2))) |
| 71 | 66, 70 | mpbid 232 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2)) |
| 72 | 64, 71 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) < (((abs‘𝑎) + 𝑀) / 2)) |
| 73 | 16 | simp3d 1145 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅) |
| 74 | 73 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅) |
| 75 | 52, 53, 57, 72, 74 | xrlttrd 13201 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) < 𝑅) |
| 76 | 6, 47, 13, 48, 75 | radcnvlt2 26462 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ∈ dom ⇝ ) |
| 77 | 1, 45, 46, 50, 76 | isumclim2 15794 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ⇝ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
| 78 | 43 | sselda 3983 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑆) |
| 79 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐺‘𝑦) = (𝐺‘𝑧)) |
| 80 | 79 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑗) = ((𝐺‘𝑧)‘𝑗)) |
| 81 | 80 | sumeq2sdv 15739 |
. . . . . 6
⊢ (𝑦 = 𝑧 → Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
| 82 | | sumex 15724 |
. . . . . 6
⊢
Σ𝑗 ∈
ℕ0 ((𝐺‘𝑧)‘𝑗) ∈ V |
| 83 | 81, 12, 82 | fvmpt 7016 |
. . . . 5
⊢ (𝑧 ∈ 𝑆 → (𝐹‘𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
| 84 | 78, 83 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
| 85 | 77, 84 | breqtrrd 5171 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ⇝ (𝐹‘𝑧)) |
| 86 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (0...𝑘) = (0...𝑚)) |
| 87 | 86 | sumeq1d 15736 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) |
| 88 | 87 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
| 89 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))) = (𝑘 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))) |
| 90 | 31 | mptex 7243 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) ∈ V |
| 91 | 88, 89, 90 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
| 92 | 91 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
| 93 | 92 | fveq1d 6908 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧) = ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧)) |
| 94 | 79 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑖) = ((𝐺‘𝑧)‘𝑖)) |
| 95 | 94 | sumeq2sdv 15739 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
| 96 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) |
| 97 | | sumex 15724 |
. . . . . . . 8
⊢
Σ𝑖 ∈
(0...𝑚)((𝐺‘𝑧)‘𝑖) ∈ V |
| 98 | 95, 96, 97 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
| 99 | 98 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
| 100 | | eqidd 2738 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺‘𝑧)‘𝑖) = ((𝐺‘𝑧)‘𝑖)) |
| 101 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
| 102 | 101, 1 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
(ℤ≥‘0)) |
| 103 | 49 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐺‘𝑧):ℕ0⟶ℂ) |
| 104 | | elfznn0 13660 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0) |
| 105 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ (((𝐺‘𝑧):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → ((𝐺‘𝑧)‘𝑖) ∈ ℂ) |
| 106 | 103, 104,
105 | syl2an 596 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺‘𝑧)‘𝑖) ∈ ℂ) |
| 107 | 100, 102,
106 | fsumser 15766 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) →
Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖) = (seq0( + , (𝐺‘𝑧))‘𝑚)) |
| 108 | 93, 99, 107 | 3eqtrd 2781 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧) = (seq0( + , (𝐺‘𝑧))‘𝑚)) |
| 109 | 108 | mpteq2dva 5242 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚))) |
| 110 | | 0z 12624 |
. . . . . . 7
⊢ 0 ∈
ℤ |
| 111 | | seqfn 14054 |
. . . . . . 7
⊢ (0 ∈
ℤ → seq0( + , (𝐺‘𝑧)) Fn
(ℤ≥‘0)) |
| 112 | 110, 111 | ax-mp 5 |
. . . . . 6
⊢ seq0( + ,
(𝐺‘𝑧)) Fn
(ℤ≥‘0) |
| 113 | 1 | fneq2i 6666 |
. . . . . 6
⊢ (seq0( +
, (𝐺‘𝑧)) Fn ℕ0 ↔
seq0( + , (𝐺‘𝑧)) Fn
(ℤ≥‘0)) |
| 114 | 112, 113 | mpbir 231 |
. . . . 5
⊢ seq0( + ,
(𝐺‘𝑧)) Fn ℕ0 |
| 115 | | dffn5 6967 |
. . . . 5
⊢ (seq0( +
, (𝐺‘𝑧)) Fn ℕ0 ↔
seq0( + , (𝐺‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚))) |
| 116 | 114, 115 | mpbi 230 |
. . . 4
⊢ seq0( + ,
(𝐺‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚)) |
| 117 | 109, 116 | eqtr4di 2795 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) = seq0( + , (𝐺‘𝑧))) |
| 118 | | fvres 6925 |
. . . 4
⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
| 119 | 118 | adantl 481 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
| 120 | 85, 117, 119 | 3brtr4d 5175 |
. 2
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) ⇝ ((𝐹 ↾ 𝐵)‘𝑧)) |
| 121 | 91 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
| 122 | 121 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)) = (ℂ D (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)))) |
| 123 | | eqid 2737 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 124 | 123 | cnfldtopon 24803 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 125 | 124 | toponrestid 22927 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 126 | 2 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ℂ
∈ {ℝ, ℂ}) |
| 127 | 123 | cnfldtopn 24802 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
| 128 | 127 | blopn 24513 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∈
(TopOpen‘ℂfld)) |
| 129 | 10, 11, 18, 128 | mp3an2i 1468 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∈
(TopOpen‘ℂfld)) |
| 130 | 9, 129 | eqeltrid 2845 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ∈
(TopOpen‘ℂfld)) |
| 131 | 130 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ∈
(TopOpen‘ℂfld)) |
| 132 | | fzfid 14014 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) →
(0...𝑚) ∈
Fin) |
| 133 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) |
| 134 | 133 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
| 135 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ⊆
ℂ) |
| 136 | 135 | sselda 3983 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 137 | 136 | 3adant2 1132 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 138 | 6, 134, 137 | psergf 26455 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦):ℕ0⟶ℂ) |
| 139 | 104 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝑖 ∈ ℕ0) |
| 140 | 138, 139 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
| 141 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ℂ ∈ {ℝ,
ℂ}) |
| 142 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → (𝐴‘𝑖) ∈ ℂ) |
| 143 | 133, 104,
142 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝐴‘𝑖) ∈ ℂ) |
| 144 | 143 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → (𝐴‘𝑖) ∈ ℂ) |
| 145 | 136 | adantlr 715 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 146 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
| 147 | 104 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0) |
| 148 | | expcl 14120 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑦↑𝑖) ∈
ℂ) |
| 149 | 146, 147,
148 | syl2anr 597 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑖) ∈ ℂ) |
| 150 | 145, 149 | syldan 591 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → (𝑦↑𝑖) ∈ ℂ) |
| 151 | 144, 150 | mulcld 11281 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · (𝑦↑𝑖)) ∈ ℂ) |
| 152 | | ovexd 7466 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V) |
| 153 | | c0ex 11255 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
| 154 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑖 · (𝑦↑(𝑖 − 1))) ∈ V |
| 155 | 153, 154 | ifex 4576 |
. . . . . . . . . 10
⊢ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V |
| 156 | 155 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V) |
| 157 | 155 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V) |
| 158 | | dvexp2 25992 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
→ (ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
| 159 | 147, 158 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
| 160 | 21 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ⊆ ℂ) |
| 161 | 130 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ∈
(TopOpen‘ℂfld)) |
| 162 | 141, 149,
157, 159, 160, 125, 123, 161 | dvmptres 26001 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ (𝑦↑𝑖))) = (𝑦 ∈ 𝐵 ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
| 163 | 141, 150,
156, 162, 143 | dvmptcmul 26002 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
| 164 | 141, 151,
152, 163 | dvmptcl 25997 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
| 165 | 164 | 3impa 1110 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
| 166 | 104 | ad2antlr 727 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → 𝑖 ∈ ℕ0) |
| 167 | 6 | pserval2 26454 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ ((𝐺‘𝑦)‘𝑖) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
| 168 | 145, 166,
167 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑦)‘𝑖) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
| 169 | 168 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
| 170 | 169 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖))) = (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖))))) |
| 171 | 170, 163 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖))) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
| 172 | 125, 123,
126, 131, 132, 140, 165, 171 | dvmptfsum 26013 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
| 173 | 122, 172 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
| 174 | 173 | mpteq2dva 5242 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))) |
| 175 | | nnssnn0 12529 |
. . . . . 6
⊢ ℕ
⊆ ℕ0 |
| 176 | | resmpt 6055 |
. . . . . 6
⊢ (ℕ
⊆ ℕ0 → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))) |
| 177 | 175, 176 | ax-mp 5 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
| 178 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝑎↑𝑖) = (𝑥↑𝑖)) |
| 179 | 178 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) |
| 180 | 179 | mpteq2dv 5244 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖)))) |
| 181 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝑖 + 1) = (𝑛 + 1)) |
| 182 | | fvoveq1 7454 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑛 + 1))) |
| 183 | 181, 182 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
| 184 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (𝑥↑𝑖) = (𝑥↑𝑛)) |
| 185 | 183, 184 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
| 186 | 185 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
| 187 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
| 188 | | fvoveq1 7454 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝐴‘(𝑚 + 1)) = (𝐴‘(𝑛 + 1))) |
| 189 | 187, 188 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
| 190 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1)))) = (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))) |
| 191 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) ∈ V |
| 192 | 189, 190,
191 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
| 193 | 192 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
| 194 | 193 | mpteq2ia 5245 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ (((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
| 195 | 186, 194 | eqtr4i 2768 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛))) |
| 196 | 180, 195 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)))) |
| 197 | 196 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)))) |
| 198 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)) |
| 199 | 198 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
| 200 | 199 | sumeq2sdv 15739 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
| 201 | 200 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘)) = (𝑧 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
| 202 | | peano2nn0 12566 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
| 203 | 202 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℕ0) |
| 204 | 203 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℂ) |
| 205 | 133, 203 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝐴‘(𝑚 + 1)) ∈ ℂ) |
| 206 | 204, 205 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) ∈ ℂ) |
| 207 | 206 | fmpttd 7135 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 +
1)))):ℕ0⟶ℂ) |
| 208 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑗 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) |
| 209 | 208 | seqeq3d 14050 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑗 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗))) |
| 210 | 209 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑗 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + ,
((𝑎 ∈ ℂ ↦
(𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ )) |
| 211 | 210 | cbvrabv 3447 |
. . . . . . . . 9
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, ((𝑎 ∈ ℂ
↦ (𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ } = {𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ } |
| 212 | 211 | supeq1i 9487 |
. . . . . . . 8
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑗 ∈
ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ }, ℝ*,
< ) |
| 213 | 198 | seqeq3d 14050 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))) |
| 214 | 213 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) |
| 215 | 214 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) |
| 216 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚)) |
| 217 | 216 | mpteq2dv 5244 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
| 218 | 215, 217 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
| 219 | 218 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
| 220 | 17 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ) |
| 221 | 6, 12, 7, 13, 14, 15 | psercnlem1 26469 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |
| 222 | 221 | simp1d 1143 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
| 223 | 222 | rpxrd 13078 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ*) |
| 224 | 197, 207,
212 | radcnvcl 26460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ (0[,]+∞)) |
| 225 | 54, 224 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
| 226 | 221 | simp2d 1144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) |
| 227 | | cnvimass 6100 |
. . . . . . . . . . . . . . . 16
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
| 228 | | absf 15376 |
. . . . . . . . . . . . . . . . 17
⊢
abs:ℂ⟶ℝ |
| 229 | 228 | fdmi 6747 |
. . . . . . . . . . . . . . . 16
⊢ dom abs =
ℂ |
| 230 | 227, 229 | sseqtri 4032 |
. . . . . . . . . . . . . . 15
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
| 231 | 14, 230 | eqsstri 4030 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ⊆
ℂ |
| 232 | 231 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 233 | 232 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
| 234 | 233 | abscld 15475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
| 235 | 222 | rpred 13077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
| 236 | | avglt2 12505 |
. . . . . . . . . . 11
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑀
∈ ℝ) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀)) |
| 237 | 234, 235,
236 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀)) |
| 238 | 226, 237 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑀) |
| 239 | 222 | rpge0d 13081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ 𝑀) |
| 240 | 235, 239 | absidd 15461 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) = 𝑀) |
| 241 | 222 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℂ) |
| 242 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑀 → (𝑤↑𝑖) = (𝑀↑𝑖)) |
| 243 | 242 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑀 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) |
| 244 | 243 | mpteq2dv 5244 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑀 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
| 245 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑤 → (𝑎↑𝑖) = (𝑤↑𝑖)) |
| 246 | 245 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑤 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖))) |
| 247 | 246 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑤 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)))) |
| 248 | 247 | cbvmptv 5255 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑤 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)))) |
| 249 | | nn0ex 12532 |
. . . . . . . . . . . . . . . 16
⊢
ℕ0 ∈ V |
| 250 | 249 | mptex 7243 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) ∈ V |
| 251 | 244, 248,
250 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
| 252 | 241, 251 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
| 253 | 252 | seqeq3d 14050 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀)) = seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))))) |
| 254 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝐴‘𝑛) = (𝐴‘𝑖)) |
| 255 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑥↑𝑛) = (𝑥↑𝑖)) |
| 256 | 254, 255 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑖) · (𝑥↑𝑖))) |
| 257 | 256 | cbvmptv 5255 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑥↑𝑖))) |
| 258 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥↑𝑖) = (𝑦↑𝑖)) |
| 259 | 258 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐴‘𝑖) · (𝑥↑𝑖)) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
| 260 | 259 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑥↑𝑖))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
| 261 | 257, 260 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
| 262 | 261 | cbvmptv 5255 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
| 263 | 6, 262 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
| 264 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (𝐺‘𝑟) = (𝐺‘𝑠)) |
| 265 | 264 | seqeq3d 14050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑠))) |
| 266 | 265 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑠 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ )) |
| 267 | 266 | cbvrabv 3447 |
. . . . . . . . . . . . . . 15
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑠 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑠)) ∈ dom ⇝
} |
| 268 | 267 | supeq1i 9487 |
. . . . . . . . . . . . . 14
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑠 ∈
ℝ ∣ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ }, ℝ*,
< ) |
| 269 | 13, 268 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝑅 = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ }, ℝ*,
< ) |
| 270 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) |
| 271 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) |
| 272 | 221 | simp3d 1145 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) |
| 273 | 240, 272 | eqbrtrd 5165 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) < 𝑅) |
| 274 | 263, 269,
270, 271, 241, 273 | dvradcnv 26464 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) ∈ dom ⇝ ) |
| 275 | 253, 274 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀)) ∈ dom ⇝ ) |
| 276 | 197, 207,
212, 241, 275 | radcnvle 26463 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 277 | 240, 276 | eqbrtrrd 5167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 278 | 18, 223, 225, 238, 277 | xrltletrd 13203 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 279 | 197, 201,
207, 212, 219, 220, 278, 41 | pserulm 26465 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘))) |
| 280 | 21 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 281 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑦 → (𝑎↑𝑖) = (𝑦↑𝑖)) |
| 282 | 281 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑦 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) |
| 283 | 282 | mpteq2dv 5244 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑦 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
| 284 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) |
| 285 | 249 | mptex 7243 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) ∈ V |
| 286 | 283, 284,
285 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
| 287 | 280, 286 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
| 288 | 287 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
| 289 | 288 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘)) |
| 290 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
| 291 | | fvoveq1 7454 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑘 + 1))) |
| 292 | 290, 291 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) |
| 293 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑦↑𝑖) = (𝑦↑𝑘)) |
| 294 | 292, 293 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 295 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) |
| 296 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) ∈ V |
| 297 | 294, 295,
296 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 298 | 297 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 299 | 289, 298 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 300 | 299 | sumeq2dv 15738 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 301 | 300 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
| 302 | 279, 301 | breqtrd 5169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
| 303 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 304 | | 1e0p1 12775 |
. . . . . . . . 9
⊢ 1 = (0 +
1) |
| 305 | 304 | fveq2i 6909 |
. . . . . . . 8
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
| 306 | 303, 305 | eqtri 2765 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘(0 + 1)) |
| 307 | | 1zzd 12648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 1 ∈ ℤ) |
| 308 | | 0zd 12625 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 0 ∈ ℤ) |
| 309 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
| 310 | 309 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℂ) |
| 311 | 310 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑖 + 1) ∈
ℂ) |
| 312 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
| 313 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴:ℕ0⟶ℂ ∧
(𝑖 + 1) ∈
ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ) |
| 314 | 312, 309,
313 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ) |
| 315 | 311, 314 | mulcld 11281 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) ∈ ℂ) |
| 316 | 280, 148 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑦↑𝑖) ∈ ℂ) |
| 317 | 315, 316 | mulcld 11281 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)) ∈ ℂ) |
| 318 | 287, 317 | fmpt3d 7136 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦):ℕ0⟶ℂ) |
| 319 | 318 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑚) ∈ ℂ) |
| 320 | 1, 308, 319 | serf 14071 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)):ℕ0⟶ℂ) |
| 321 | 320 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → (seq0( +
, ((𝑎 ∈ ℂ
↦ (𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) ∈ ℂ) |
| 322 | 321 | an32s 652 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) ∈ ℂ) |
| 323 | 322 | fmpttd 7135 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ) |
| 324 | 30, 31 | elmap 8911 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ) |
| 325 | 323, 324 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑m 𝐵)) |
| 326 | 325 | fmpttd 7135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))):ℕ0⟶(ℂ
↑m 𝐵)) |
| 327 | | elfznn 13593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ) |
| 328 | 327 | nnne0d 12316 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ≠ 0) |
| 329 | 328 | neneqd 2945 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑚) → ¬ 𝑖 = 0) |
| 330 | 329 | iffalsed 4536 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑚) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = (𝑖 · (𝑦↑(𝑖 − 1)))) |
| 331 | 330 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑚) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))) |
| 332 | 331 | sumeq2i 15734 |
. . . . . . . . . . . 12
⊢
Σ𝑖 ∈
(1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) |
| 333 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 1 ∈ ℤ) |
| 334 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
| 335 | 334 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑚 ∈ ℤ) |
| 336 | 271 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
| 337 | 327 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ0) |
| 338 | 336, 337,
142 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝐴‘𝑖) ∈ ℂ) |
| 339 | 327 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ) |
| 340 | 339 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℂ) |
| 341 | 280 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
| 342 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (𝑖 − 1) ∈
ℕ0) |
| 343 | 327, 342 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑚) → (𝑖 − 1) ∈
ℕ0) |
| 344 | | expcl 14120 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℂ ∧ (𝑖 − 1) ∈
ℕ0) → (𝑦↑(𝑖 − 1)) ∈ ℂ) |
| 345 | 341, 343,
344 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑦↑(𝑖 − 1)) ∈ ℂ) |
| 346 | 340, 345 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑖 · (𝑦↑(𝑖 − 1))) ∈
ℂ) |
| 347 | 338, 346 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) ∈
ℂ) |
| 348 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝐴‘𝑖) = (𝐴‘(𝑘 + 1))) |
| 349 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1)) |
| 350 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑘 + 1) → (𝑖 − 1) = ((𝑘 + 1) − 1)) |
| 351 | 350 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑘 + 1) → (𝑦↑(𝑖 − 1)) = (𝑦↑((𝑘 + 1) − 1))) |
| 352 | 349, 351 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (𝑦↑(𝑖 − 1))) = ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) |
| 353 | 348, 352 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
| 354 | 333, 333,
335, 347, 353 | fsumshftm 15817 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
| 355 | 332, 354 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
| 356 | | fz1ssfz0 13663 |
. . . . . . . . . . . . 13
⊢
(1...𝑚) ⊆
(0...𝑚) |
| 357 | 356 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (1...𝑚) ⊆ (0...𝑚)) |
| 358 | 331 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))) |
| 359 | 358, 347 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
| 360 | | eldif 3961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) ↔ (𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚))) |
| 361 | | elfzuz2 13569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (0...𝑚) → 𝑚 ∈
(ℤ≥‘0)) |
| 362 | | elfzp12 13643 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈
(ℤ≥‘0) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))) |
| 363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (0...𝑚) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))) |
| 364 | 363 | ibi 267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0...𝑚) → (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))) |
| 365 | 364 | ord 865 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0...𝑚) → (¬ 𝑖 = 0 → 𝑖 ∈ ((0 + 1)...𝑚))) |
| 366 | 365 | con1d 145 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0...𝑚) → (¬ 𝑖 ∈ ((0 + 1)...𝑚) → 𝑖 = 0)) |
| 367 | 366 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)) → 𝑖 = 0) |
| 368 | 360, 367 | sylbi 217 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) → 𝑖 = 0) |
| 369 | 304 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑚) = ((0 +
1)...𝑚) |
| 370 | 369 | difeq2i 4123 |
. . . . . . . . . . . . . . . . 17
⊢
((0...𝑚) ∖
(1...𝑚)) = ((0...𝑚) ∖ ((0 + 1)...𝑚)) |
| 371 | 368, 370 | eleq2s 2859 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 = 0) |
| 372 | 371 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → 𝑖 = 0) |
| 373 | 372 | iftrued 4533 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = 0) |
| 374 | 373 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · 0)) |
| 375 | | eldifi 4131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ (0...𝑚)) |
| 376 | 375, 104 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ ℕ0) |
| 377 | 336, 376,
142 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → (𝐴‘𝑖) ∈ ℂ) |
| 378 | 377 | mul01d 11460 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · 0) = 0) |
| 379 | 374, 378 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = 0) |
| 380 | | fzfid 14014 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (0...𝑚) ∈ Fin) |
| 381 | 357, 359,
379, 380 | fsumss 15761 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
| 382 | | 1m1e0 12338 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
| 383 | 382 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((1
− 1)...(𝑚 − 1))
= (0...(𝑚 −
1)) |
| 384 | 383 | sumeq1i 15733 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈ ((1
− 1)...(𝑚 −
1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) |
| 385 | | elfznn0 13660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...(𝑚 − 1)) → 𝑘 ∈ ℕ0) |
| 386 | 385 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℕ0) |
| 387 | 386, 297 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 388 | 341 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑦 ∈ ℂ) |
| 389 | 388, 286 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
| 390 | 389 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘)) |
| 391 | 336 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝐴:ℕ0⟶ℂ) |
| 392 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
| 393 | 386, 392 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈
ℕ0) |
| 394 | 391, 393 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝐴‘(𝑘 + 1)) ∈ ℂ) |
| 395 | 393 | nn0cnd 12589 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℂ) |
| 396 | | expcl 14120 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑦↑𝑘) ∈
ℂ) |
| 397 | 341, 385,
396 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑𝑘) ∈ ℂ) |
| 398 | 394, 395,
397 | mul12d 11470 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑𝑘))) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦↑𝑘)))) |
| 399 | 386 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℂ) |
| 400 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
| 401 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
| 402 | 399, 400,
401 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) − 1) = 𝑘) |
| 403 | 402 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) = (𝑦↑𝑘)) |
| 404 | 403 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑦↑𝑘))) |
| 405 | 404 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑𝑘)))) |
| 406 | 395, 394,
397 | mulassd 11284 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦↑𝑘)))) |
| 407 | 398, 405,
406 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
| 408 | 387, 390,
407 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
| 409 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → (𝑚 − 1) ∈
ℕ0) |
| 410 | 409 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈
ℕ0) |
| 411 | 410 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑚 − 1) ∈
ℕ0) |
| 412 | 411, 1 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑚 − 1) ∈
(ℤ≥‘0)) |
| 413 | 403, 397 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) ∈
ℂ) |
| 414 | 395, 413 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) ∈
ℂ) |
| 415 | 394, 414 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) ∈
ℂ) |
| 416 | 408, 412,
415 | fsumser 15766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
| 417 | 384, 416 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
| 418 | 355, 381,
417 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
| 419 | 418 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
| 420 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑚 − 1) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
| 421 | 420 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑚 − 1) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
| 422 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) = (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) |
| 423 | 31 | mptex 7243 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) ∈ V |
| 424 | 421, 422,
423 | fvmpt 7016 |
. . . . . . . . . 10
⊢ ((𝑚 − 1) ∈
ℕ0 → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
| 425 | 410, 424 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
| 426 | 419, 425 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1))) |
| 427 | 426 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ ↦ ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)))) |
| 428 | 1, 306, 4, 307, 326, 427 | ulmshft 26433 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) ↔ (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))) |
| 429 | 302, 428 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
| 430 | 177, 429 | eqbrtrid 5178 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾
ℕ)(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
| 431 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 432 | 431 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 1 ∈
ℕ0) |
| 433 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (0...𝑚) ∈ Fin) |
| 434 | 164 | an32s 652 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
| 435 | 433, 434 | fsumcl 15769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
| 436 | 435 | fmpttd 7135 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ) |
| 437 | 30, 31 | elmap 8911 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ
↑m 𝐵)
↔ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ) |
| 438 | 436, 437 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ
↑m 𝐵)) |
| 439 | 438 | fmpttd 7135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1))))))):ℕ0⟶(ℂ ↑m 𝐵)) |
| 440 | 1, 303, 432, 439 | ulmres 26431 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) ↔ ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾
ℕ)(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))) |
| 441 | 430, 440 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
| 442 | 174, 441 | eqbrtrd 5165 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
| 443 | 1, 3, 4, 34, 44, 120, 442 | ulmdv 26446 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |