Metamath Proof Explorer


Theorem pcbcctr

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

Ref Expression
Assertion pcbcctr ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ๐‘ƒ pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( 2 ยท ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2nn โŠข 2 โˆˆ โ„•
2 nnmulcl โŠข ( ( 2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
3 1 2 mpan โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
4 3 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( 2 ยท ๐‘ ) โˆˆ โ„• )
5 nnnn0 โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„•0 )
6 fzctr โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) )
7 5 6 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) )
8 7 adantr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) )
9 simpr โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ๐‘ƒ โˆˆ โ„™ )
10 pcbc โŠข ( ( ( 2 ยท ๐‘ ) โˆˆ โ„• โˆง ๐‘ โˆˆ ( 0 ... ( 2 ยท ๐‘ ) ) โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ๐‘ƒ pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) )
11 4 8 9 10 syl3anc โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ๐‘ƒ pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) )
12 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
13 12 2timesd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ๐‘ ) = ( ๐‘ + ๐‘ ) )
14 12 12 13 mvrladdd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) = ๐‘ )
15 14 fvoveq1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) = ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) )
16 15 oveq1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) = ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) )
17 16 ad2antrr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) = ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) )
18 nnre โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ )
19 18 ad2antrr โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ๐‘ โˆˆ โ„ )
20 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
21 20 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ๐‘ƒ โˆˆ โ„• )
22 elfznn โŠข ( ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) โ†’ ๐‘˜ โˆˆ โ„• )
23 22 nnnn0d โŠข ( ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
24 nnexpcl โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ โ†‘ ๐‘˜ ) โˆˆ โ„• )
25 21 23 24 syl2an โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( ๐‘ƒ โ†‘ ๐‘˜ ) โˆˆ โ„• )
26 19 25 nndivred โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) โˆˆ โ„ )
27 26 flcld โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ค )
28 27 zcnd โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆˆ โ„‚ )
29 28 2timesd โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( 2 ยท ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) = ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) )
30 17 29 eqtr4d โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) = ( 2 ยท ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) )
31 30 oveq2d โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โˆง ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ) โ†’ ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) = ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( 2 ยท ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) )
32 31 sumeq2dv โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ฮฃ ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( ( โŒŠ โ€˜ ( ( ( 2 ยท ๐‘ ) โˆ’ ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) + ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( 2 ยท ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) )
33 11 32 eqtrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„™ ) โ†’ ( ๐‘ƒ pCnt ( ( 2 ยท ๐‘ ) C ๐‘ ) ) = ฮฃ ๐‘˜ โˆˆ ( 1 ... ( 2 ยท ๐‘ ) ) ( ( โŒŠ โ€˜ ( ( 2 ยท ๐‘ ) / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) โˆ’ ( 2 ยท ( โŒŠ โ€˜ ( ๐‘ / ( ๐‘ƒ โ†‘ ๐‘˜ ) ) ) ) ) )