Metamath Proof Explorer

Theorem ser1const

Description: Value of the partial series sum of a constant function. (Contributed by NM, 8-Aug-2005) (Revised by Mario Carneiro, 16-Feb-2014)

Ref Expression
Assertion ser1const 
|- ( ( A e. CC /\ N e. NN ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` N ) = ( N x. A ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( j = 1 -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( seq 1 ( + , ( NN X. { A } ) ) ` 1 ) )
2 oveq1 
 |-  ( j = 1 -> ( j x. A ) = ( 1 x. A ) )
3 1 2 eqeq12d 
 |-  ( j = 1 -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) <-> ( seq 1 ( + , ( NN X. { A } ) ) ` 1 ) = ( 1 x. A ) ) )
4 3 imbi2d 
 |-  ( j = 1 -> ( ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) ) <-> ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` 1 ) = ( 1 x. A ) ) ) )
5 fveq2 
 |-  ( j = k -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( seq 1 ( + , ( NN X. { A } ) ) ` k ) )
6 oveq1 
 |-  ( j = k -> ( j x. A ) = ( k x. A ) )
7 5 6 eqeq12d 
 |-  ( j = k -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) <-> ( seq 1 ( + , ( NN X. { A } ) ) ` k ) = ( k x. A ) ) )
8 7 imbi2d 
 |-  ( j = k -> ( ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) ) <-> ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` k ) = ( k x. A ) ) ) )
9 fveq2 
 |-  ( j = ( k + 1 ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) )
10 oveq1 
 |-  ( j = ( k + 1 ) -> ( j x. A ) = ( ( k + 1 ) x. A ) )
11 9 10 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) <-> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. A ) ) )
12 11 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) ) <-> ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. A ) ) ) )
13 fveq2 
 |-  ( j = N -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( seq 1 ( + , ( NN X. { A } ) ) ` N ) )
14 oveq1 
 |-  ( j = N -> ( j x. A ) = ( N x. A ) )
15 13 14 eqeq12d 
 |-  ( j = N -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) <-> ( seq 1 ( + , ( NN X. { A } ) ) ` N ) = ( N x. A ) ) )
16 15 imbi2d 
 |-  ( j = N -> ( ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` j ) = ( j x. A ) ) <-> ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` N ) = ( N x. A ) ) ) )
17 1z 
 |-  1 e. ZZ
18 1nn 
 |-  1 e. NN
19 fvconst2g 
 |-  ( ( A e. CC /\ 1 e. NN ) -> ( ( NN X. { A } ) ` 1 ) = A )
20 18 19 mpan2 
 |-  ( A e. CC -> ( ( NN X. { A } ) ` 1 ) = A )
21 mulid2 
 |-  ( A e. CC -> ( 1 x. A ) = A )
22 20 21 eqtr4d 
 |-  ( A e. CC -> ( ( NN X. { A } ) ` 1 ) = ( 1 x. A ) )
23 17 22 seq1i 
 |-  ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` 1 ) = ( 1 x. A ) )
24 oveq1 
 |-  ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) = ( k x. A ) -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + A ) = ( ( k x. A ) + A ) )
25 seqp1 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + ( ( NN X. { A } ) ` ( k + 1 ) ) ) )
26 nnuz 
 |-  NN = ( ZZ>= ` 1 )
27 25 26 eleq2s 
 |-  ( k e. NN -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + ( ( NN X. { A } ) ` ( k + 1 ) ) ) )
28 27 adantl 
 |-  ( ( A e. CC /\ k e. NN ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + ( ( NN X. { A } ) ` ( k + 1 ) ) ) )
29 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
30 fvconst2g 
 |-  ( ( A e. CC /\ ( k + 1 ) e. NN ) -> ( ( NN X. { A } ) ` ( k + 1 ) ) = A )
31 29 30 sylan2 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( NN X. { A } ) ` ( k + 1 ) ) = A )
32 31 oveq2d 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + ( ( NN X. { A } ) ` ( k + 1 ) ) ) = ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + A ) )
33 28 32 eqtrd 
 |-  ( ( A e. CC /\ k e. NN ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + A ) )
34 nncn 
 |-  ( k e. NN -> k e. CC )
35 id 
 |-  ( A e. CC -> A e. CC )
36 ax-1cn 
 |-  1 e. CC
37 adddir 
 |-  ( ( k e. CC /\ 1 e. CC /\ A e. CC ) -> ( ( k + 1 ) x. A ) = ( ( k x. A ) + ( 1 x. A ) ) )
38 36 37 mp3an2 
 |-  ( ( k e. CC /\ A e. CC ) -> ( ( k + 1 ) x. A ) = ( ( k x. A ) + ( 1 x. A ) ) )
39 34 35 38 syl2anr 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( k + 1 ) x. A ) = ( ( k x. A ) + ( 1 x. A ) ) )
40 21 adantr 
 |-  ( ( A e. CC /\ k e. NN ) -> ( 1 x. A ) = A )
41 40 oveq2d 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( k x. A ) + ( 1 x. A ) ) = ( ( k x. A ) + A ) )
42 39 41 eqtrd 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( k + 1 ) x. A ) = ( ( k x. A ) + A ) )
43 33 42 eqeq12d 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. A ) <-> ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) + A ) = ( ( k x. A ) + A ) ) )
44 24 43 syl5ibr 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) = ( k x. A ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. A ) ) )
45 44 expcom 
 |-  ( k e. NN -> ( A e. CC -> ( ( seq 1 ( + , ( NN X. { A } ) ) ` k ) = ( k x. A ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. A ) ) ) )
46 45 a2d 
 |-  ( k e. NN -> ( ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` k ) = ( k x. A ) ) -> ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` ( k + 1 ) ) = ( ( k + 1 ) x. A ) ) ) )
47 4 8 12 16 23 46 nnind 
 |-  ( N e. NN -> ( A e. CC -> ( seq 1 ( + , ( NN X. { A } ) ) ` N ) = ( N x. A ) ) )
48 47 impcom 
 |-  ( ( A e. CC /\ N e. NN ) -> ( seq 1 ( + , ( NN X. { A } ) ) ` N ) = ( N x. A ) )