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 
|- ( ph -> N e. ( ZZ>= ` 5 ) )
bpos.2 
|- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
bpos.3 
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
bpos.4 
|- K = ( |_ ` ( ( 2 x. N ) / 3 ) )
bpos.5 
|- M = ( |_ ` ( sqrt ` ( 2 x. N ) ) )
Assertion bposlem5 
|- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) )

Proof

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