Metamath Proof Explorer

Theorem pcbcctr

Description: Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Assertion pcbcctr 
|- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
3 1 2 mpan 
 |-  ( N e. NN -> ( 2 x. N ) e. NN )
4 3 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. NN )
5 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 fzctr 
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
7 5 6 syl 
 |-  ( N e. NN -> N e. ( 0 ... ( 2 x. N ) ) )
8 7 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> N e. ( 0 ... ( 2 x. N ) ) )
9 simpr 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. Prime )
10 pcbc 
 |-  ( ( ( 2 x. N ) e. NN /\ N e. ( 0 ... ( 2 x. N ) ) /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
11 4 8 9 10 syl3anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
12 nncn 
 |-  ( N e. NN -> N e. CC )
13 12 2timesd 
 |-  ( N e. NN -> ( 2 x. N ) = ( N + N ) )
14 12 12 13 mvrladdd 
 |-  ( N e. NN -> ( ( 2 x. N ) - N ) = N )
15 14 fvoveq1d 
 |-  ( N e. NN -> ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) = ( |_ ` ( N / ( P ^ k ) ) ) )
16 15 oveq1d 
 |-  ( N e. NN -> ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) = ( ( |_ ` ( N / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) )
17 16 ad2antrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) = ( ( |_ ` ( N / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) )
18 nnre 
 |-  ( N e. NN -> N e. RR )
19 18 ad2antrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. RR )
20 prmnn 
 |-  ( P e. Prime -> P e. NN )
21 20 adantl 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. NN )
22 elfznn 
 |-  ( k e. ( 1 ... ( 2 x. N ) ) -> k e. NN )
23 22 nnnn0d 
 |-  ( k e. ( 1 ... ( 2 x. N ) ) -> k e. NN0 )
24 nnexpcl 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P ^ k ) e. NN )
25 21 23 24 syl2an 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. NN )
26 19 25 nndivred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. RR )
27 26 flcld 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ )
28 27 zcnd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. CC )
29 28 2timesd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( ( |_ ` ( N / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) )
30 17 29 eqtr4d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) )
31 30 oveq2d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
32 31 sumeq2dv 
 |-  ( ( N e. NN /\ P e. Prime ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( ( |_ ` ( ( ( 2 x. N ) - N ) / ( P ^ k ) ) ) + ( |_ ` ( N / ( P ^ k ) ) ) ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
33 11 32 eqtrd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )