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 )