Metamath Proof Explorer


Theorem bposlem5

Description: Lemma for bpos . Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypotheses bpos.1 ( 𝜑𝑁 ∈ ( ℤ ‘ 5 ) )
bpos.2 ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )
bpos.3 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
bpos.4 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
bpos.5 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
Assertion bposlem5 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )

Proof

Step Hyp Ref Expression
1 bpos.1 ( 𝜑𝑁 ∈ ( ℤ ‘ 5 ) )
2 bpos.2 ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )
3 bpos.3 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
4 bpos.4 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
5 bpos.5 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
6 id ( 𝑛 ∈ ℙ → 𝑛 ∈ ℙ )
7 5nn 5 ∈ ℕ
8 eluznn ( ( 5 ∈ ℕ ∧ 𝑁 ∈ ( ℤ ‘ 5 ) ) → 𝑁 ∈ ℕ )
9 7 1 8 sylancr ( 𝜑𝑁 ∈ ℕ )
10 9 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
11 fzctr ( 𝑁 ∈ ℕ0𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
12 bccl2 ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
13 10 11 12 3syl ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
14 pccl ( ( 𝑛 ∈ ℙ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
15 6 13 14 syl2anr ( ( 𝜑𝑛 ∈ ℙ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
16 15 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
17 3 16 pcmptcl ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )
18 17 simprd ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
19 3nn 3 ∈ ℕ
20 2z 2 ∈ ℤ
21 9 nnzd ( 𝜑𝑁 ∈ ℤ )
22 zmulcl ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ )
23 20 21 22 sylancr ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
24 23 zred ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
25 2nn 2 ∈ ℕ
26 nnmulcl ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
27 25 9 26 sylancr ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
28 27 nnrpd ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
29 28 rpge0d ( 𝜑 → 0 ≤ ( 2 · 𝑁 ) )
30 24 29 resqrtcld ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
31 30 flcld ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ )
32 sqrt9 ( √ ‘ 9 ) = 3
33 9re 9 ∈ ℝ
34 33 a1i ( 𝜑 → 9 ∈ ℝ )
35 10re 1 0 ∈ ℝ
36 35 a1i ( 𝜑 1 0 ∈ ℝ )
37 lep1 ( 9 ∈ ℝ → 9 ≤ ( 9 + 1 ) )
38 33 37 ax-mp 9 ≤ ( 9 + 1 )
39 9p1e10 ( 9 + 1 ) = 1 0
40 38 39 breqtri 9 ≤ 1 0
41 40 a1i ( 𝜑 → 9 ≤ 1 0 )
42 5cn 5 ∈ ℂ
43 2cn 2 ∈ ℂ
44 5t2e10 ( 5 · 2 ) = 1 0
45 42 43 44 mulcomli ( 2 · 5 ) = 1 0
46 eluzle ( 𝑁 ∈ ( ℤ ‘ 5 ) → 5 ≤ 𝑁 )
47 1 46 syl ( 𝜑 → 5 ≤ 𝑁 )
48 9 nnred ( 𝜑𝑁 ∈ ℝ )
49 5re 5 ∈ ℝ
50 2re 2 ∈ ℝ
51 2pos 0 < 2
52 50 51 pm3.2i ( 2 ∈ ℝ ∧ 0 < 2 )
53 lemul2 ( ( 5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
54 49 52 53 mp3an13 ( 𝑁 ∈ ℝ → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
55 48 54 syl ( 𝜑 → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) )
56 47 55 mpbid ( 𝜑 → ( 2 · 5 ) ≤ ( 2 · 𝑁 ) )
57 45 56 eqbrtrrid ( 𝜑 1 0 ≤ ( 2 · 𝑁 ) )
58 34 36 24 41 57 letrd ( 𝜑 → 9 ≤ ( 2 · 𝑁 ) )
59 0re 0 ∈ ℝ
60 9pos 0 < 9
61 59 33 60 ltleii 0 ≤ 9
62 33 61 pm3.2i ( 9 ∈ ℝ ∧ 0 ≤ 9 )
63 24 29 jca ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) )
64 sqrtle ( ( ( 9 ∈ ℝ ∧ 0 ≤ 9 ) ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) ) → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) )
65 62 63 64 sylancr ( 𝜑 → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) )
66 58 65 mpbid ( 𝜑 → ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
67 32 66 eqbrtrrid ( 𝜑 → 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
68 3z 3 ∈ ℤ
69 flge ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℤ ) → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
70 30 68 69 sylancl ( 𝜑 → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
71 67 70 mpbid ( 𝜑 → 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) )
72 68 eluz1i ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ ‘ 3 ) ↔ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) )
73 31 71 72 sylanbrc ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ ‘ 3 ) )
74 5 73 eqeltrid ( 𝜑𝑀 ∈ ( ℤ ‘ 3 ) )
75 eluznn ( ( 3 ∈ ℕ ∧ 𝑀 ∈ ( ℤ ‘ 3 ) ) → 𝑀 ∈ ℕ )
76 19 74 75 sylancr ( 𝜑𝑀 ∈ ℕ )
77 18 76 ffvelrnd ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ )
78 77 nnred ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
79 76 nnred ( 𝜑𝑀 ∈ ℝ )
80 ppicl ( 𝑀 ∈ ℝ → ( π𝑀 ) ∈ ℕ0 )
81 79 80 syl ( 𝜑 → ( π𝑀 ) ∈ ℕ0 )
82 27 81 nnexpcld ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) ∈ ℕ )
83 82 nnred ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) ∈ ℝ )
84 nndivre ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
85 30 19 84 sylancl ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
86 readdcl ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
87 85 50 86 sylancl ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
88 24 29 87 recxpcld ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ∈ ℝ )
89 fveq2 ( 𝑥 = 1 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 1 ) )
90 fveq2 ( 𝑥 = 1 → ( π𝑥 ) = ( π ‘ 1 ) )
91 ppi1 ( π ‘ 1 ) = 0
92 90 91 eqtrdi ( 𝑥 = 1 → ( π𝑥 ) = 0 )
93 92 oveq2d ( 𝑥 = 1 → ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ 0 ) )
94 89 93 breq12d ( 𝑥 = 1 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) )
95 94 imbi2d ( 𝑥 = 1 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) ) )
96 fveq2 ( 𝑥 = 𝑘 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
97 fveq2 ( 𝑥 = 𝑘 → ( π𝑥 ) = ( π𝑘 ) )
98 97 oveq2d ( 𝑥 = 𝑘 → ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) )
99 96 98 breq12d ( 𝑥 = 𝑘 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ) )
100 99 imbi2d ( 𝑥 = 𝑘 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ) ) )
101 fveq2 ( 𝑥 = ( 𝑘 + 1 ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) )
102 fveq2 ( 𝑥 = ( 𝑘 + 1 ) → ( π𝑥 ) = ( π ‘ ( 𝑘 + 1 ) ) )
103 102 oveq2d ( 𝑥 = ( 𝑘 + 1 ) → ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) )
104 101 103 breq12d ( 𝑥 = ( 𝑘 + 1 ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
105 104 imbi2d ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) )
106 fveq2 ( 𝑥 = 𝑀 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) )
107 fveq2 ( 𝑥 = 𝑀 → ( π𝑥 ) = ( π𝑀 ) )
108 107 oveq2d ( 𝑥 = 𝑀 → ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) )
109 106 108 breq12d ( 𝑥 = 𝑀 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) ) )
110 109 imbi2d ( 𝑥 = 𝑀 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) ) ) )
111 1z 1 ∈ ℤ
112 seq1 ( 1 ∈ ℤ → ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) )
113 111 112 ax-mp ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 )
114 1nn 1 ∈ ℕ
115 1nprm ¬ 1 ∈ ℙ
116 eleq1 ( 𝑛 = 1 → ( 𝑛 ∈ ℙ ↔ 1 ∈ ℙ ) )
117 115 116 mtbiri ( 𝑛 = 1 → ¬ 𝑛 ∈ ℙ )
118 117 iffalsed ( 𝑛 = 1 → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = 1 )
119 1ex 1 ∈ V
120 118 3 119 fvmpt ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) = 1 )
121 114 120 ax-mp ( 𝐹 ‘ 1 ) = 1
122 113 121 eqtri ( seq 1 ( · , 𝐹 ) ‘ 1 ) = 1
123 1le1 1 ≤ 1
124 122 123 eqbrtri ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ 1
125 23 zcnd ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
126 125 exp0d ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 0 ) = 1 )
127 124 126 breqtrrid ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) )
128 18 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ )
129 128 nnred ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
130 129 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
131 27 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℕ )
132 nnre ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
133 132 ad2antlr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → 𝑘 ∈ ℝ )
134 ppicl ( 𝑘 ∈ ℝ → ( π𝑘 ) ∈ ℕ0 )
135 133 134 syl ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π𝑘 ) ∈ ℕ0 )
136 131 135 nnexpcld ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ∈ ℕ )
137 136 nnred ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ∈ ℝ )
138 nnre ( ( 2 · 𝑁 ) ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
139 nngt0 ( ( 2 · 𝑁 ) ∈ ℕ → 0 < ( 2 · 𝑁 ) )
140 138 139 jca ( ( 2 · 𝑁 ) ∈ ℕ → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) )
141 27 140 syl ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) )
142 141 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) )
143 lemul1 ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) · ( 2 · 𝑁 ) ) ) )
144 130 137 142 143 syl3anc ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) · ( 2 · 𝑁 ) ) ) )
145 nnz ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
146 145 adantl ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
147 ppiprm ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( ( π𝑘 ) + 1 ) )
148 146 147 sylan ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( ( π𝑘 ) + 1 ) )
149 148 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( 2 · 𝑁 ) ↑ ( ( π𝑘 ) + 1 ) ) )
150 125 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℂ )
151 150 135 expp1d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( ( π𝑘 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) · ( 2 · 𝑁 ) ) )
152 149 151 eqtrd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) · ( 2 · 𝑁 ) ) )
153 152 breq2d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) · ( 2 · 𝑁 ) ) ) )
154 144 153 bitr4d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
155 simpr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
156 nnuz ℕ = ( ℤ ‘ 1 )
157 155 156 eleqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ ‘ 1 ) )
158 seqp1 ( 𝑘 ∈ ( ℤ ‘ 1 ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
159 157 158 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
160 159 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
161 peano2nn ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
162 161 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
163 eleq1 ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 ∈ ℙ ↔ ( 𝑘 + 1 ) ∈ ℙ ) )
164 id ( 𝑛 = ( 𝑘 + 1 ) → 𝑛 = ( 𝑘 + 1 ) )
165 oveq1 ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
166 164 165 oveq12d ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
167 163 166 ifbieq1d ( 𝑛 = ( 𝑘 + 1 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
168 ovex ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ V
169 168 119 ifex if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ∈ V
170 167 3 169 fvmpt ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
171 162 170 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
172 iftrue ( ( 𝑘 + 1 ) ∈ ℙ → if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
173 171 172 sylan9eq ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
174 9 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑁 ∈ ℕ )
175 bposlem1 ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
176 174 175 sylan ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
177 173 176 eqbrtrd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) )
178 17 simpld ( 𝜑𝐹 : ℕ ⟶ ℕ )
179 ffvelrn ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
180 178 161 179 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
181 180 nnred ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
182 181 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
183 24 ad2antrr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℝ )
184 nnre ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
185 nngt0 ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
186 184 185 jca ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
187 128 186 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
188 187 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) )
189 lemul2 ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) )
190 182 183 188 189 syl3anc ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) )
191 177 190 mpbid ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) )
192 160 191 eqbrtrd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) )
193 ffvelrn ( ( seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
194 18 161 193 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
195 194 nnred ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
196 27 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
197 128 196 nnmulcld ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℕ )
198 197 nnred ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℝ )
199 162 nnred ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℝ )
200 ppicl ( ( 𝑘 + 1 ) ∈ ℝ → ( π ‘ ( 𝑘 + 1 ) ) ∈ ℕ0 )
201 199 200 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( π ‘ ( 𝑘 + 1 ) ) ∈ ℕ0 )
202 196 201 nnexpcld ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℕ )
203 202 nnred ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
204 letr ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
205 195 198 203 204 syl3anc ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
206 205 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
207 192 206 mpand ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
208 154 207 sylbid ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
209 159 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
210 iffalse ( ¬ ( 𝑘 + 1 ) ∈ ℙ → if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = 1 )
211 171 210 sylan9eq ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = 1 )
212 211 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · 1 ) )
213 128 adantr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ )
214 213 nncnd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
215 214 mulid1d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · 1 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
216 209 212 215 3eqtrd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) )
217 ppinprm ( ( 𝑘 ∈ ℤ ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( π𝑘 ) )
218 146 217 sylan ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( π𝑘 ) )
219 218 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) )
220 216 219 breq12d ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ) )
221 220 biimprd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
222 208 221 pm2.61dan ( ( 𝜑𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) )
223 222 expcom ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) )
224 223 a2d ( 𝑘 ∈ ℕ → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑘 ) ) ) → ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) )
225 95 100 105 110 127 224 nnind ( 𝑀 ∈ ℕ → ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) ) )
226 76 225 mpcom ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) )
227 cxpexp ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( π𝑀 ) ∈ ℕ0 ) → ( ( 2 · 𝑁 ) ↑𝑐 ( π𝑀 ) ) = ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) )
228 125 81 227 syl2anc ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( π𝑀 ) ) = ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) )
229 81 nn0red ( 𝜑 → ( π𝑀 ) ∈ ℝ )
230 nndivre ( ( 𝑀 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 𝑀 / 3 ) ∈ ℝ )
231 79 19 230 sylancl ( 𝜑 → ( 𝑀 / 3 ) ∈ ℝ )
232 readdcl ( ( ( 𝑀 / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝑀 / 3 ) + 2 ) ∈ ℝ )
233 231 50 232 sylancl ( 𝜑 → ( ( 𝑀 / 3 ) + 2 ) ∈ ℝ )
234 76 nnnn0d ( 𝜑𝑀 ∈ ℕ0 )
235 234 nn0ge0d ( 𝜑 → 0 ≤ 𝑀 )
236 ppiub ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( π𝑀 ) ≤ ( ( 𝑀 / 3 ) + 2 ) )
237 79 235 236 syl2anc ( 𝜑 → ( π𝑀 ) ≤ ( ( 𝑀 / 3 ) + 2 ) )
238 50 a1i ( 𝜑 → 2 ∈ ℝ )
239 flle ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
240 30 239 syl ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
241 5 240 eqbrtrid ( 𝜑𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
242 3re 3 ∈ ℝ
243 3pos 0 < 3
244 242 243 pm3.2i ( 3 ∈ ℝ ∧ 0 < 3 )
245 244 a1i ( 𝜑 → ( 3 ∈ ℝ ∧ 0 < 3 ) )
246 lediv1 ( ( 𝑀 ∈ ℝ ∧ ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) )
247 79 30 245 246 syl3anc ( 𝜑 → ( 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) )
248 241 247 mpbid ( 𝜑 → ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) )
249 231 85 238 248 leadd1dd ( 𝜑 → ( ( 𝑀 / 3 ) + 2 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) )
250 229 233 87 237 249 letrd ( 𝜑 → ( π𝑀 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) )
251 2t1e2 ( 2 · 1 ) = 2
252 9 nnge1d ( 𝜑 → 1 ≤ 𝑁 )
253 1re 1 ∈ ℝ
254 lemul2 ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
255 253 52 254 mp3an13 ( 𝑁 ∈ ℝ → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
256 48 255 syl ( 𝜑 → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
257 252 256 mpbid ( 𝜑 → ( 2 · 1 ) ≤ ( 2 · 𝑁 ) )
258 251 257 eqbrtrrid ( 𝜑 → 2 ≤ ( 2 · 𝑁 ) )
259 20 eluz1i ( ( 2 · 𝑁 ) ∈ ( ℤ ‘ 2 ) ↔ ( ( 2 · 𝑁 ) ∈ ℤ ∧ 2 ≤ ( 2 · 𝑁 ) ) )
260 23 258 259 sylanbrc ( 𝜑 → ( 2 · 𝑁 ) ∈ ( ℤ ‘ 2 ) )
261 eluz2gt1 ( ( 2 · 𝑁 ) ∈ ( ℤ ‘ 2 ) → 1 < ( 2 · 𝑁 ) )
262 260 261 syl ( 𝜑 → 1 < ( 2 · 𝑁 ) )
263 24 262 229 87 cxpled ( 𝜑 → ( ( π𝑀 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ↔ ( ( 2 · 𝑁 ) ↑𝑐 ( π𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ) )
264 250 263 mpbid ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( π𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )
265 228 264 eqbrtrrd ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )
266 78 83 88 226 265 letrd ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )