Metamath Proof Explorer

Theorem bposlem1

Description: An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014)

Ref Expression
Assertion bposlem1 
|- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 1 ... ( 2 x. N ) ) e. Fin )
2 2nn 
 |-  2 e. NN
3 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
4 2 3 mpan 
 |-  ( N e. NN -> ( 2 x. N ) e. NN )
5 4 ad2antrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. NN )
6 prmnn 
 |-  ( P e. Prime -> P e. NN )
7 6 ad2antlr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> P e. NN )
8 elfznn 
 |-  ( k e. ( 1 ... ( 2 x. N ) ) -> k e. NN )
9 8 adantl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. NN )
10 9 nnnn0d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. NN0 )
11 7 10 nnexpcld 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. NN )
12 nnrp 
 |-  ( ( 2 x. N ) e. NN -> ( 2 x. N ) e. RR+ )
13 nnrp 
 |-  ( ( P ^ k ) e. NN -> ( P ^ k ) e. RR+ )
14 rpdivcl 
 |-  ( ( ( 2 x. N ) e. RR+ /\ ( P ^ k ) e. RR+ ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
15 12 13 14 syl2an 
 |-  ( ( ( 2 x. N ) e. NN /\ ( P ^ k ) e. NN ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
16 5 11 15 syl2anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
17 16 rpred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR )
18 17 flcld 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) e. ZZ )
19 2z 
 |-  2 e. ZZ
20 simpll 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. NN )
21 nnrp 
 |-  ( N e. NN -> N e. RR+ )
22 rpdivcl 
 |-  ( ( N e. RR+ /\ ( P ^ k ) e. RR+ ) -> ( N / ( P ^ k ) ) e. RR+ )
23 21 13 22 syl2an 
 |-  ( ( N e. NN /\ ( P ^ k ) e. NN ) -> ( N / ( P ^ k ) ) e. RR+ )
24 20 11 23 syl2anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. RR+ )
25 24 rpred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. RR )
26 25 flcld 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ )
27 zmulcl 
 |-  ( ( 2 e. ZZ /\ ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. ZZ )
28 19 26 27 sylancr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. ZZ )
29 18 28 zsubcld 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. ZZ )
30 29 zred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. RR )
31 1re 
 |-  1 e. RR
32 0re 
 |-  0 e. RR
33 31 32 ifcli 
 |-  if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) e. RR
34 33 a1i 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) e. RR )
35 28 zred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. RR )
36 17 35 resubcld 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. RR )
37 2re 
 |-  2 e. RR
38 37 a1i 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 2 e. RR )
39 18 zred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) e. RR )
40 flle 
 |-  ( ( ( 2 x. N ) / ( P ^ k ) ) e. RR -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) <_ ( ( 2 x. N ) / ( P ^ k ) ) )
41 17 40 syl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) <_ ( ( 2 x. N ) / ( P ^ k ) ) )
42 39 17 35 41 lesub1dd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
43 resubcl 
 |-  ( ( ( N / ( P ^ k ) ) e. RR /\ 1 e. RR ) -> ( ( N / ( P ^ k ) ) - 1 ) e. RR )
44 25 31 43 sylancl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) - 1 ) e. RR )
45 remulcl 
 |-  ( ( 2 e. RR /\ ( ( N / ( P ^ k ) ) - 1 ) e. RR ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) e. RR )
46 37 44 45 sylancr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) e. RR )
47 flltp1 
 |-  ( ( N / ( P ^ k ) ) e. RR -> ( N / ( P ^ k ) ) < ( ( |_ ` ( N / ( P ^ k ) ) ) + 1 ) )
48 25 47 syl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) < ( ( |_ ` ( N / ( P ^ k ) ) ) + 1 ) )
49 1red 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. RR )
50 26 zred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. RR )
51 25 49 50 ltsubaddd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( N / ( P ^ k ) ) < ( ( |_ ` ( N / ( P ^ k ) ) ) + 1 ) ) )
52 48 51 mpbird 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) )
53 2pos 
 |-  0 < 2
54 37 53 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
55 ltmul2 
 |-  ( ( ( ( N / ( P ^ k ) ) - 1 ) e. RR /\ ( |_ ` ( N / ( P ^ k ) ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
56 54 55 mp3an3 
 |-  ( ( ( ( N / ( P ^ k ) ) - 1 ) e. RR /\ ( |_ ` ( N / ( P ^ k ) ) ) e. RR ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
57 44 50 56 syl2anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
58 52 57 mpbid 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) )
59 46 35 17 58 ltsub2dd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) ) )
60 2cnd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 2 e. CC )
61 nncn 
 |-  ( N e. NN -> N e. CC )
62 61 ad2antrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. CC )
63 11 nncnd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. CC )
64 11 nnne0d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) =/= 0 )
65 60 62 63 64 divassd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) = ( 2 x. ( N / ( P ^ k ) ) ) )
66 25 recnd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. CC )
67 60 66 muls1d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) = ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) )
68 65 67 oveq12d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) ) = ( ( 2 x. ( N / ( P ^ k ) ) ) - ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) ) )
69 remulcl 
 |-  ( ( 2 e. RR /\ ( N / ( P ^ k ) ) e. RR ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. RR )
70 37 25 69 sylancr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. RR )
71 70 recnd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. CC )
72 2cn 
 |-  2 e. CC
73 nncan 
 |-  ( ( ( 2 x. ( N / ( P ^ k ) ) ) e. CC /\ 2 e. CC ) -> ( ( 2 x. ( N / ( P ^ k ) ) ) - ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) ) = 2 )
74 71 72 73 sylancl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. ( N / ( P ^ k ) ) ) - ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) ) = 2 )
75 68 74 eqtrd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) ) = 2 )
76 59 75 breqtrd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < 2 )
77 30 36 38 42 76 lelttrd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < 2 )
78 df-2 
 |-  2 = ( 1 + 1 )
79 77 78 breqtrdi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( 1 + 1 ) )
80 1z 
 |-  1 e. ZZ
81 zleltp1 
 |-  ( ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( 1 + 1 ) ) )
82 29 80 81 sylancl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( 1 + 1 ) ) )
83 79 82 mpbird 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 )
84 iftrue 
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = 1 )
85 84 breq2d 
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 ) )
86 83 85 syl5ibrcom 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) ) )
87 9 nnge1d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 <_ k )
88 87 biantrurd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <-> ( 1 <_ k /\ k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
89 6 adantl 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. NN )
90 89 nnred 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. RR )
91 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
92 91 adantl 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. ( ZZ>= ` 2 ) )
93 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
94 92 93 syl 
 |-  ( ( N e. NN /\ P e. Prime ) -> 1 < P )
95 90 94 jca 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P e. RR /\ 1 < P ) )
96 95 adantr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P e. RR /\ 1 < P ) )
97 elfzelz 
 |-  ( k e. ( 1 ... ( 2 x. N ) ) -> k e. ZZ )
98 97 adantl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. ZZ )
99 4 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. NN )
100 99 nnrpd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. RR+ )
101 100 adantr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. RR+ )
102 efexple 
 |-  ( ( ( P e. RR /\ 1 < P ) /\ k e. ZZ /\ ( 2 x. N ) e. RR+ ) -> ( ( P ^ k ) <_ ( 2 x. N ) <-> k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
103 96 98 101 102 syl3anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( P ^ k ) <_ ( 2 x. N ) <-> k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
104 9 nnzd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. ZZ )
105 80 a1i 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. ZZ )
106 99 nnred 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. RR )
107 1red 
 |-  ( ( N e. NN /\ P e. Prime ) -> 1 e. RR )
108 37 a1i 
 |-  ( ( N e. NN /\ P e. Prime ) -> 2 e. RR )
109 1lt2 
 |-  1 < 2
110 109 a1i 
 |-  ( ( N e. NN /\ P e. Prime ) -> 1 < 2 )
111 2t1e2 
 |-  ( 2 x. 1 ) = 2
112 nnre 
 |-  ( N e. NN -> N e. RR )
113 112 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> N e. RR )
114 0le2 
 |-  0 <_ 2
115 37 114 pm3.2i 
 |-  ( 2 e. RR /\ 0 <_ 2 )
116 115 a1i 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 e. RR /\ 0 <_ 2 ) )
117 nnge1 
 |-  ( N e. NN -> 1 <_ N )
118 117 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> 1 <_ N )
119 lemul2a 
 |-  ( ( ( 1 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 <_ 2 ) ) /\ 1 <_ N ) -> ( 2 x. 1 ) <_ ( 2 x. N ) )
