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 ffvelcdmd ⊢ ( 𝜑 → ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 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 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑘 + 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 ffvelcdm ⊢ ( ( 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 mulridd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 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 ) ) )