Metamath Proof Explorer

Theorem esumfzf

Description: Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017)

Ref Expression
Hypothesis esumfzf.1 
|- F/_ k F
Assertion esumfzf 
|- ( ( F : NN --> ( 0 [,] +oo ) /\ N e. NN ) -> sum* k e. ( 1 ... N ) ( F ` k ) = ( seq 1 ( +e , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 esumfzf.1 
 |-  F/_ k F
2 nfv 
 |-  F/ k i = 1
3 oveq2 
 |-  ( i = 1 -> ( 1 ... i ) = ( 1 ... 1 ) )
4 2 3 esumeq1d 
 |-  ( i = 1 -> sum* k e. ( 1 ... i ) ( F ` k ) = sum* k e. ( 1 ... 1 ) ( F ` k ) )
5 fveq2 
 |-  ( i = 1 -> ( seq 1 ( +e , F ) ` i ) = ( seq 1 ( +e , F ) ` 1 ) )
6 4 5 eqeq12d 
 |-  ( i = 1 -> ( sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) <-> sum* k e. ( 1 ... 1 ) ( F ` k ) = ( seq 1 ( +e , F ) ` 1 ) ) )
7 6 imbi2d 
 |-  ( i = 1 -> ( ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) ) <-> ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... 1 ) ( F ` k ) = ( seq 1 ( +e , F ) ` 1 ) ) ) )
8 nfv 
 |-  F/ k i = n
9 oveq2 
 |-  ( i = n -> ( 1 ... i ) = ( 1 ... n ) )
10 8 9 esumeq1d 
 |-  ( i = n -> sum* k e. ( 1 ... i ) ( F ` k ) = sum* k e. ( 1 ... n ) ( F ` k ) )
11 fveq2 
 |-  ( i = n -> ( seq 1 ( +e , F ) ` i ) = ( seq 1 ( +e , F ) ` n ) )
12 10 11 eqeq12d 
 |-  ( i = n -> ( sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) <-> sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) )
13 12 imbi2d 
 |-  ( i = n -> ( ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) ) <-> ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) ) )
14 nfv 
 |-  F/ k i = ( n + 1 )
15 oveq2 
 |-  ( i = ( n + 1 ) -> ( 1 ... i ) = ( 1 ... ( n + 1 ) ) )
16 14 15 esumeq1d 
 |-  ( i = ( n + 1 ) -> sum* k e. ( 1 ... i ) ( F ` k ) = sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) )
17 fveq2 
 |-  ( i = ( n + 1 ) -> ( seq 1 ( +e , F ) ` i ) = ( seq 1 ( +e , F ) ` ( n + 1 ) ) )
18 16 17 eqeq12d 
 |-  ( i = ( n + 1 ) -> ( sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) <-> sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) = ( seq 1 ( +e , F ) ` ( n + 1 ) ) ) )
19 18 imbi2d 
 |-  ( i = ( n + 1 ) -> ( ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) ) <-> ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) = ( seq 1 ( +e , F ) ` ( n + 1 ) ) ) ) )
20 nfv 
 |-  F/ k i = N
21 oveq2 
 |-  ( i = N -> ( 1 ... i ) = ( 1 ... N ) )
22 20 21 esumeq1d 
 |-  ( i = N -> sum* k e. ( 1 ... i ) ( F ` k ) = sum* k e. ( 1 ... N ) ( F ` k ) )
23 fveq2 
 |-  ( i = N -> ( seq 1 ( +e , F ) ` i ) = ( seq 1 ( +e , F ) ` N ) )
24 22 23 eqeq12d 
 |-  ( i = N -> ( sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) <-> sum* k e. ( 1 ... N ) ( F ` k ) = ( seq 1 ( +e , F ) ` N ) ) )
25 24 imbi2d 
 |-  ( i = N -> ( ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... i ) ( F ` k ) = ( seq 1 ( +e , F ) ` i ) ) <-> ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... N ) ( F ` k ) = ( seq 1 ( +e , F ) ` N ) ) ) )
26 fveq2 
 |-  ( k = x -> ( F ` k ) = ( F ` x ) )
27 nfcv 
 |-  F/_ x { 1 }
28 nfcv 
 |-  F/_ k { 1 }
29 nfcv 
 |-  F/_ x ( F ` k )
30 nfcv 
 |-  F/_ k x
31 1 30 nffv 
 |-  F/_ k ( F ` x )
32 26 27 28 29 31 cbvesum 
 |-  sum* k e. { 1 } ( F ` k ) = sum* x e. { 1 } ( F ` x )
33 simpr 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x = 1 ) -> x = 1 )
34 33 fveq2d 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ x = 1 ) -> ( F ` x ) = ( F ` 1 ) )
35 1z 
 |-  1 e. ZZ
36 35 a1i 
 |-  ( F : NN --> ( 0 [,] +oo ) -> 1 e. ZZ )
37 1nn 
 |-  1 e. NN
38 ffvelcdm 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ 1 e. NN ) -> ( F ` 1 ) e. ( 0 [,] +oo ) )
39 37 38 mpan2 
 |-  ( F : NN --> ( 0 [,] +oo ) -> ( F ` 1 ) e. ( 0 [,] +oo ) )
40 34 36 39 esumsn 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* x e. { 1 } ( F ` x ) = ( F ` 1 ) )
41 32 40 eqtrid 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* k e. { 1 } ( F ` k ) = ( F ` 1 ) )
42 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
43 35 42 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
44 esumeq1 
 |-  ( ( 1 ... 1 ) = { 1 } -> sum* k e. ( 1 ... 1 ) ( F ` k ) = sum* k e. { 1 } ( F ` k ) )
45 43 44 ax-mp 
 |-  sum* k e. ( 1 ... 1 ) ( F ` k ) = sum* k e. { 1 } ( F ` k )
46 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( +e , F ) ` 1 ) = ( F ` 1 ) )
47 35 46 ax-mp 
 |-  ( seq 1 ( +e , F ) ` 1 ) = ( F ` 1 )
48 41 45 47 3eqtr4g 
 |-  ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... 1 ) ( F ` k ) = ( seq 1 ( +e , F ) ` 1 ) )
49 simpl 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> n e. NN )
50 nnuz 
 |-  NN = ( ZZ>= ` 1 )
51 49 50 eleqtrdi 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> n e. ( ZZ>= ` 1 ) )
52 seqp1 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( seq 1 ( +e , F ) ` ( n + 1 ) ) = ( ( seq 1 ( +e , F ) ` n ) +e ( F ` ( n + 1 ) ) ) )
53 51 52 syl 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( seq 1 ( +e , F ) ` ( n + 1 ) ) = ( ( seq 1 ( +e , F ) ` n ) +e ( F ` ( n + 1 ) ) ) )
54 53 adantr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) -> ( seq 1 ( +e , F ) ` ( n + 1 ) ) = ( ( seq 1 ( +e , F ) ` n ) +e ( F ` ( n + 1 ) ) ) )
55 simpr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) -> sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) )
56 55 oveq1d 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) +e ( F ` ( n + 1 ) ) ) = ( ( seq 1 ( +e , F ) ` n ) +e ( F ` ( n + 1 ) ) ) )
57 nfv 
 |-  F/ k n e. NN
58 57 nfci 
 |-  F/_ k NN
59 nfcv 
 |-  F/_ k ( 0 [,] +oo )
60 1 58 59 nff 
 |-  F/ k F : NN --> ( 0 [,] +oo )
61 57 60 nfan 
 |-  F/ k ( n e. NN /\ F : NN --> ( 0 [,] +oo ) )
62 fzsuc 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
63 51 62 syl 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
64 61 63 esumeq1d 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) = sum* k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( F ` k ) )
65 nfcv 
 |-  F/_ k ( 1 ... n )
66 nfcv 
 |-  F/_ k { ( n + 1 ) }
67 ovexd 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( 1 ... n ) e. _V )
68 snex 
 |-  { ( n + 1 ) } e. _V
69 68 a1i 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> { ( n + 1 ) } e. _V )
70 fzp1disj 
 |-  ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/)
71 70 a1i 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( ( 1 ... n ) i^i { ( n + 1 ) } ) = (/) )
72 simplr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. ( 1 ... n ) ) -> F : NN --> ( 0 [,] +oo ) )
73 fzssnn 
 |-  ( 1 e. NN -> ( 1 ... n ) C_ NN )
74 37 73 ax-mp 
 |-  ( 1 ... n ) C_ NN
75 simpr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. ( 1 ... n ) ) -> k e. ( 1 ... n ) )
76 74 75 sselid 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. ( 1 ... n ) ) -> k e. NN )
77 72 76 ffvelcdmd 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. ( 1 ... n ) ) -> ( F ` k ) e. ( 0 [,] +oo ) )
78 simplr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> F : NN --> ( 0 [,] +oo ) )
79 simpr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> k e. { ( n + 1 ) } )
80 velsn 
 |-  ( k e. { ( n + 1 ) } <-> k = ( n + 1 ) )
81 79 80 sylib 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> k = ( n + 1 ) )
82 simpll 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> n e. NN )
83 82 peano2nnd 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> ( n + 1 ) e. NN )
84 81 83 eqeltrd 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> k e. NN )
85 78 84 ffvelcdmd 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ k e. { ( n + 1 ) } ) -> ( F ` k ) e. ( 0 [,] +oo ) )
86 61 65 66 67 69 71 77 85 esumsplit 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> sum* k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( F ` k ) = ( sum* k e. ( 1 ... n ) ( F ` k ) +e sum* k e. { ( n + 1 ) } ( F ` k ) ) )
87 nfcv 
 |-  F/_ x { ( n + 1 ) }
88 26 87 66 29 31 cbvesum 
 |-  sum* k e. { ( n + 1 ) } ( F ` k ) = sum* x e. { ( n + 1 ) } ( F ` x )
89 simpr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ x = ( n + 1 ) ) -> x = ( n + 1 ) )
90 89 fveq2d 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ x = ( n + 1 ) ) -> ( F ` x ) = ( F ` ( n + 1 ) ) )
91 49 peano2nnd 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( n + 1 ) e. NN )
92 simpr 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> F : NN --> ( 0 [,] +oo ) )
93 92 91 ffvelcdmd 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( F ` ( n + 1 ) ) e. ( 0 [,] +oo ) )
94 90 91 93 esumsn 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> sum* x e. { ( n + 1 ) } ( F ` x ) = ( F ` ( n + 1 ) ) )
95 88 94 eqtrid 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> sum* k e. { ( n + 1 ) } ( F ` k ) = ( F ` ( n + 1 ) ) )
96 95 oveq2d 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) +e sum* k e. { ( n + 1 ) } ( F ` k ) ) = ( sum* k e. ( 1 ... n ) ( F ` k ) +e ( F ` ( n + 1 ) ) ) )
97 64 86 96 3eqtrrd 
 |-  ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) +e ( F ` ( n + 1 ) ) ) = sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) )
98 97 adantr 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) +e ( F ` ( n + 1 ) ) ) = sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) )
99 54 56 98 3eqtr2rd 
 |-  ( ( ( n e. NN /\ F : NN --> ( 0 [,] +oo ) ) /\ sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) -> sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) = ( seq 1 ( +e , F ) ` ( n + 1 ) ) )
100 99 exp31 
 |-  ( n e. NN -> ( F : NN --> ( 0 [,] +oo ) -> ( sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) -> sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) = ( seq 1 ( +e , F ) ` ( n + 1 ) ) ) ) )
101 100 a2d 
 |-  ( n e. NN -> ( ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... n ) ( F ` k ) = ( seq 1 ( +e , F ) ` n ) ) -> ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... ( n + 1 ) ) ( F ` k ) = ( seq 1 ( +e , F ) ` ( n + 1 ) ) ) ) )
102 7 13 19 25 48 101 nnind 
 |-  ( N e. NN -> ( F : NN --> ( 0 [,] +oo ) -> sum* k e. ( 1 ... N ) ( F ` k ) = ( seq 1 ( +e , F ) ` N ) ) )
103 102 impcom 
 |-  ( ( F : NN --> ( 0 [,] +oo ) /\ N e. NN ) -> sum* k e. ( 1 ... N ) ( F ` k ) = ( seq 1 ( +e , F ) ` N ) )