Metamath Proof Explorer

Theorem aks4d1p1p1

Description: Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024)

Ref Expression
Hypotheses aks4d1p1p1.1 
|- ( ph -> A e. RR+ )
aks4d1p1p1.2 
|- ( ph -> N e. NN )
Assertion aks4d1p1p1 
|- ( ph -> prod_ k e. ( 1 ... N ) ( A ^c k ) = ( A ^c sum_ k e. ( 1 ... N ) k ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p1.1 
 |-  ( ph -> A e. RR+ )
2 aks4d1p1p1.2 
 |-  ( ph -> N e. NN )
3 1 rpcnd 
 |-  ( ph -> A e. CC )
4 3 adantr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> A e. CC )
5 1 rpne0d 
 |-  ( ph -> A =/= 0 )
6 5 adantr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> A =/= 0 )
7 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
8 7 zcnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
9 8 adantl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> k e. CC )
10 4 6 9 3jca 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( A e. CC /\ A =/= 0 /\ k e. CC ) )
11 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ k e. CC ) -> ( A ^c k ) = ( exp ` ( k x. ( log ` A ) ) ) )
12 10 11 syl 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( A ^c k ) = ( exp ` ( k x. ( log ` A ) ) ) )
13 12 prodeq2dv 
 |-  ( ph -> prod_ k e. ( 1 ... N ) ( A ^c k ) = prod_ k e. ( 1 ... N ) ( exp ` ( k x. ( log ` A ) ) ) )
14 eqid 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 2 15 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
17 eluzelcn 
 |-  ( k e. ( ZZ>= ` 1 ) -> k e. CC )
18 17 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> k e. CC )
19 3 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> A e. CC )
20 5 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> A =/= 0 )
21 19 20 logcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( log ` A ) e. CC )
22 18 21 mulcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( k x. ( log ` A ) ) e. CC )
23 14 16 22 fprodefsum 
 |-  ( ph -> prod_ k e. ( 1 ... N ) ( exp ` ( k x. ( log ` A ) ) ) = ( exp ` sum_ k e. ( 1 ... N ) ( k x. ( log ` A ) ) ) )
24 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
25 3 5 logcld 
 |-  ( ph -> ( log ` A ) e. CC )
26 24 25 9 fsummulc1 
 |-  ( ph -> ( sum_ k e. ( 1 ... N ) k x. ( log ` A ) ) = sum_ k e. ( 1 ... N ) ( k x. ( log ` A ) ) )
27 26 eqcomd 
 |-  ( ph -> sum_ k e. ( 1 ... N ) ( k x. ( log ` A ) ) = ( sum_ k e. ( 1 ... N ) k x. ( log ` A ) ) )
28 27 fveq2d 
 |-  ( ph -> ( exp ` sum_ k e. ( 1 ... N ) ( k x. ( log ` A ) ) ) = ( exp ` ( sum_ k e. ( 1 ... N ) k x. ( log ` A ) ) ) )
29 24 9 fsumcl 
 |-  ( ph -> sum_ k e. ( 1 ... N ) k e. CC )
30 3 5 29 cxpefd 
 |-  ( ph -> ( A ^c sum_ k e. ( 1 ... N ) k ) = ( exp ` ( sum_ k e. ( 1 ... N ) k x. ( log ` A ) ) ) )
31 30 eqcomd 
 |-  ( ph -> ( exp ` ( sum_ k e. ( 1 ... N ) k x. ( log ` A ) ) ) = ( A ^c sum_ k e. ( 1 ... N ) k ) )
32 28 31 eqtrd 
 |-  ( ph -> ( exp ` sum_ k e. ( 1 ... N ) ( k x. ( log ` A ) ) ) = ( A ^c sum_ k e. ( 1 ... N ) k ) )
33 23 32 eqtrd 
 |-  ( ph -> prod_ k e. ( 1 ... N ) ( exp ` ( k x. ( log ` A ) ) ) = ( A ^c sum_ k e. ( 1 ... N ) k ) )
34 13 33 eqtrd 
 |-  ( ph -> prod_ k e. ( 1 ... N ) ( A ^c k ) = ( A ^c sum_ k e. ( 1 ... N ) k ) )