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 ( 𝜑𝑁 ∈ ℕ )
bposlem2.2 ( 𝜑𝑃 ∈ ℙ )
bposlem2.3 ( 𝜑 → 2 < 𝑃 )
bposlem2.4 ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) < 𝑃 )
bposlem2.5 ( 𝜑𝑃𝑁 )
Assertion bposlem2 ( 𝜑 → ( 𝑃 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )

Proof

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