Metamath Proof Explorer

Theorem bposlem2

Description: There are no odd primes in the range ( 2 N / 3 , N ] dividing the N -th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypotheses bposlem2.1 
|- ( ph -> N e. NN )
bposlem2.2 
|- ( ph -> P e. Prime )
bposlem2.3 
|- ( ph -> 2 < P )
bposlem2.4 
|- ( ph -> ( ( 2 x. N ) / 3 ) < P )
bposlem2.5 
|- ( ph -> P <_ N )
Assertion bposlem2 
|- ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = 0 )

Proof

Step Hyp Ref Expression
1 bposlem2.1 
 |-  ( ph -> N e. NN )
2 bposlem2.2 
 |-  ( ph -> P e. Prime )
3 bposlem2.3 
 |-  ( ph -> 2 < P )
4 bposlem2.4 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) < P )
5 bposlem2.5 
 |-  ( ph -> P <_ N )
6 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 ) ) ) ) ) )
7 1 2 6 syl2anc 
 |-  ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
8 elfznn 
 |-  ( k e. ( 1 ... ( 2 x. N ) ) -> k e. NN )
9 elnn1uz2 
 |-  ( k e. NN <-> ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) )
10 8 9 sylib 
 |-  ( k e. ( 1 ... ( 2 x. N ) ) -> ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) )
11 oveq2 
 |-  ( k = 1 -> ( P ^ k ) = ( P ^ 1 ) )
12 prmnn 
 |-  ( P e. Prime -> P e. NN )
13 2 12 syl 
 |-  ( ph -> P e. NN )
14 13 nncnd 
 |-  ( ph -> P e. CC )
15 14 exp1d 
 |-  ( ph -> ( P ^ 1 ) = P )
16 11 15 sylan9eqr 
 |-  ( ( ph /\ k = 1 ) -> ( P ^ k ) = P )
17 16 oveq2d 
 |-  ( ( ph /\ k = 1 ) -> ( ( 2 x. N ) / ( P ^ k ) ) = ( ( 2 x. N ) / P ) )
18 17 fveq2d 
 |-  ( ( ph /\ k = 1 ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = ( |_ ` ( ( 2 x. N ) / P ) ) )
19 2t1e2 
 |-  ( 2 x. 1 ) = 2
20 14 mulid2d 
 |-  ( ph -> ( 1 x. P ) = P )
21 20 5 eqbrtrd 
 |-  ( ph -> ( 1 x. P ) <_ N )
22 1red 
 |-  ( ph -> 1 e. RR )
23 1 nnred 
 |-  ( ph -> N e. RR )
24 13 nnred 
 |-  ( ph -> P e. RR )
25 13 nngt0d 
 |-  ( ph -> 0 < P )
26 lemuldiv 
 |-  ( ( 1 e. RR /\ N e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( 1 x. P ) <_ N <-> 1 <_ ( N / P ) ) )
27 22 23 24 25 26 syl112anc 
 |-  ( ph -> ( ( 1 x. P ) <_ N <-> 1 <_ ( N / P ) ) )
28 21 27 mpbid 
 |-  ( ph -> 1 <_ ( N / P ) )
29 23 13 nndivred 
 |-  ( ph -> ( N / P ) e. RR )
30 1re 
 |-  1 e. RR
31 2re 
 |-  2 e. RR
32 2pos 
 |-  0 < 2
33 31 32 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
34 lemul2 
 |-  ( ( 1 e. RR /\ ( N / P ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 1 <_ ( N / P ) <-> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) ) )
35 30 33 34 mp3an13 
 |-  ( ( N / P ) e. RR -> ( 1 <_ ( N / P ) <-> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) ) )
36 29 35 syl 
 |-  ( ph -> ( 1 <_ ( N / P ) <-> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) ) )
37 28 36 mpbid 
 |-  ( ph -> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) )
38 19 37 eqbrtrrid 
 |-  ( ph -> 2 <_ ( 2 x. ( N / P ) ) )
39 2cnd 
 |-  ( ph -> 2 e. CC )
40 1 nncnd 
 |-  ( ph -> N e. CC )
41 13 nnne0d 
 |-  ( ph -> P =/= 0 )
42 39 40 14 41 divassd 
 |-  ( ph -> ( ( 2 x. N ) / P ) = ( 2 x. ( N / P ) ) )
43 38 42 breqtrrd 
 |-  ( ph -> 2 <_ ( ( 2 x. N ) / P ) )
44 2nn 
 |-  2 e. NN
45 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
46 44 1 45 sylancr 
 |-  ( ph -> ( 2 x. N ) e. NN )
47 46 nnred 
 |-  ( ph -> ( 2 x. N ) e. RR )
48 3re 
 |-  3 e. RR
49 3pos 
 |-  0 < 3
50 48 49 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
51 ltdiv23 
 |-  ( ( ( 2 x. N ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( ( 2 x. N ) / P ) < 3 ) )
52 50 51 mp3an2 
 |-  ( ( ( 2 x. N ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( ( 2 x. N ) / P ) < 3 ) )
53 47 24 25 52 syl12anc 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) < P <-> ( ( 2 x. N ) / P ) < 3 ) )
54 4 53 mpbid 
 |-  ( ph -> ( ( 2 x. N ) / P ) < 3 )
55 df-3 
 |-  3 = ( 2 + 1 )
56 54 55 breqtrdi 
 |-  ( ph -> ( ( 2 x. N ) / P ) < ( 2 + 1 ) )
57 47 13 nndivred 
 |-  ( ph -> ( ( 2 x. N ) / P ) e. RR )
58 2z 
 |-  2 e. ZZ
59 flbi 
 |-  ( ( ( ( 2 x. N ) / P ) e. RR /\ 2 e. ZZ ) -> ( ( |_ ` ( ( 2 x. N ) / P ) ) = 2 <-> ( 2 <_ ( ( 2 x. N ) / P ) /\ ( ( 2 x. N ) / P ) < ( 2 + 1 ) ) ) )
60 57 58 59 sylancl 
 |-  ( ph -> ( ( |_ ` ( ( 2 x. N ) / P ) ) = 2 <-> ( 2 <_ ( ( 2 x. N ) / P ) /\ ( ( 2 x. N ) / P ) < ( 2 + 1 ) ) ) )
61 43 56 60 mpbir2and 
 |-  ( ph -> ( |_ ` ( ( 2 x. N ) / P ) ) = 2 )
62 61 adantr 
 |-  ( ( ph /\ k = 1 ) -> ( |_ ` ( ( 2 x. N ) / P ) ) = 2 )
63 18 62 eqtrd 
 |-  ( ( ph /\ k = 1 ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 2 )
64 16 oveq2d 
 |-  ( ( ph /\ k = 1 ) -> ( N / ( P ^ k ) ) = ( N / P ) )
65 64 fveq2d 
 |-  ( ( ph /\ k = 1 ) -> ( |_ ` ( N / ( P ^ k ) ) ) = ( |_ ` ( N / P ) ) )
66 remulcl 
 |-  ( ( 2 e. RR /\ ( N / P ) e. RR ) -> ( 2 x. ( N / P ) ) e. RR )
67 31 29 66 sylancr 
 |-  ( ph -> ( 2 x. ( N / P ) ) e. RR )
68 48 a1i 
 |-  ( ph -> 3 e. RR )
69 4re 
 |-  4 e. RR
70 69 a1i 
 |-  ( ph -> 4 e. RR )
71 42 54 eqbrtrrd 
 |-  ( ph -> ( 2 x. ( N / P ) ) < 3 )
72 3lt4 
 |-  3 < 4
73 72 a1i 
 |-  ( ph -> 3 < 4 )
74 67 68 70 71 73 lttrd 
 |-  ( ph -> ( 2 x. ( N / P ) ) < 4 )
75 2t2e4 
 |-  ( 2 x. 2 ) = 4
76 74 75 breqtrrdi 
 |-  ( ph -> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) )
77 ltmul2 
 |-  ( ( ( N / P ) e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( N / P ) < 2 <-> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) ) )
78 31 33 77 mp3an23 
 |-  ( ( N / P ) e. RR -> ( ( N / P ) < 2 <-> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) ) )
79 29 78 syl 
 |-  ( ph -> ( ( N / P ) < 2 <-> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) ) )
80 76 79 mpbird 
 |-  ( ph -> ( N / P ) < 2 )
81 df-2 
 |-  2 = ( 1 + 1 )
82 80 81 breqtrdi 
 |-  ( ph -> ( N / P ) < ( 1 + 1 ) )
83 1z 
 |-  1 e. ZZ
84 flbi 
 |-  ( ( ( N / P ) e. RR /\ 1 e. ZZ ) -> ( ( |_ ` ( N / P ) ) = 1 <-> ( 1 <_ ( N / P ) /\ ( N / P ) < ( 1 + 1 ) ) ) )
85 29 83 84 sylancl 
 |-  ( ph -> ( ( |_ ` ( N / P ) ) = 1 <-> ( 1 <_ ( N / P ) /\ ( N / P ) < ( 1 + 1 ) ) ) )
86 28 82 85 mpbir2and 
 |-  ( ph -> ( |_ ` ( N / P ) ) = 1 )
87 86 adantr 
 |-  ( ( ph /\ k = 1 ) -> ( |_ ` ( N / P ) ) = 1 )
88 65 87 eqtrd 
 |-  ( ( ph /\ k = 1 ) -> ( |_ ` ( N / ( P ^ k ) ) ) = 1 )
89 88 oveq2d 
 |-  ( ( ph /\ k = 1 ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. 1 ) )
90 89 19 eqtrdi 
 |-  ( ( ph /\ k = 1 ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = 2 )
91 63 90 oveq12d 
 |-  ( ( ph /\ k = 1 ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( 2 - 2 ) )
92 2cn 
 |-  2 e. CC
93 92 subidi 
 |-  ( 2 - 2 ) = 0
94 91 93 eqtrdi 
 |-  ( ( ph /\ k = 1 ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
95 46 nnrpd 
 |-  ( ph -> ( 2 x. N ) e. RR+ )
96 95 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) e. RR+ )
97 eluzge2nn0 
 |-  ( k e. ( ZZ>= ` 2 ) -> k e. NN0 )
98 nnexpcl 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P ^ k ) e. NN )
99 13 97 98 syl2an 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. NN )
100 99 nnrpd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. RR+ )
101 96 100 rpdivcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
102 101 rpge0d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) )
103 47 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) e. RR )
104 remulcl 
 |-  ( ( 3 e. RR /\ P e. RR ) -> ( 3 x. P ) e. RR )
105 48 24 104 sylancr 
 |-  ( ph -> ( 3 x. P ) e. RR )
106 105 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 3 x. P ) e. RR )
107 99 nnred 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. RR )
108 ltdivmul 
 |-  ( ( ( 2 x. N ) e. RR /\ P e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( 2 x. N ) < ( 3 x. P ) ) )
109 50 108 mp3an3 
 |-  ( ( ( 2 x. N ) e. RR /\ P e. RR ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( 2 x. N ) < ( 3 x. P ) ) )
110 47 24 109 syl2anc 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) < P <-> ( 2 x. N ) < ( 3 x. P ) ) )
111 4 110 mpbid 
 |-  ( ph -> ( 2 x. N ) < ( 3 x. P ) )
112 111 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) < ( 3 x. P ) )
113 24 24 remulcld 
 |-  ( ph -> ( P x. P ) e. RR )
114 113 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P x. P ) e. RR )
115 nnltp1le 
 |-  ( ( 2 e. NN /\ P e. NN ) -> ( 2 < P <-> ( 2 + 1 ) <_ P ) )
116 44 13 115 sylancr 
 |-  ( ph -> ( 2 < P <-> ( 2 + 1 ) <_ P ) )
117 3 116 mpbid 
 |-  ( ph -> ( 2 + 1 ) <_ P )
118 55 117 eqbrtrid 
 |-  ( ph -> 3 <_ P )
119 lemul1 
 |-  ( ( 3 e. RR /\ P e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( 3 <_ P <-> ( 3 x. P ) <_ ( P x. P ) ) )
120 48 119 mp3an1 
 |-  ( ( P e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( 3 <_ P <-> ( 3 x. P ) <_ ( P x. P ) ) )
121 24 24 25 120 syl12anc 
 |-  ( ph -> ( 3 <_ P <-> ( 3 x. P ) <_ ( P x. P ) ) )
122 118 121 mpbid 
 |-  ( ph -> ( 3 x. P ) <_ ( P x. P ) )
123 122 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 3 x. P ) <_ ( P x. P ) )
124 14 sqvald 
 |-  ( ph -> ( P ^ 2 ) = ( P x. P ) )
125 124 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ 2 ) = ( P x. P ) )
126 24 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> P e. RR )
127 13 nnge1d 
 |-  ( ph -> 1 <_ P )
128 127 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 <_ P )
129 simpr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. ( ZZ>= ` 2 ) )
130 126 128 129 leexp2ad 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ 2 ) <_ ( P ^ k ) )
131 125 130 eqbrtrrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P x. P ) <_ ( P ^ k ) )
132 106 114 107 123 131 letrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 3 x. P ) <_ ( P ^ k ) )
133 103 106 107 112 132 ltletrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) < ( P ^ k ) )
134 99 nncnd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. CC )
135 134 mulid1d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( P ^ k ) x. 1 ) = ( P ^ k ) )
136 133 135 breqtrrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) )
137 1red 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
138 103 137 100 ltdivmuld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) ) )
139 136 138 mpbird 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < 1 )
140 1e0p1 
 |-  1 = ( 0 + 1 )
141 139 140 breqtrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) )
142 101 rpred 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR )
143 0z 
 |-  0 e. ZZ
144 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 ) ) ) )
145 142 143 144 sylancl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
146 102 141 145 mpbir2and 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 )
147 1 nnrpd 
 |-  ( ph -> N e. RR+ )
148 147 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N e. RR+ )
149 148 100 rpdivcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) e. RR+ )
150 149 rpge0d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 0 <_ ( N / ( P ^ k ) ) )
151 23 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N e. RR )
152 23 147 ltaddrpd 
 |-  ( ph -> N < ( N + N ) )
153 40 2timesd 
 |-  ( ph -> ( 2 x. N ) = ( N + N ) )
154 152 153 breqtrrd 
 |-  ( ph -> N < ( 2 x. N ) )
155 154 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N < ( 2 x. N ) )
156 151 103 107 155 133 lttrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N < ( P ^ k ) )
157 156 135 breqtrrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N < ( ( P ^ k ) x. 1 ) )
158 151 137 100 ltdivmuld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( ( P ^ k ) x. 1 ) ) )
159 157 158 mpbird 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) < 1 )
160 159 140 breqtrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) < ( 0 + 1 ) )
161 149 rpred 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) e. RR )
162 flbi 
 |-  ( ( ( N / ( P ^ k ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
163 161 143 162 sylancl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
164 150 160 163 mpbir2and 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) = 0 )
165 164 oveq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. 0 ) )
166 2t0e0 
 |-  ( 2 x. 0 ) = 0
167 165 166 eqtrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = 0 )
168 146 167 oveq12d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( 0 - 0 ) )
169 0m0e0 
 |-  ( 0 - 0 ) = 0
170 168 169 eqtrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
171 94 170 jaodan 
 |-  ( ( ph /\ ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
172 10 171 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
173 172 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) 0 )
174 fzfid 
 |-  ( ph -> ( 1 ... ( 2 x. N ) ) e. Fin )
175 sumz 
 |-  ( ( ( 1 ... ( 2 x. N ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( 2 x. N ) ) e. Fin ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) 0 = 0 )
176 175 olcs 
 |-  ( ( 1 ... ( 2 x. N ) ) e. Fin -> sum_ k e. ( 1 ... ( 2 x. N ) ) 0 = 0 )
177 174 176 syl 
 |-  ( ph -> sum_ k e. ( 1 ... ( 2 x. N ) ) 0 = 0 )
178 173 177 eqtrd 
 |-  ( ph -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
179 7 178 eqtrd 
 |-  ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = 0 )