Metamath Proof Explorer

Theorem clim2ser2

Description: The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
clim2ser.2 ${⊢}{\phi }\to {N}\in {Z}$
clim2ser.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
clim2ser2.5 ${⊢}{\phi }\to seq\left({N}+1\right)\left(+,{F}\right)⇝{A}$
Assertion clim2ser2 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝\left({A}+seq{M}\left(+,{F}\right)\left({N}\right)\right)$

Proof

Step Hyp Ref Expression
1 clim2ser.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 clim2ser.2 ${⊢}{\phi }\to {N}\in {Z}$
3 clim2ser.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
4 clim2ser2.5 ${⊢}{\phi }\to seq\left({N}+1\right)\left(+,{F}\right)⇝{A}$
5 eqid ${⊢}{ℤ}_{\ge \left({N}+1\right)}={ℤ}_{\ge \left({N}+1\right)}$
6 2 1 eleqtrdi ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
7 peano2uz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1\in {ℤ}_{\ge {M}}$
8 6 7 syl ${⊢}{\phi }\to {N}+1\in {ℤ}_{\ge {M}}$
9 eluzelz ${⊢}{N}+1\in {ℤ}_{\ge {M}}\to {N}+1\in ℤ$
10 8 9 syl ${⊢}{\phi }\to {N}+1\in ℤ$
11 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
12 6 11 syl ${⊢}{\phi }\to {M}\in ℤ$
13 1 12 3 serf ${⊢}{\phi }\to seq{M}\left(+,{F}\right):{Z}⟶ℂ$
14 13 2 ffvelrnd ${⊢}{\phi }\to seq{M}\left(+,{F}\right)\left({N}\right)\in ℂ$
15 seqex ${⊢}seq{M}\left(+,{F}\right)\in \mathrm{V}$
16 15 a1i ${⊢}{\phi }\to seq{M}\left(+,{F}\right)\in \mathrm{V}$
17 8 1 eleqtrrdi ${⊢}{\phi }\to {N}+1\in {Z}$
18 1 uztrn2 ${⊢}\left({N}+1\in {Z}\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {k}\in {Z}$
19 17 18 sylan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {k}\in {Z}$
20 19 3 syldan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {F}\left({k}\right)\in ℂ$
21 5 10 20 serf ${⊢}{\phi }\to seq\left({N}+1\right)\left(+,{F}\right):{ℤ}_{\ge \left({N}+1\right)}⟶ℂ$
22 21 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to seq\left({N}+1\right)\left(+,{F}\right)\left({j}\right)\in ℂ$
23 14 adantr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to seq{M}\left(+,{F}\right)\left({N}\right)\in ℂ$
24 addcl ${⊢}\left({k}\in ℂ\wedge {x}\in ℂ\right)\to {k}+{x}\in ℂ$
25 24 adantl ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge \left({k}\in ℂ\wedge {x}\in ℂ\right)\right)\to {k}+{x}\in ℂ$
26 addass ${⊢}\left({k}\in ℂ\wedge {x}\in ℂ\wedge {y}\in ℂ\right)\to {k}+{x}+{y}={k}+{x}+{y}$
27 26 adantl ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge \left({k}\in ℂ\wedge {x}\in ℂ\wedge {y}\in ℂ\right)\right)\to {k}+{x}+{y}={k}+{x}+{y}$
28 simpr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {j}\in {ℤ}_{\ge \left({N}+1\right)}$
29 6 adantr ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}\in {ℤ}_{\ge {M}}$
30 elfzuz ${⊢}{k}\in \left({M}\dots {j}\right)\to {k}\in {ℤ}_{\ge {M}}$
31 30 1 eleqtrrdi ${⊢}{k}\in \left({M}\dots {j}\right)\to {k}\in {Z}$
32 31 3 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {j}\right)\right)\to {F}\left({k}\right)\in ℂ$
33 32 adantlr ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {k}\in \left({M}\dots {j}\right)\right)\to {F}\left({k}\right)\in ℂ$
34 25 27 28 29 33 seqsplit ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to seq{M}\left(+,{F}\right)\left({j}\right)=seq{M}\left(+,{F}\right)\left({N}\right)+seq\left({N}+1\right)\left(+,{F}\right)\left({j}\right)$
35 23 22 34 comraddd ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to seq{M}\left(+,{F}\right)\left({j}\right)=seq\left({N}+1\right)\left(+,{F}\right)\left({j}\right)+seq{M}\left(+,{F}\right)\left({N}\right)$
36 5 10 4 14 16 22 35 climaddc1 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝\left({A}+seq{M}\left(+,{F}\right)\left({N}\right)\right)$