This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fz1sumconst

Description: The sum of N constant terms ( k is not free in C ). (Contributed by SN, 21-Mar-2025)

Ref Expression
Hypotheses fz1sumconst.n 
|- ( ph -> N e. NN0 )
fz1sumconst.c 
|- ( ph -> C e. CC )
Assertion fz1sumconst 
|- ( ph -> sum_ k e. ( 1 ... N ) C = ( N x. C ) )

Proof

Step Hyp Ref Expression
1 fz1sumconst.n 
 |-  ( ph -> N e. NN0 )
2 fz1sumconst.c 
 |-  ( ph -> C e. CC )
3 fzfi 
 |-  ( 1 ... N ) e. Fin
4 fsumconst 
 |-  ( ( ( 1 ... N ) e. Fin /\ C e. CC ) -> sum_ k e. ( 1 ... N ) C = ( ( # ` ( 1 ... N ) ) x. C ) )
5 3 2 4 sylancr 
 |-  ( ph -> sum_ k e. ( 1 ... N ) C = ( ( # ` ( 1 ... N ) ) x. C ) )
6 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
7 1 6 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
8 7 oveq1d 
 |-  ( ph -> ( ( # ` ( 1 ... N ) ) x. C ) = ( N x. C ) )
9 5 8 eqtrd 
 |-  ( ph -> sum_ k e. ( 1 ... N ) C = ( N x. C ) )