Metamath Proof Explorer

Theorem sgmppw

Description: The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion sgmppw 
|- ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( A sigma ( P ^ N ) ) = sum_ k e. ( 0 ... N ) ( ( P ^c A ) ^ k ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> A e. CC )
2 simp2 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> P e. Prime )
3 prmnn 
 |-  ( P e. Prime -> P e. NN )
4 2 3 syl 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> P e. NN )
5 simp3 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> N e. NN0 )
6 4 5 nnexpcld 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( P ^ N ) e. NN )
7 sgmval 
 |-  ( ( A e. CC /\ ( P ^ N ) e. NN ) -> ( A sigma ( P ^ N ) ) = sum_ n e. { x e. NN | x || ( P ^ N ) } ( n ^c A ) )
8 1 6 7 syl2anc 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( A sigma ( P ^ N ) ) = sum_ n e. { x e. NN | x || ( P ^ N ) } ( n ^c A ) )
9 oveq1 
 |-  ( n = ( P ^ k ) -> ( n ^c A ) = ( ( P ^ k ) ^c A ) )
10 fzfid 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( 0 ... N ) e. Fin )
11 eqid 
 |-  ( i e. ( 0 ... N ) |-> ( P ^ i ) ) = ( i e. ( 0 ... N ) |-> ( P ^ i ) )
12 11 dvdsppwf1o 
 |-  ( ( P e. Prime /\ N e. NN0 ) -> ( i e. ( 0 ... N ) |-> ( P ^ i ) ) : ( 0 ... N ) -1-1-onto-> { x e. NN | x || ( P ^ N ) } )
13 2 5 12 syl2anc 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( i e. ( 0 ... N ) |-> ( P ^ i ) ) : ( 0 ... N ) -1-1-onto-> { x e. NN | x || ( P ^ N ) } )
14 oveq2 
 |-  ( i = k -> ( P ^ i ) = ( P ^ k ) )
15 ovex 
 |-  ( P ^ k ) e. _V
16 14 11 15 fvmpt 
 |-  ( k e. ( 0 ... N ) -> ( ( i e. ( 0 ... N ) |-> ( P ^ i ) ) ` k ) = ( P ^ k ) )
17 16 adantl 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( i e. ( 0 ... N ) |-> ( P ^ i ) ) ` k ) = ( P ^ k ) )
18 elrabi 
 |-  ( n e. { x e. NN | x || ( P ^ N ) } -> n e. NN )
19 18 nncnd 
 |-  ( n e. { x e. NN | x || ( P ^ N ) } -> n e. CC )
20 cxpcl 
 |-  ( ( n e. CC /\ A e. CC ) -> ( n ^c A ) e. CC )
21 19 1 20 syl2anr 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ n e. { x e. NN | x || ( P ^ N ) } ) -> ( n ^c A ) e. CC )
22 9 10 13 17 21 fsumf1o 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> sum_ n e. { x e. NN | x || ( P ^ N ) } ( n ^c A ) = sum_ k e. ( 0 ... N ) ( ( P ^ k ) ^c A ) )
23 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
24 23 adantl 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
25 24 nn0cnd 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> k e. CC )
26 1 adantr 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> A e. CC )
27 25 26 mulcomd 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( k x. A ) = ( A x. k ) )
28 27 oveq2d 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( P ^c ( k x. A ) ) = ( P ^c ( A x. k ) ) )
29 4 adantr 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> P e. NN )
30 29 nnrpd 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> P e. RR+ )
31 24 nn0red 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> k e. RR )
32 30 31 26 cxpmuld 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( P ^c ( k x. A ) ) = ( ( P ^c k ) ^c A ) )
33 29 nncnd 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> P e. CC )
34 cxpexp 
 |-  ( ( P e. CC /\ k e. NN0 ) -> ( P ^c k ) = ( P ^ k ) )
35 33 24 34 syl2anc 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( P ^c k ) = ( P ^ k ) )
36 35 oveq1d 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( P ^c k ) ^c A ) = ( ( P ^ k ) ^c A ) )
37 32 36 eqtrd 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( P ^c ( k x. A ) ) = ( ( P ^ k ) ^c A ) )
38 33 26 24 cxpmul2d 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( P ^c ( A x. k ) ) = ( ( P ^c A ) ^ k ) )
39 28 37 38 3eqtr3d 
 |-  ( ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( P ^ k ) ^c A ) = ( ( P ^c A ) ^ k ) )
40 39 sumeq2dv 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> sum_ k e. ( 0 ... N ) ( ( P ^ k ) ^c A ) = sum_ k e. ( 0 ... N ) ( ( P ^c A ) ^ k ) )
41 8 22 40 3eqtrd 
 |-  ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( A sigma ( P ^ N ) ) = sum_ k e. ( 0 ... N ) ( ( P ^c A ) ^ k ) )