Metamath Proof Explorer

Theorem bposlem6

Description: Lemma for bpos . By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Wolf Lammen, 12-Sep-2020)

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 bposlem6 
|- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )

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 4nn 
 |-  4 e. NN
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 nnexpcl 
 |-  ( ( 4 e. NN /\ N e. NN0 ) -> ( 4 ^ N ) e. NN )
12 6 10 11 sylancr 
 |-  ( ph -> ( 4 ^ N ) e. NN )
13 12 nnred 
 |-  ( ph -> ( 4 ^ N ) e. RR )
14 13 9 nndivred 
 |-  ( ph -> ( ( 4 ^ N ) / N ) e. RR )
15 fzctr 
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
16 10 15 syl 
 |-  ( ph -> N e. ( 0 ... ( 2 x. N ) ) )
17 bccl2 
 |-  ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
18 16 17 syl 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. NN )
19 18 nnred 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. RR )
20 2nn 
 |-  2 e. NN
21 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
22 20 9 21 sylancr 
 |-  ( ph -> ( 2 x. N ) e. NN )
23 22 nnrpd 
 |-  ( ph -> ( 2 x. N ) e. RR+ )
24 22 nnred 
 |-  ( ph -> ( 2 x. N ) e. RR )
25 23 rpge0d 
 |-  ( ph -> 0 <_ ( 2 x. N ) )
26 24 25 resqrtcld 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) e. RR )
27 3nn 
 |-  3 e. NN
28 nndivre 
 |-  ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ 3 e. NN ) -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR )
29 26 27 28 sylancl 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR )
30 2re 
 |-  2 e. RR
31 readdcl 
 |-  ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR /\ 2 e. RR ) -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
32 29 30 31 sylancl 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
33 23 32 rpcxpcld 
 |-  ( ph -> ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
34 33 rpred 
 |-  ( ph -> ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR )
35 2rp 
 |-  2 e. RR+
36 nnmulcl 
 |-  ( ( 4 e. NN /\ N e. NN ) -> ( 4 x. N ) e. NN )
37 6 9 36 sylancr 
 |-  ( ph -> ( 4 x. N ) e. NN )
38 37 nnred 
 |-  ( ph -> ( 4 x. N ) e. RR )
39 nndivre 
 |-  ( ( ( 4 x. N ) e. RR /\ 3 e. NN ) -> ( ( 4 x. N ) / 3 ) e. RR )
40 38 27 39 sylancl 
 |-  ( ph -> ( ( 4 x. N ) / 3 ) e. RR )
41 5re 
 |-  5 e. RR
42 resubcl 
 |-  ( ( ( ( 4 x. N ) / 3 ) e. RR /\ 5 e. RR ) -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
43 40 41 42 sylancl 
 |-  ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
44 rpcxpcl 
 |-  ( ( 2 e. RR+ /\ ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR ) -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR+ )
45 35 43 44 sylancr 
 |-  ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR+ )
46 45 rpred 
 |-  ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR )
47 34 46 remulcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) e. RR )
48 df-5 
 |-  5 = ( 4 + 1 )
49 4z 
 |-  4 e. ZZ
50 uzid 
 |-  ( 4 e. ZZ -> 4 e. ( ZZ>= ` 4 ) )
51 peano2uz 
 |-  ( 4 e. ( ZZ>= ` 4 ) -> ( 4 + 1 ) e. ( ZZ>= ` 4 ) )
52 49 50 51 mp2b 
 |-  ( 4 + 1 ) e. ( ZZ>= ` 4 )
53 48 52 eqeltri 
 |-  5 e. ( ZZ>= ` 4 )
54 eqid 
 |-  ( ZZ>= ` 4 ) = ( ZZ>= ` 4 )
55 54 uztrn2 
 |-  ( ( 5 e. ( ZZ>= ` 4 ) /\ N e. ( ZZ>= ` 5 ) ) -> N e. ( ZZ>= ` 4 ) )
56 53 1 55 sylancr 
 |-  ( ph -> N e. ( ZZ>= ` 4 ) )
57 bclbnd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
58 56 57 syl 
 |-  ( ph -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
59 id 
 |-  ( n e. Prime -> n e. Prime )
60 pccl 
 |-  ( ( n e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
61 59 18 60 syl2anr 
 |-  ( ( ph /\ n e. Prime ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
62 61 ralrimiva 
 |-  ( ph -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
63 3 62 pcmptcl 
 |-  ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
64 63 simprd 
 |-  ( ph -> seq 1 ( x. , F ) : NN --> NN )
65 1 2 3 4 5 bposlem4 
 |-  ( ph -> M e. ( 3 ... K ) )
66 elfzuz 
 |-  ( M e. ( 3 ... K ) -> M e. ( ZZ>= ` 3 ) )
67 65 66 syl 
 |-  ( ph -> M e. ( ZZ>= ` 3 ) )
68 eluznn 
 |-  ( ( 3 e. NN /\ M e. ( ZZ>= ` 3 ) ) -> M e. NN )
69 27 67 68 sylancr 
 |-  ( ph -> M e. NN )
70 64 69 ffvelcdmd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
71 70 nnred 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
72 2z 
 |-  2 e. ZZ
73 nndivre 
 |-  ( ( ( 2 x. N ) e. RR /\ 3 e. NN ) -> ( ( 2 x. N ) / 3 ) e. RR )
74 24 27 73 sylancl 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) e. RR )
75 74 flcld 
 |-  ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ZZ )
76 4 75 eqeltrid 
 |-  ( ph -> K e. ZZ )
77 zmulcl 
 |-  ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 x. K ) e. ZZ )
78 72 76 77 sylancr 
 |-  ( ph -> ( 2 x. K ) e. ZZ )
79 7 nnzi 
 |-  5 e. ZZ
80 zsubcl 
 |-  ( ( ( 2 x. K ) e. ZZ /\ 5 e. ZZ ) -> ( ( 2 x. K ) - 5 ) e. ZZ )
81 78 79 80 sylancl 
 |-  ( ph -> ( ( 2 x. K ) - 5 ) e. ZZ )
82 81 zred 
 |-  ( ph -> ( ( 2 x. K ) - 5 ) e. RR )
83 rpcxpcl 
 |-  ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 5 ) e. RR ) -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR+ )
84 35 82 83 sylancr 
 |-  ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR+ )
85 84 rpred 
 |-  ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR )
86 71 85 remulcld 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
87 1 2 3 4 bposlem3 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )
88 elfzuz3 
 |-  ( M e. ( 3 ... K ) -> K e. ( ZZ>= ` M ) )
89 65 88 syl 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
90 3 62 69 89 pcmptdvds 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) )
91 70 nnzd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. ZZ )
92 70 nnne0d 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) =/= 0 )
93 uztrn 
 |-  ( ( K e. ( ZZ>= ` M ) /\ M e. ( ZZ>= ` 3 ) ) -> K e. ( ZZ>= ` 3 ) )
94 89 67 93 syl2anc 
 |-  ( ph -> K e. ( ZZ>= ` 3 ) )
95 eluznn 
 |-  ( ( 3 e. NN /\ K e. ( ZZ>= ` 3 ) ) -> K e. NN )
96 27 94 95 sylancr 
 |-  ( ph -> K e. NN )
97 64 96 ffvelcdmd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) e. NN )
98 97 nnzd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) e. ZZ )
99 dvdsval2 
 |-  ( ( ( seq 1 ( x. , F ) ` M ) e. ZZ /\ ( seq 1 ( x. , F ) ` M ) =/= 0 /\ ( seq 1 ( x. , F ) ` K ) e. ZZ ) -> ( ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) <-> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ ) )
100 91 92 98 99 syl3anc 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) <-> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ ) )
101 90 100 mpbid 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ )
102 101 zred 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. RR )
103 69 nnred 
 |-  ( ph -> M e. RR )
104 76 zred 
 |-  ( ph -> K e. RR )
105 eluzle 
 |-  ( K e. ( ZZ>= ` M ) -> M <_ K )
106 89 105 syl 
 |-  ( ph -> M <_ K )
107 efchtdvds 
 |-  ( ( M e. RR /\ K e. RR /\ M <_ K ) -> ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) )
108 103 104 106 107 syl3anc 
 |-  ( ph -> ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) )
109 efchtcl 
 |-  ( M e. RR -> ( exp ` ( theta ` M ) ) e. NN )
110 103 109 syl 
 |-  ( ph -> ( exp ` ( theta ` M ) ) e. NN )
111 110 nnzd 
 |-  ( ph -> ( exp ` ( theta ` M ) ) e. ZZ )
112 110 nnne0d 
 |-  ( ph -> ( exp ` ( theta ` M ) ) =/= 0 )