120 107 113 116 118 119 syl31anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. 1 ) <_ ( 2 x. N ) )
121 111 120 eqbrtrrid 
 |-  ( ( N e. NN /\ P e. Prime ) -> 2 <_ ( 2 x. N ) )
122 107 108 106 110 121 ltletrd 
 |-  ( ( N e. NN /\ P e. Prime ) -> 1 < ( 2 x. N ) )
123 106 122 rplogcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) e. RR+ )
124 90 94 rplogcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( log ` P ) e. RR+ )
125 123 124 rpdivcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR+ )
126 125 rpred 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR )
127 126 flcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ )
128 127 adantr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ )
129 elfz 
 |-  ( ( k e. ZZ /\ 1 e. ZZ /\ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( 1 <_ k /\ k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
130 104 105 128 129 syl3anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( 1 <_ k /\ k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
131 88 103 130 3bitr4rd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( P ^ k ) <_ ( 2 x. N ) ) )
132 131 notbid 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> -. ( P ^ k ) <_ ( 2 x. N ) ) )
133 106 adantr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. RR )
134 11 nnred 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. RR )
135 133 134 ltnled 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) <-> -. ( P ^ k ) <_ ( 2 x. N ) ) )
136 132 135 bitr4d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( 2 x. N ) < ( P ^ k ) ) )
137 16 rpge0d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) )
138 137 adantrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) )
139 11 nngt0d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 < ( P ^ k ) )
140 ltdivmul 
 |-  ( ( ( 2 x. N ) e. RR /\ 1 e. RR /\ ( ( P ^ k ) e. RR /\ 0 < ( P ^ k ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) ) )
141 133 49 134 139 140 syl112anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) ) )
142 63 mulridd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( P ^ k ) x. 1 ) = ( P ^ k ) )
143 142 breq2d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( ( P ^ k ) x. 1 ) <-> ( 2 x. N ) < ( P ^ k ) ) )
144 141 143 bitrd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( P ^ k ) ) )
145 144 biimprd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> ( ( 2 x. N ) / ( P ^ k ) ) < 1 ) )
146 145 impr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < 1 )
147 0p1e1 
 |-  ( 0 + 1 ) = 1
148 146 147 breqtrrdi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) )
149 17 adantrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR )
150 0z 
 |-  0 e. ZZ
151 flbi 
 |-  ( ( ( ( 2 x. N ) / ( P ^ k ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
152 149 150 151 sylancl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
153 138 148 152 mpbir2and 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 )
154 24 rpge0d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 <_ ( N / ( P ^ k ) ) )
155 154 adantrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> 0 <_ ( N / ( P ^ k ) ) )
156 112 21 ltaddrp2d 
 |-  ( N e. NN -> N < ( N + N ) )
157 61 2timesd 
 |-  ( N e. NN -> ( 2 x. N ) = ( N + N ) )
158 156 157 breqtrrd 
 |-  ( N e. NN -> N < ( 2 x. N ) )
159 158 ad2antrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N < ( 2 x. N ) )
160 112 ad2antrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. RR )
161 lttr 
 |-  ( ( N e. RR /\ ( 2 x. N ) e. RR /\ ( P ^ k ) e. RR ) -> ( ( N < ( 2 x. N ) /\ ( 2 x. N ) < ( P ^ k ) ) -> N < ( P ^ k ) ) )
162 160 133 134 161 syl3anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N < ( 2 x. N ) /\ ( 2 x. N ) < ( P ^ k ) ) -> N < ( P ^ k ) ) )
163 159 162 mpand 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> N < ( P ^ k ) ) )
164 ltdivmul 
 |-  ( ( N e. RR /\ 1 e. RR /\ ( ( P ^ k ) e. RR /\ 0 < ( P ^ k ) ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( ( P ^ k ) x. 1 ) ) )
165 160 49 134 139 164 syl112anc 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( ( P ^ k ) x. 1 ) ) )
166 142 breq2d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N < ( ( P ^ k ) x. 1 ) <-> N < ( P ^ k ) ) )
167 165 166 bitrd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( P ^ k ) ) )
168 163 167 sylibrd 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> ( N / ( P ^ k ) ) < 1 ) )
169 168 impr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( N / ( P ^ k ) ) < 1 )
170 169 147 breqtrrdi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( N / ( P ^ k ) ) < ( 0 + 1 ) )
171 25 adantrr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( N / ( P ^ k ) ) e. RR )
172 flbi 
 |-  ( ( ( N / ( P ^ k ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
173 171 150 172 sylancl 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
174 155 170 173 mpbir2and 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) = 0 )
175 174 oveq2d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. 0 ) )
176 2t0e0 
 |-  ( 2 x. 0 ) = 0
177 175 176 eqtrdi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = 0 )
178 153 177 oveq12d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( 0 - 0 ) )
179 0m0e0 
 |-  ( 0 - 0 ) = 0
180 178 179 eqtrdi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
181 0le0 
 |-  0 <_ 0
182 180 181 eqbrtrdi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 )
183 182 expr 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 ) )
184 136 183 sylbid 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 ) )
185 iffalse 
 |-  ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = 0 )
186 185 eqcomd 
 |-  ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> 0 = if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
187 186 breq2d 
 |-  ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) ) )
188 184 187 mpbidi 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) ) )
189 86 188 pm2.61d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
190 1 30 34 189 fsumle 
 |-  ( ( N e. NN /\ P e. Prime ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
191 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 ) ) ) ) ) )
192 127 zred 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. RR )
193 flle 
 |-  ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
194 126 193 syl 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
195 99 nnnn0d 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. NN0 )
196 89 195 nnexpcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) e. NN )
197 196 nnred 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) e. RR )
198 bernneq3 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( 2 x. N ) e. NN0 ) -> ( 2 x. N ) < ( P ^ ( 2 x. N ) ) )
199 92 195 198 syl2anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) < ( P ^ ( 2 x. N ) ) )
200 106 197 199 ltled 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) <_ ( P ^ ( 2 x. N ) ) )
201 100 reeflogd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( log ` ( 2 x. N ) ) ) = ( 2 x. N ) )
202 89 nnrpd 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. RR+ )
203 99 nnzd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ZZ )
204 reexplog 
 |-  ( ( P e. RR+ /\ ( 2 x. N ) e. ZZ ) -> ( P ^ ( 2 x. N ) ) = ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
205 202 203 204 syl2anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) = ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
206 205 eqcomd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) = ( P ^ ( 2 x. N ) ) )
207 200 201 206 3brtr4d 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
208 100 relogcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) e. RR )
209 124 rpred 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( log ` P ) e. RR )
210 106 209 remulcld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) x. ( log ` P ) ) e. RR )
211 efle 
 |-  ( ( ( log ` ( 2 x. N ) ) e. RR /\ ( ( 2 x. N ) x. ( log ` P ) ) e. RR ) -> ( ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) <-> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) ) )
212 208 210 211 syl2anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) <-> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) ) )
213 207 212 mpbird 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) )
214 208 106 124 ledivmul2d 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) <_ ( 2 x. N ) <-> ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) ) )
215 213 214 mpbird 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) <_ ( 2 x. N ) )
216 192 126 106 194 215 letrd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) )
217 eluz 
 |-  ( ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) ) )
218 127 203 217 syl2anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) ) )
219 216 218 mpbird 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
220 fzss2 
 |-  ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) C_ ( 1 ... ( 2 x. N ) ) )
221 219 220 syl 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) C_ ( 1 ... ( 2 x. N ) ) )
222 sumhash 
 |-  ( ( ( 1 ... ( 2 x. N ) ) e. Fin /\ ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) C_ ( 1 ... ( 2 x. N ) ) ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = ( # ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
223 1 221 222 syl2anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = ( # ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
224 125 rprege0d 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ 0 <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
225 flge0nn0 
 |-  ( ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ 0 <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. NN0 )
226 hashfz1 
 |-  ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) = ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
227 224 225 226 3syl 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( # ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) = ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
228 223 227 eqtr2d 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
229 190 191 228 3brtr4d 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
230 simpr 
 |-  ( ( N e. NN /\ P e. Prime ) -> P e. Prime )
231 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
232 fzctr 
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
233 bccl2 
 |-  ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
234 231 232 233 3syl 
 |-  ( N e. NN -> ( ( 2 x. N ) _C N ) e. NN )
235 234 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) _C N ) e. NN )
236 230 235 pccld 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
237 236 nn0zd 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
238 efexple 
 |-  ( ( ( P e. RR /\ 1 < P ) /\ ( P pCnt ( ( 2 x. N ) _C N ) ) e. ZZ /\ ( 2 x. N ) e. RR+ ) -> ( ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) <-> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
239 90 94 237 100 238 syl211anc 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) <-> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
240 229 239 mpbird 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )