Metamath Proof Explorer

Theorem pcbc

Description: Calculate the prime count of a binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014) (Revised by Mario Carneiro, 21-May-2014)

Ref Expression
Assertion pcbc 
|- ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( N _C K ) ) = sum_ k e. ( 1 ... N ) ( ( |_ ` ( N / ( P ^ k ) ) ) - ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> P e. Prime )
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 2 3ad2ant1 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> N e. NN0 )
4 3 faccld 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` N ) e. NN )
5 4 nnzd 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` N ) e. ZZ )
6 4 nnne0d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` N ) =/= 0 )
7 fznn0sub 
 |-  ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
8 7 3ad2ant2 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( N - K ) e. NN0 )
9 8 faccld 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` ( N - K ) ) e. NN )
10 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
11 10 3ad2ant2 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> K e. NN0 )
12 11 faccld 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` K ) e. NN )
13 9 12 nnmulcld 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN )
14 pcdiv 
 |-  ( ( P e. Prime /\ ( ( ! ` N ) e. ZZ /\ ( ! ` N ) =/= 0 ) /\ ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN ) -> ( P pCnt ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) = ( ( P pCnt ( ! ` N ) ) - ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) )
15 1 5 6 13 14 syl121anc 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) = ( ( P pCnt ( ! ` N ) ) - ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) )
16 bcval2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
17 16 3ad2ant2 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
18 17 oveq2d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( N _C K ) ) = ( P pCnt ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) )
19 fzfid 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( 1 ... N ) e. Fin )
20 nnre 
 |-  ( N e. NN -> N e. RR )
21 20 3ad2ant1 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> N e. RR )
22 21 adantr 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> N e. RR )
23 simpl3 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> P e. Prime )
24 prmnn 
 |-  ( P e. Prime -> P e. NN )
25 23 24 syl 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> P e. NN )
26 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
27 26 nnnn0d 
 |-  ( k e. ( 1 ... N ) -> k e. NN0 )
28 27 adantl 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> k e. NN0 )
29 25 28 nnexpcld 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( P ^ k ) e. NN )
30 22 29 nndivred 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( N / ( P ^ k ) ) e. RR )
31 30 flcld 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ )
32 31 zcnd 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. CC )
33 11 nn0red 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> K e. RR )
34 21 33 resubcld 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( N - K ) e. RR )
35 34 adantr 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( N - K ) e. RR )
36 35 29 nndivred 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( ( N - K ) / ( P ^ k ) ) e. RR )
37 36 flcld 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) e. ZZ )
38 37 zcnd 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) e. CC )
39 33 adantr 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> K e. RR )
40 39 29 nndivred 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( K / ( P ^ k ) ) e. RR )
41 40 flcld 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( |_ ` ( K / ( P ^ k ) ) ) e. ZZ )
42 41 zcnd 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( |_ ` ( K / ( P ^ k ) ) ) e. CC )
43 38 42 addcld 
 |-  ( ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) /\ k e. ( 1 ... N ) ) -> ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) e. CC )
44 19 32 43 fsumsub 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> sum_ k e. ( 1 ... N ) ( ( |_ ` ( N / ( P ^ k ) ) ) - ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) = ( sum_ k e. ( 1 ... N ) ( |_ ` ( N / ( P ^ k ) ) ) - sum_ k e. ( 1 ... N ) ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) )
45 3 nn0zd 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> N e. ZZ )
46 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
47 45 46 syl 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> N e. ( ZZ>= ` N ) )
48 pcfac 
 |-  ( ( N e. NN0 /\ N e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( P pCnt ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( |_ ` ( N / ( P ^ k ) ) ) )
49 3 47 1 48 syl3anc 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( |_ ` ( N / ( P ^ k ) ) ) )
50 11 nn0ge0d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> 0 <_ K )
51 21 33 subge02d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( 0 <_ K <-> ( N - K ) <_ N ) )
52 50 51 mpbid 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( N - K ) <_ N )
53 11 nn0zd 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> K e. ZZ )
54 45 53 zsubcld 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( N - K ) e. ZZ )
55 eluz 
 |-  ( ( ( N - K ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( N - K ) ) <-> ( N - K ) <_ N ) )
56 54 45 55 syl2anc 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( N e. ( ZZ>= ` ( N - K ) ) <-> ( N - K ) <_ N ) )
57 52 56 mpbird 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> N e. ( ZZ>= ` ( N - K ) ) )
58 pcfac 
 |-  ( ( ( N - K ) e. NN0 /\ N e. ( ZZ>= ` ( N - K ) ) /\ P e. Prime ) -> ( P pCnt ( ! ` ( N - K ) ) ) = sum_ k e. ( 1 ... N ) ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) )
59 8 57 1 58 syl3anc 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( ! ` ( N - K ) ) ) = sum_ k e. ( 1 ... N ) ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) )
60 elfzuz3 
 |-  ( K e. ( 0 ... N ) -> N e. ( ZZ>= ` K ) )
61 60 3ad2ant2 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> N e. ( ZZ>= ` K ) )
62 pcfac 
 |-  ( ( K e. NN0 /\ N e. ( ZZ>= ` K ) /\ P e. Prime ) -> ( P pCnt ( ! ` K ) ) = sum_ k e. ( 1 ... N ) ( |_ ` ( K / ( P ^ k ) ) ) )
63 11 61 1 62 syl3anc 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( ! ` K ) ) = sum_ k e. ( 1 ... N ) ( |_ ` ( K / ( P ^ k ) ) ) )
64 59 63 oveq12d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ( P pCnt ( ! ` ( N - K ) ) ) + ( P pCnt ( ! ` K ) ) ) = ( sum_ k e. ( 1 ... N ) ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + sum_ k e. ( 1 ... N ) ( |_ ` ( K / ( P ^ k ) ) ) ) )
65 9 nnzd 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` ( N - K ) ) e. ZZ )
66 9 nnne0d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` ( N - K ) ) =/= 0 )
67 12 nnzd 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` K ) e. ZZ )
68 12 nnne0d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ! ` K ) =/= 0 )
69 pcmul 
 |-  ( ( P e. Prime /\ ( ( ! ` ( N - K ) ) e. ZZ /\ ( ! ` ( N - K ) ) =/= 0 ) /\ ( ( ! ` K ) e. ZZ /\ ( ! ` K ) =/= 0 ) ) -> ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( P pCnt ( ! ` ( N - K ) ) ) + ( P pCnt ( ! ` K ) ) ) )
70 1 65 66 67 68 69 syl122anc 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( P pCnt ( ! ` ( N - K ) ) ) + ( P pCnt ( ! ` K ) ) ) )
71 19 38 42 fsumadd 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> sum_ k e. ( 1 ... N ) ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) = ( sum_ k e. ( 1 ... N ) ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + sum_ k e. ( 1 ... N ) ( |_ ` ( K / ( P ^ k ) ) ) ) )
72 64 70 71 3eqtr4d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = sum_ k e. ( 1 ... N ) ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) )
73 49 72 oveq12d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( ( P pCnt ( ! ` N ) ) - ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) = ( sum_ k e. ( 1 ... N ) ( |_ ` ( N / ( P ^ k ) ) ) - sum_ k e. ( 1 ... N ) ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) )
74 44 73 eqtr4d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> sum_ k e. ( 1 ... N ) ( ( |_ ` ( N / ( P ^ k ) ) ) - ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) = ( ( P pCnt ( ! ` N ) ) - ( P pCnt ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) )
75 15 18 74 3eqtr4d 
 |-  ( ( N e. NN /\ K e. ( 0 ... N ) /\ P e. Prime ) -> ( P pCnt ( N _C K ) ) = sum_ k e. ( 1 ... N ) ( ( |_ ` ( N / ( P ^ k ) ) ) - ( ( |_ ` ( ( N - K ) / ( P ^ k ) ) ) + ( |_ ` ( K / ( P ^ k ) ) ) ) ) )