113 efchtcl 
 |-  ( K e. RR -> ( exp ` ( theta ` K ) ) e. NN )
114 104 113 syl 
 |-  ( ph -> ( exp ` ( theta ` K ) ) e. NN )
115 114 nnzd 
 |-  ( ph -> ( exp ` ( theta ` K ) ) e. ZZ )
116 dvdsval2 
 |-  ( ( ( exp ` ( theta ` M ) ) e. ZZ /\ ( exp ` ( theta ` M ) ) =/= 0 /\ ( exp ` ( theta ` K ) ) e. ZZ ) -> ( ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) )
117 111 112 115 116 syl3anc 
 |-  ( ph -> ( ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) )
118 108 117 mpbid 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ )
119 118 zred 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. RR )
120 prmz 
 |-  ( p e. Prime -> p e. ZZ )
121 fllt 
 |-  ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ p e. ZZ ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> ( |_ ` ( sqrt ` ( 2 x. N ) ) ) < p ) )
122 26 120 121 syl2an 
 |-  ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> ( |_ ` ( sqrt ` ( 2 x. N ) ) ) < p ) )
123 5 breq1i 
 |-  ( M < p <-> ( |_ ` ( sqrt ` ( 2 x. N ) ) ) < p )
124 122 123 bitr4di 
 |-  ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> M < p ) )
125 120 zred 
 |-  ( p e. Prime -> p e. RR )
126 ltnle 
 |-  ( ( M e. RR /\ p e. RR ) -> ( M < p <-> -. p <_ M ) )
127 103 125 126 syl2an 
 |-  ( ( ph /\ p e. Prime ) -> ( M < p <-> -. p <_ M ) )
128 124 127 bitrd 
 |-  ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> -. p <_ M ) )
129 bposlem1 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
130 9 129 sylan 
 |-  ( ( ph /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
131 125 adantl 
 |-  ( ( ph /\ p e. Prime ) -> p e. RR )
132 id 
 |-  ( p e. Prime -> p e. Prime )
133 pccl 
 |-  ( ( p e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
134 132 18 133 syl2anr 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
135 131 134 reexpcld 
 |-  ( ( ph /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) e. RR )
136 24 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( 2 x. N ) e. RR )
137 131 resqcld 
 |-  ( ( ph /\ p e. Prime ) -> ( p ^ 2 ) e. RR )
138 lelttr 
 |-  ( ( ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) e. RR /\ ( 2 x. N ) e. RR /\ ( p ^ 2 ) e. RR ) -> ( ( ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) /\ ( 2 x. N ) < ( p ^ 2 ) ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
139 135 136 137 138 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) /\ ( 2 x. N ) < ( p ^ 2 ) ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
140 130 139 mpand 
 |-  ( ( ph /\ p e. Prime ) -> ( ( 2 x. N ) < ( p ^ 2 ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
141 resqrtth 
 |-  ( ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) -> ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) = ( 2 x. N ) )
142 24 25 141 syl2anc 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) = ( 2 x. N ) )
143 142 breq1d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) <-> ( 2 x. N ) < ( p ^ 2 ) ) )
144 143 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) <-> ( 2 x. N ) < ( p ^ 2 ) ) )
145 134 nn0zd 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
146 72 a1i 
 |-  ( ( ph /\ p e. Prime ) -> 2 e. ZZ )
147 prmgt1 
 |-  ( p e. Prime -> 1 < p )
148 147 adantl 
 |-  ( ( ph /\ p e. Prime ) -> 1 < p )
149 131 145 146 148 ltexp2d 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 <-> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
150 140 144 149 3imtr4d 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 ) )
151 df-2 
 |-  2 = ( 1 + 1 )
152 151 breq2i 
 |-  ( ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) )
153 150 152 imbitrdi 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
154 26 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( sqrt ` ( 2 x. N ) ) e. RR )
155 24 25 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( 2 x. N ) ) )
156 155 adantr 
 |-  ( ( ph /\ p e. Prime ) -> 0 <_ ( sqrt ` ( 2 x. N ) ) )
157 prmnn 
 |-  ( p e. Prime -> p e. NN )
158 157 nnrpd 
 |-  ( p e. Prime -> p e. RR+ )
159 158 rpge0d 
 |-  ( p e. Prime -> 0 <_ p )
160 159 adantl 
 |-  ( ( ph /\ p e. Prime ) -> 0 <_ p )
161 154 131 156 160 lt2sqd 
 |-  ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) ) )
