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 syl6eq ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) = 2 )
91 63 90 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 = 1 ) → ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) = ( 2 − 2 ) )
92 2cn ⊢ 2 ∈ ℂ
93 92 subidi ⊢ ( 2 − 2 ) = 0
94 91 93 syl6eq ⊢ ( ( 𝜑 ∧ 𝑘 = 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 syl6eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) = 0 )
168 146 167 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ⌊ ‘ ( ( 2 · 𝑁 ) / ( 𝑃 ↑ 𝑘 ) ) ) − ( 2 · ( ⌊ ‘ ( 𝑁 / ( 𝑃 ↑ 𝑘 ) ) ) ) ) = ( 0 − 0 ) )
169 0m0e0 ⊢ ( 0 − 0 ) = 0
170 168 169 syl6eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 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 )