Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  abelthlem6 Structured version   Visualization version   GIF version

Theorem abelthlem6 23994
 Description: Lemma for abelth 23999. (Contributed by Mario Carneiro, 2-Apr-2015.)
Hypotheses
Ref Expression
abelth.1 (𝜑𝐴:ℕ0⟶ℂ)
abelth.2 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3 (𝜑𝑀 ∈ ℝ)
abelth.4 (𝜑 → 0 ≤ 𝑀)
abelth.5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
abelth.7 (𝜑 → seq0( + , 𝐴) ⇝ 0)
abelthlem6.1 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
Assertion
Ref Expression
abelthlem6 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
Distinct variable groups:   𝑥,𝑛,𝑧,𝑀   𝑛,𝑋,𝑥,𝑧   𝐴,𝑛,𝑥,𝑧   𝜑,𝑛,𝑥   𝑆,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑧)   𝑆(𝑧)   𝐹(𝑥,𝑧,𝑛)

Proof of Theorem abelthlem6
Dummy variables 𝑖 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 abelthlem6.1 . . . 4 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
21eldifad 3552 . . 3 (𝜑𝑋𝑆)
3 oveq1 6556 . . . . . 6 (𝑥 = 𝑋 → (𝑥𝑛) = (𝑋𝑛))
43oveq2d 6565 . . . . 5 (𝑥 = 𝑋 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑛) · (𝑋𝑛)))
54sumeq2sdv 14282 . . . 4 (𝑥 = 𝑋 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑋𝑛)))
6 abelth.6 . . . 4 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
7 sumex 14266 . . . 4 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑋𝑛)) ∈ V
85, 6, 7fvmpt 6191 . . 3 (𝑋𝑆 → (𝐹𝑋) = Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑋𝑛)))
92, 8syl 17 . 2 (𝜑 → (𝐹𝑋) = Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑋𝑛)))
10 nn0uz 11598 . . 3 0 = (ℤ‘0)
11 0zd 11266 . . 3 (𝜑 → 0 ∈ ℤ)
12 fveq2 6103 . . . . . 6 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
13 oveq2 6557 . . . . . 6 (𝑘 = 𝑛 → (𝑋𝑘) = (𝑋𝑛))
1412, 13oveq12d 6567 . . . . 5 (𝑘 = 𝑛 → ((𝐴𝑘) · (𝑋𝑘)) = ((𝐴𝑛) · (𝑋𝑛)))
15 eqid 2610 . . . . 5 (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))
16 ovex 6577 . . . . 5 ((𝐴𝑛) · (𝑋𝑛)) ∈ V
1714, 15, 16fvmpt 6191 . . . 4 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))‘𝑛) = ((𝐴𝑛) · (𝑋𝑛)))
1817adantl 481 . . 3 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))‘𝑛) = ((𝐴𝑛) · (𝑋𝑛)))
19 abelth.1 . . . . 5 (𝜑𝐴:ℕ0⟶ℂ)
2019ffvelrnda 6267 . . . 4 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
21 abelth.5 . . . . . . 7 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
22 ssrab2 3650 . . . . . . 7 {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⊆ ℂ
2321, 22eqsstri 3598 . . . . . 6 𝑆 ⊆ ℂ
2423, 2sseldi 3566 . . . . 5 (𝜑𝑋 ∈ ℂ)
25 expcl 12740 . . . . 5 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2624, 25sylan 487 . . . 4 ((𝜑𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2720, 26mulcld 9939 . . 3 ((𝜑𝑛 ∈ ℕ0) → ((𝐴𝑛) · (𝑋𝑛)) ∈ ℂ)
28 fveq2 6103 . . . . . . . . 9 (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
2928, 13oveq12d 6567 . . . . . . . 8 (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
30 eqid 2610 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))
31 ovex 6577 . . . . . . . 8 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ V
3229, 30, 31fvmpt 6191 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
3332adantl 481 . . . . . 6 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
3410, 11, 20serf 12691 . . . . . . . 8 (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ)
3534ffvelrnda 6267 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
3635, 26mulcld 9939 . . . . . 6 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
37 abelth.2 . . . . . . . . . 10 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
38 abelth.3 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
39 abelth.4 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑀)
4019, 37, 38, 39, 21abelthlem2 23990 . . . . . . . . 9 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
4140simprd 478 . . . . . . . 8 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
4241, 1sseldd 3569 . . . . . . 7 (𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1))
43 abelth.7 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ⇝ 0)
4419, 37, 38, 39, 21, 6, 43abelthlem5 23993 . . . . . . 7 ((𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4542, 44mpdan 699 . . . . . 6 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4610, 11, 33, 36, 45isumclim2 14331 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
47 seqex 12665 . . . . . 6 seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))) ∈ V
4847a1i 11 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))) ∈ V)
49 0nn0 11184 . . . . . . . 8 0 ∈ ℕ0
5049a1i 11 . . . . . . 7 (𝜑 → 0 ∈ ℕ0)
51 oveq1 6556 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑘 − 1) = (𝑖 − 1))
5251oveq2d 6565 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (0...(𝑘 − 1)) = (0...(𝑖 − 1)))
5352sumeq1d 14279 . . . . . . . . . . 11 (𝑘 = 𝑖 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) = Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚))
54 oveq2 6557 . . . . . . . . . . 11 (𝑘 = 𝑖 → (𝑋𝑘) = (𝑋𝑖))
5553, 54oveq12d 6567 . . . . . . . . . 10 (𝑘 = 𝑖 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚) · (𝑋𝑖)))
56 eqid 2610 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))
57 ovex 6577 . . . . . . . . . 10 𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚) · (𝑋𝑖)) ∈ V
5855, 56, 57fvmpt 6191 . . . . . . . . 9 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑖) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚) · (𝑋𝑖)))
5958adantl 481 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑖) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚) · (𝑋𝑖)))
60 fzfid 12634 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ0) → (0...(𝑖 − 1)) ∈ Fin)
6119adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ)
62 elfznn0 12302 . . . . . . . . . . 11 (𝑚 ∈ (0...(𝑖 − 1)) → 𝑚 ∈ ℕ0)
63 ffvelrn 6265 . . . . . . . . . . 11 ((𝐴:ℕ0⟶ℂ ∧ 𝑚 ∈ ℕ0) → (𝐴𝑚) ∈ ℂ)
6461, 62, 63syl2an 493 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑚 ∈ (0...(𝑖 − 1))) → (𝐴𝑚) ∈ ℂ)
6560, 64fsumcl 14311 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚) ∈ ℂ)
66 expcl 12740 . . . . . . . . . 10 ((𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑋𝑖) ∈ ℂ)
6724, 66sylan 487 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → (𝑋𝑖) ∈ ℂ)
6865, 67mulcld 9939 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴𝑚) · (𝑋𝑖)) ∈ ℂ)
6959, 68eqeltrd 2688 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑖) ∈ ℂ)
7011peano2zd 11361 . . . . . . . . 9 (𝜑 → (0 + 1) ∈ ℤ)
71 nnuz 11599 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
72 1e0p1 11428 . . . . . . . . . . . . 13 1 = (0 + 1)
7372fveq2i 6106 . . . . . . . . . . . 12 (ℤ‘1) = (ℤ‘(0 + 1))
7471, 73eqtri 2632 . . . . . . . . . . 11 ℕ = (ℤ‘(0 + 1))
7574eleq2i 2680 . . . . . . . . . 10 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ‘(0 + 1)))
76 nnm1nn0 11211 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
7776adantl 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑛 − 1) ∈ ℕ0)
78 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = (𝑛 − 1) → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘(𝑛 − 1)))
79 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑘 = (𝑛 − 1) → (𝑋𝑘) = (𝑋↑(𝑛 − 1)))
8078, 79oveq12d 6567 . . . . . . . . . . . . . 14 (𝑘 = (𝑛 − 1) → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))
8180oveq2d 6565 . . . . . . . . . . . . 13 (𝑘 = (𝑛 − 1) → (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))))
82 eqid 2610 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) = (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))
83 ovex 6577 . . . . . . . . . . . . 13 (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) ∈ V
8481, 82, 83fvmpt 6191 . . . . . . . . . . . 12 ((𝑛 − 1) ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘(𝑛 − 1)) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))))
8577, 84syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘(𝑛 − 1)) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))))
86 ax-1cn 9873 . . . . . . . . . . . 12 1 ∈ ℂ
87 nncn 10905 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
8887adantl 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
89 nn0ex 11175 . . . . . . . . . . . . . 14 0 ∈ V
9089mptex 6390 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ V
9190shftval 13662 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘(𝑛 − 1)))
9286, 88, 91sylancr 694 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘(𝑛 − 1)))
93 eqidd 2611 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴𝑚) = (𝐴𝑚))
9477, 10syl6eleq 2698 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑛 − 1) ∈ (ℤ‘0))
9519adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ0⟶ℂ)
96 elfznn0 12302 . . . . . . . . . . . . . . 15 (𝑚 ∈ (0...(𝑛 − 1)) → 𝑚 ∈ ℕ0)
9795, 96, 63syl2an 493 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴𝑚) ∈ ℂ)
9893, 94, 97fsumser 14308 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) = (seq0( + , 𝐴)‘(𝑛 − 1)))
99 expm1t 12750 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑋𝑛) = ((𝑋↑(𝑛 − 1)) · 𝑋))
10024, 99sylan 487 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑋𝑛) = ((𝑋↑(𝑛 − 1)) · 𝑋))
10124adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ ℂ)
102 expcl 12740 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑋↑(𝑛 − 1)) ∈ ℂ)
10324, 76, 102syl2an 493 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝑋↑(𝑛 − 1)) ∈ ℂ)
104101, 103mulcomd 9940 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (𝑋 · (𝑋↑(𝑛 − 1))) = ((𝑋↑(𝑛 − 1)) · 𝑋))
105100, 104eqtr4d 2647 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝑋𝑛) = (𝑋 · (𝑋↑(𝑛 − 1))))
10698, 105oveq12d 6567 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋 · (𝑋↑(𝑛 − 1)))))
107 nnnn0 11176 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
108107adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
109 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘 − 1) = (𝑛 − 1))
110109oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (0...(𝑘 − 1)) = (0...(𝑛 − 1)))
111110sumeq1d 14279 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) = Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚))
112111, 13oveq12d 6567 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)))
113 ovex 6577 . . . . . . . . . . . . . 14 𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)) ∈ V
114112, 56, 113fvmpt 6191 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)))
115108, 114syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)))
116 ffvelrn 6265 . . . . . . . . . . . . . 14 ((seq0( + , 𝐴):ℕ0⟶ℂ ∧ (𝑛 − 1) ∈ ℕ0) → (seq0( + , 𝐴)‘(𝑛 − 1)) ∈ ℂ)
11734, 76, 116syl2an 493 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (seq0( + , 𝐴)‘(𝑛 − 1)) ∈ ℂ)
118101, 117, 103mul12d 10124 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋 · (𝑋↑(𝑛 − 1)))))
119106, 115, 1183eqtr4d 2654 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))))
12085, 92, 1193eqtr4d 2654 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛))
12175, 120sylan2br 492 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ‘(0 + 1))) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛))
12270, 121seqfeq 12688 . . . . . . . 8 (𝜑 → seq(0 + 1)( + , ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)) = seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))))
123 fveq2 6103 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑖))
124123, 54oveq12d 6567 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖)))
125 ovex 6577 . . . . . . . . . . . . 13 ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖)) ∈ V
126124, 30, 125fvmpt 6191 . . . . . . . . . . . 12 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖)))
127126adantl 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖)))
12834ffvelrnda 6267 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ)
129128, 67mulcld 9939 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖)) ∈ ℂ)
130127, 129eqeltrd 2688 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑖) ∈ ℂ)
131124oveq2d 6565 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖))))
132 ovex 6577 . . . . . . . . . . . . 13 (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖))) ∈ V
133131, 82, 132fvmpt 6191 . . . . . . . . . . . 12 (𝑖 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑖) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖))))
134133adantl 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑖) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖))))
135127oveq2d 6565 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ℕ0) → (𝑋 · ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑖)) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋𝑖))))
136134, 135eqtr4d 2647 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑖) = (𝑋 · ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑖)))
13710, 11, 24, 46, 130, 136isermulc2 14236 . . . . . . . . 9 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
138 0z 11265 . . . . . . . . . 10 0 ∈ ℤ
139 1z 11284 . . . . . . . . . 10 1 ∈ ℤ
14090isershft 14242 . . . . . . . . . 10 ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ↔ seq(0 + 1)( + , ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
141138, 139, 140mp2an 704 . . . . . . . . 9 (seq0( + , (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ↔ seq(0 + 1)( + , ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
142137, 141sylib 207 . . . . . . . 8 (𝜑 → seq(0 + 1)( + , ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
143122, 142eqbrtrrd 4607 . . . . . . 7 (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
14410, 50, 69, 143clim2ser2 14234 . . . . . 6 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))) ⇝ ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0)))
145 seq1 12676 . . . . . . . . . . 11 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘0))
146138, 145ax-mp 5 . . . . . . . . . 10 (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘0)
147 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
148147oveq2d 6565 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → (0...(𝑘 − 1)) = (0...(0 − 1)))
149 0re 9919 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
150 ltm1 10742 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → (0 − 1) < 0)
151149, 150ax-mp 5 . . . . . . . . . . . . . . . . 17 (0 − 1) < 0
152 peano2zm 11297 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ℤ → (0 − 1) ∈ ℤ)
153138, 152ax-mp 5 . . . . . . . . . . . . . . . . . 18 (0 − 1) ∈ ℤ
154 fzn 12228 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) < 0 ↔ (0...(0 − 1)) = ∅))
155138, 153, 154mp2an 704 . . . . . . . . . . . . . . . . 17 ((0 − 1) < 0 ↔ (0...(0 − 1)) = ∅)
156151, 155mpbi 219 . . . . . . . . . . . . . . . 16 (0...(0 − 1)) = ∅
157148, 156syl6eq 2660 . . . . . . . . . . . . . . 15 (𝑘 = 0 → (0...(𝑘 − 1)) = ∅)
158157sumeq1d 14279 . . . . . . . . . . . . . 14 (𝑘 = 0 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) = Σ𝑚 ∈ ∅ (𝐴𝑚))
159 sum0 14299 . . . . . . . . . . . . . 14 Σ𝑚 ∈ ∅ (𝐴𝑚) = 0
160158, 159syl6eq 2660 . . . . . . . . . . . . 13 (𝑘 = 0 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) = 0)
161 oveq2 6557 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑋𝑘) = (𝑋↑0))
162160, 161oveq12d 6567 . . . . . . . . . . . 12 (𝑘 = 0 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)) = (0 · (𝑋↑0)))
163 ovex 6577 . . . . . . . . . . . 12 (0 · (𝑋↑0)) ∈ V
164162, 56, 163fvmpt 6191 . . . . . . . . . . 11 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘0) = (0 · (𝑋↑0)))
16549, 164ax-mp 5 . . . . . . . . . 10 ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘0) = (0 · (𝑋↑0))
166146, 165eqtri 2632 . . . . . . . . 9 (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0) = (0 · (𝑋↑0))
167 expcl 12740 . . . . . . . . . . 11 ((𝑋 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝑋↑0) ∈ ℂ)
16824, 49, 167sylancl 693 . . . . . . . . . 10 (𝜑 → (𝑋↑0) ∈ ℂ)
169168mul02d 10113 . . . . . . . . 9 (𝜑 → (0 · (𝑋↑0)) = 0)
170166, 169syl5eq 2656 . . . . . . . 8 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0) = 0)
171170oveq2d 6565 . . . . . . 7 (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0)) = ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + 0))
17210, 11, 33, 36, 45isumcl 14334 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
17324, 172mulcld 9939 . . . . . . . 8 (𝜑 → (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
174173addid1d 10115 . . . . . . 7 (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + 0) = (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
175171, 174eqtrd 2644 . . . . . 6 (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘0)) = (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
176144, 175breqtrd 4609 . . . . 5 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
17710, 11, 130serf 12691 . . . . . 6 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))):ℕ0⟶ℂ)
178177ffvelrnda 6267 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑖) ∈ ℂ)
17910, 11, 69serf 12691 . . . . . 6 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))):ℕ0⟶ℂ)
180179ffvelrnda 6267 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘𝑖) ∈ ℂ)
181 simpr 476 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
182181, 10syl6eleq 2698 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ (ℤ‘0))
183 simpl 472 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → 𝜑)
184 elfznn0 12302 . . . . . . 7 (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℕ0)
18533, 36eqeltrd 2688 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
186183, 184, 185syl2an 493 . . . . . 6 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
187114adantl 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)))
188 fzfid 12634 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (0...(𝑛 − 1)) ∈ Fin)
18919adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ)
190189, 96, 63syl2an 493 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴𝑚) ∈ ℂ)
191188, 190fsumcl 14311 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) ∈ ℂ)
192191, 26mulcld 9939 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛)) ∈ ℂ)
193187, 192eqeltrd 2688 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
194183, 184, 193syl2an 493 . . . . . 6 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
195 eqidd 2611 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...𝑛)) → (𝐴𝑚) = (𝐴𝑚))
196 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
197196, 10syl6eleq 2698 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ (ℤ‘0))
198 elfznn0 12302 . . . . . . . . . . . . . . 15 (𝑚 ∈ (0...𝑛) → 𝑚 ∈ ℕ0)
199189, 198, 63syl2an 493 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...𝑛)) → (𝐴𝑚) ∈ ℂ)
200195, 197, 199fsumser 14308 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → Σ𝑚 ∈ (0...𝑛)(𝐴𝑚) = (seq0( + , 𝐴)‘𝑛))
201 fveq2 6103 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝐴𝑚) = (𝐴𝑛))
202197, 199, 201fsumm1 14324 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → Σ𝑚 ∈ (0...𝑛)(𝐴𝑚) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) + (𝐴𝑛)))
203200, 202eqtr3d 2646 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) + (𝐴𝑛)))
204203oveq1d 6564 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚)) = ((Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) + (𝐴𝑛)) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚)))
205191, 20pncan2d 10273 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → ((Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) + (𝐴𝑛)) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚)) = (𝐴𝑛))
206204, 205eqtr2d 2645 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) = ((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚)))
207206oveq1d 6564 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝐴𝑛) · (𝑋𝑛)) = (((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚)) · (𝑋𝑛)))
20835, 191, 26subdird 10366 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚)) · (𝑋𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛))))
209207, 208eqtrd 2644 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝐴𝑛) · (𝑋𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛))))
21033, 187oveq12d 6567 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴𝑚) · (𝑋𝑛))))
211209, 18, 2103eqtr4d 2654 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))‘𝑛) = (((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛)))
212183, 184, 211syl2an 493 . . . . . 6 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))‘𝑛) = (((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘)))‘𝑛)))
213182, 186, 194, 212sersub 12706 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘))))‘𝑖) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑖) − (seq0( + , (𝑘 ∈ ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴𝑚) · (𝑋𝑘))))‘𝑖)))
21410, 11, 46, 48, 176, 178, 180, 213climsub 14212 . . . 4 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))) ⇝ (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
215 1cnd 9935 . . . . . 6 (𝜑 → 1 ∈ ℂ)
216215, 24, 172subdird 10366 . . . . 5 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((1 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
217172mulid2d 9937 . . . . . 6 (𝜑 → (1 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
218217oveq1d 6564 . . . . 5 (𝜑 → ((1 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
219216, 218eqtrd 2644 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
220214, 219breqtrrd 4611 . . 3 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((𝐴𝑘) · (𝑋𝑘)))) ⇝ ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
22110, 11, 18, 27, 220isumclim 14330 . 2 (𝜑 → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑋𝑛)) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
2229, 221eqtrd 2644 1 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  seqcseq 12663  ↑cexp 12722   shift cshi 13654  abscabs 13822   ⇝ cli 14063  Σcsu 14264  ballcbl 19554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-xadd 11823  df-ico 12052  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562 This theorem is referenced by:  abelthlem7  23996
 Copyright terms: Public domain W3C validator