162 1z 
 |-  1 e. ZZ
163 zleltp1 
 |-  ( ( ( p pCnt ( ( 2 x. N ) _C N ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
164 145 162 163 sylancl 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
165 153 161 164 3imtr4d 
 |-  ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 ) )
166 128 165 sylbird 
 |-  ( ( ph /\ p e. Prime ) -> ( -. p <_ M -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 ) )
167 166 imp 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p <_ M ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 )
168 167 adantrl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 )
169 iftrue 
 |-  ( ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
170 169 adantl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
171 iftrue 
 |-  ( ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 1 )
172 171 adantl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 1 )
173 168 170 172 3brtr4d 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
174 0le0 
 |-  0 <_ 0
175 iffalse 
 |-  ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = 0 )
176 iffalse 
 |-  ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 0 )
177 175 176 breq12d 
 |-  ( -. ( p <_ K /\ -. p <_ M ) -> ( if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) <-> 0 <_ 0 ) )
178 174 177 mpbiri 
 |-  ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
179 178 adantl 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
180 173 179 pm2.61dan 
 |-  ( ( ph /\ p e. Prime ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
181 62 adantr 
 |-  ( ( ph /\ p e. Prime ) -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
182 69 adantr 
 |-  ( ( ph /\ p e. Prime ) -> M e. NN )
183 simpr 
 |-  ( ( ph /\ p e. Prime ) -> p e. Prime )
184 oveq1 
 |-  ( n = p -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
185 89 adantr 
 |-  ( ( ph /\ p e. Prime ) -> K e. ( ZZ>= ` M ) )
186 3 181 182 183 184 185 pcmpt2 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) )
187 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , n , 1 ) ) = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
188 187 prmorcht 
 |-  ( K e. NN -> ( exp ` ( theta ` K ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) )
189 96 188 syl 
 |-  ( ph -> ( exp ` ( theta ` K ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) )
190 187 prmorcht 
 |-  ( M e. NN -> ( exp ` ( theta ` M ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) )
191 69 190 syl 
 |-  ( ph -> ( exp ` ( theta ` M ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) )
192 189 191 oveq12d 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) )
193 192 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) )
194 193 oveq2d 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) = ( p pCnt ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) ) )
195 nncn 
 |-  ( n e. NN -> n e. CC )
196 195 exp1d 
 |-  ( n e. NN -> ( n ^ 1 ) = n )
197 196 ifeq1d 
 |-  ( n e. NN -> if ( n e. Prime , ( n ^ 1 ) , 1 ) = if ( n e. Prime , n , 1 ) )
198 197 mpteq2ia 
 |-  ( n e. NN |-> if ( n e. Prime , ( n ^ 1 ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
199 198 eqcomi 
 |-  ( n e. NN |-> if ( n e. Prime , n , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( n ^ 1 ) , 1 ) )
200 1nn0 
 |-  1 e. NN0
201 200 a1i 
 |-  ( ( ph /\ n e. Prime ) -> 1 e. NN0 )
202 201 ralrimiva 
 |-  ( ph -> A. n e. Prime 1 e. NN0 )
203 202 adantr 
 |-  ( ( ph /\ p e. Prime ) -> A. n e. Prime 1 e. NN0 )
204 eqidd 
 |-  ( n = p -> 1 = 1 )
205 199 203 182 183 204 185 pcmpt2 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
206 194 205 eqtrd 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
207 180 186 206 3brtr4d 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
208 207 ralrimiva 
 |-  ( ph -> A. p e. Prime ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
209 pc2dvds 
 |-  ( ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ /\ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) <-> A. p e. Prime ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) ) )
210 101 118 209 syl2anc 
 |-  ( ph -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) <-> A. p e. Prime ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) ) )
211 208 210 mpbird 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
212 114 nnred 
 |-  ( ph -> ( exp ` ( theta ` K ) ) e. RR )
213 110 nnred 
 |-  ( ph -> ( exp ` ( theta ` M ) ) e. RR )
214 114 nngt0d 
 |-  ( ph -> 0 < ( exp ` ( theta ` K ) ) )
215 110 nngt0d 
 |-  ( ph -> 0 < ( exp ` ( theta ` M ) ) )
216 212 213 214 215 divgt0d 
 |-  ( ph -> 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
217 elnnz 
 |-  ( ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN <-> ( ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ /\ 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
218 118 216 217 sylanbrc 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN )
219 dvdsle 
 |-  ( ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ /\ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN ) -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
220 101 218 219 syl2anc 
 |-  ( ph -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
221 211 220 mpd 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
222 nndivre 
 |-  ( ( ( exp ` ( theta ` K ) ) e. RR /\ 4 e. NN ) -> ( ( exp ` ( theta ` K ) ) / 4 ) e. RR )
223 212 6 222 sylancl 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / 4 ) e. RR )
224 4re 
 |-  4 e. RR
225 224 a1i 
 |-  ( ph -> 4 e. RR )
226 6re 
 |-  6 e. RR
227 226 a1i 
 |-  ( ph -> 6 e. RR )
228 4lt6 
 |-  4 < 6
229 228 a1i 
 |-  ( ph -> 4 < 6 )
230 cht3 
 |-  ( theta ` 3 ) = ( log ` 6 )
231 230 fveq2i 
 |-  ( exp ` ( theta ` 3 ) ) = ( exp ` ( log ` 6 ) )
232 6pos 
 |-  0 < 6
233 226 232 elrpii 
 |-  6 e. RR+
234 reeflog 
 |-  ( 6 e. RR+ -> ( exp ` ( log ` 6 ) ) = 6 )
235 233 234 ax-mp 
 |-  ( exp ` ( log ` 6 ) ) = 6
236 231 235 eqtri 
 |-  ( exp ` ( theta ` 3 ) ) = 6
237 3re 
 |-  3 e. RR
238 237 a1i 
 |-  ( ph -> 3 e. RR )
239 eluzle 
 |-  ( M e. ( ZZ>= ` 3 ) -> 3 <_ M )
240 67 239 syl 
 |-  ( ph -> 3 <_ M )
241 chtwordi 
 |-  ( ( 3 e. RR /\ M e. RR /\ 3 <_ M ) -> ( theta ` 3 ) <_ ( theta ` M ) )
242 238 103 240 241 syl3anc 
 |-  ( ph -> ( theta ` 3 ) <_ ( theta ` M ) )
243 chtcl 
 |-  ( 3 e. RR -> ( theta ` 3 ) e. RR )
244 237 243 ax-mp 
 |-  ( theta ` 3 ) e. RR
245 chtcl 
 |-  ( M e. RR -> ( theta ` M ) e. RR )
246 103 245 syl 
 |-  ( ph -> ( theta ` M ) e. RR )
247 efle 
 |-  ( ( ( theta ` 3 ) e. RR /\ ( theta ` M ) e. RR ) -> ( ( theta ` 3 ) <_ ( theta ` M ) <-> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) ) )
248 244 246 247 sylancr 
 |-  ( ph -> ( ( theta ` 3 ) <_ ( theta ` M ) <-> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) ) )
249 242 248 mpbid 
 |-  ( ph -> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) )
250 236 249 eqbrtrrid 
 |-  ( ph -> 6 <_ ( exp ` ( theta ` M ) ) )
251 225 227 213 229 250 ltletrd 
 |-  ( ph -> 4 < ( exp ` ( theta ` M ) ) )
252 4pos 
 |-  0 < 4
253 252 a1i 
 |-  ( ph -> 0 < 4 )
254 ltdiv2 
 |-  ( ( ( 4 e. RR /\ 0 < 4 ) /\ ( ( exp ` ( theta ` M ) ) e. RR /\ 0 < ( exp ` ( theta ` M ) ) ) /\ ( ( exp ` ( theta ` K ) ) e. RR /\ 0 < ( exp ` ( theta ` K ) ) ) ) -> ( 4 < ( exp ` ( theta ` M ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) ) )
255 225 253 213 215 212 214 254 syl222anc 
 |-  ( ph -> ( 4 < ( exp ` ( theta ` M ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) ) )
256 251 255 mpbid 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) )
257 30 a1i 
 |-  ( ph -> 2 e. RR )
258 2lt3 
 |-  2 < 3
259 258 a1i 
 |-  ( ph -> 2 < 3 )
260 238 103 104 240 106 letrd 
 |-  ( ph -> 3 <_ K )
261 257 238 104 259 260 ltletrd 
 |-  ( ph -> 2 < K )
262 chtub 
 |-  ( ( K e. RR /\ 2 < K ) -> ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
263 104 261 262 syl2anc 
 |-  ( ph -> ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
264 chtcl 
 |-  ( K e. RR -> ( theta ` K ) e. RR )
265 104 264 syl 
 |-  ( ph -> ( theta ` K ) e. RR )
266 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
267 35 266 ax-mp 
 |-  ( log ` 2 ) e. RR
268 3z 
 |-  3 e. ZZ
269 zsubcl 
 |-  ( ( ( 2 x. K ) e. ZZ /\ 3 e. ZZ ) -> ( ( 2 x. K ) - 3 ) e. ZZ )
270 78 268 269 sylancl 
 |-  ( ph -> ( ( 2 x. K ) - 3 ) e. ZZ )
271 270 zred 
 |-  ( ph -> ( ( 2 x. K ) - 3 ) e. RR )
272 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. K ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR )
273 267 271 272 sylancr 
 |-  ( ph -> ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR )
274 eflt 
 |-  ( ( ( theta ` K ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR ) -> ( ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) <-> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) ) )
275 265 273 274 syl2anc 
 |-  ( ph -> ( ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) <-> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) ) )
276 263 275 mpbid 
 |-  ( ph -> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
277 reexplog 
 |-  ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 3 ) e. ZZ ) -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) )
278 35 270 277 sylancr 
 |-  ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) )
279 270 zcnd 
 |-  ( ph -> ( ( 2 x. K ) - 3 ) e. CC )
280 267 recni 
 |-  ( log ` 2 ) e. CC
281 mulcom 
 |-  ( ( ( ( 2 x. K ) - 3 ) e. CC /\ ( log ` 2 ) e. CC ) -> ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) = ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
282 279 280 281 sylancl 
 |-  ( ph -> ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) = ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
283 282 fveq2d 
 |-  ( ph -> ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) = ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
284 278 283 eqtrd 
 |-  ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
285 276 284 breqtrrd 
 |-  ( ph -> ( exp ` ( theta ` K ) ) < ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
286 3p2e5 
 |-  ( 3 + 2 ) = 5
287 286 oveq1i 
 |-  ( ( 3 + 2 ) - 2 ) = ( 5 - 2 )
288 3cn 
 |-  3 e. CC
289 2cn 
 |-  2 e. CC
290 288 289 pncan3oi 
 |-  ( ( 3 + 2 ) - 2 ) = 3
291 287 290 eqtr3i 
 |-  ( 5 - 2 ) = 3
292 291 oveq2i 
 |-  ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( 2 x. K ) - 3 )
293 78 zcnd 
 |-  ( ph -> ( 2 x. K ) e. CC )
294 5cn 
 |-  5 e. CC
295 subsub 
 |-  ( ( ( 2 x. K ) e. CC /\ 5 e. CC /\ 2 e. CC ) -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
296 294 289 295 mp3an23 
 |-  ( ( 2 x. K ) e. CC -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
297 293 296 syl 
 |-  ( ph -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
298 292 297 eqtr3id 
 |-  ( ph -> ( ( 2 x. K ) - 3 ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
299 298 oveq2d 
 |-  ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) )
300 2ne0 
 |-  2 =/= 0
301 cxpexpz 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ ( ( 2 x. K ) - 3 ) e. ZZ ) -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
302 289 300 270 301 mp3an12i 
 |-  ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
303 81 zcnd 
 |-  ( ph -> ( ( 2 x. K ) - 5 ) e. CC )
304 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
305 cxpadd 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( 2 x. K ) - 5 ) e. CC /\ 2 e. CC ) -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
306 304 289 305 mp3an13 
 |-  ( ( ( 2 x. K ) - 5 ) e. CC -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
307 303 306 syl 
 |-  ( ph -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
308 299 302 307 3eqtr3d 
 |-  ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
309 2nn0 
 |-  2 e. NN0
310 cxpexp 
 |-  ( ( 2 e. CC /\ 2 e. NN0 ) -> ( 2 ^c 2 ) = ( 2 ^ 2 ) )
311 289 309 310 mp2an 
 |-  ( 2 ^c 2 ) = ( 2 ^ 2 )
312 sq2 
 |-  ( 2 ^ 2 ) = 4
313 311 312 eqtri 
 |-  ( 2 ^c 2 ) = 4
314 313 oveq2i 
 |-  ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 )
315 308 314 eqtrdi 
 |-  ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) )
316 285 315 breqtrd 
 |-  ( ph -> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) )
317 224 252 pm3.2i 
 |-  ( 4 e. RR /\ 0 < 4 )
318 317 a1i 
 |-  ( ph -> ( 4 e. RR /\ 0 < 4 ) )
319 ltdivmul2 
 |-  ( ( ( exp ` ( theta ` K ) ) e. RR /\ ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) ) )
320 212 85 318 319 syl3anc 
 |-  ( ph -> ( ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) ) )
321 316 320 mpbird 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
322 119 223 85 256 321 lttrd 
 |-  ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
323 102 119 85 221 322 lelttrd 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
324 97 nnred 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) e. RR )
325 nnre 
 |-  ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( seq 1 ( x. , F ) ` M ) e. RR )
326 nngt0 
 |-  ( ( seq 1 ( x. , F ) ` M ) e. NN -> 0 < ( seq 1 ( x. , F ) ` M ) )
327 325 326 jca 
 |-  ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) )
328 70 327 syl 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) )
329 ltdivmul 
 |-  ( ( ( seq 1 ( x. , F ) ` K ) e. RR /\ ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR /\ ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) ) -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
330 324 85 328 329 syl3anc 
 |-  ( ph -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
331 323 330 mpbid 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
332 87 331 eqbrtrrd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
333 34 85 remulcld 
 |-  ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
334 1 2 3 4 5 bposlem5 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
335 71 34 84 lemul1d 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) <-> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
336 334 335 mpbid 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
337 78 zred 
 |-  ( ph -> ( 2 x. K ) e. RR )
338 41 a1i 
 |-  ( ph -> 5 e. RR )
339 flle 
 |-  ( ( ( 2 x. N ) / 3 ) e. RR -> ( |_ ` ( ( 2 x. N ) / 3 ) ) <_ ( ( 2 x. N ) / 3 ) )
340 74 339 syl 
 |-  ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) <_ ( ( 2 x. N ) / 3 ) )
341 4 340 eqbrtrid 
 |-  ( ph -> K <_ ( ( 2 x. N ) / 3 ) )
342 2pos 
 |-  0 < 2
343 30 342 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
344 343 a1i 
 |-  ( ph -> ( 2 e. RR /\ 0 < 2 ) )
345 lemul2 
 |-  ( ( K e. RR /\ ( ( 2 x. N ) / 3 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( K <_ ( ( 2 x. N ) / 3 ) <-> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) ) )
346 104 74 344 345 syl3anc 
 |-  ( ph -> ( K <_ ( ( 2 x. N ) / 3 ) <-> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) ) )
347 341 346 mpbid 
 |-  ( ph -> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) )
348 22 nncnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
349 3ne0 
 |-  3 =/= 0
350 288 349 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
351 divass 
 |-  ( ( 2 e. CC /\ ( 2 x. N ) e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
352 289 350 351 mp3an13 
 |-  ( ( 2 x. N ) e. CC -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
353 348 352 syl 
 |-  ( ph -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
354 9 nncnd 
 |-  ( ph -> N e. CC )
355 mulass 
 |-  ( ( 2 e. CC /\ 2 e. CC /\ N e. CC ) -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
356 289 289 354 355 mp3an12i 
 |-  ( ph -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
357 2t2e4 
 |-  ( 2 x. 2 ) = 4
358 357 oveq1i 
 |-  ( ( 2 x. 2 ) x. N ) = ( 4 x. N )
359 356 358 eqtr3di 
 |-  ( ph -> ( 2 x. ( 2 x. N ) ) = ( 4 x. N ) )
360 359 oveq1d 
 |-  ( ph -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( ( 4 x. N ) / 3 ) )
361 353 360 eqtr3d 
 |-  ( ph -> ( 2 x. ( ( 2 x. N ) / 3 ) ) = ( ( 4 x. N ) / 3 ) )
362 347 361 breqtrd 
 |-  ( ph -> ( 2 x. K ) <_ ( ( 4 x. N ) / 3 ) )
363 337 40 338 362 lesub1dd 
 |-  ( ph -> ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) )
364 1lt2 
 |-  1 < 2
365 364 a1i 
 |-  ( ph -> 1 < 2 )
366 257 365 82 43 cxpled 
 |-  ( ph -> ( ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) <-> ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
367 363 366 mpbid 
 |-  ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) )
368 85 46 33 lemul2d 
 |-  ( ph -> ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) <-> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) ) )
369 367 368 mpbid 
 |-  ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
370 86 333 47 336 369 letrd 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
371 19 86 47 332 370 ltletrd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
372 14 19 47 58 371 lttrd 
 |-  ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )