Metamath Proof Explorer


Theorem prmreclem6

Description: Lemma for prmrec . If the series F was convergent, there would be some k such that the sum starting from k + 1 sums to less than 1 / 2 ; this is a sufficient hypothesis for prmreclem5 to produce the contradictory bound N / 2 < ( 2 ^ k ) sqrt N , which is false for N = 2 ^ ( 2 k + 2 ) . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis prmrec.1 F = n if n 1 n 0
Assertion prmreclem6 ¬ seq 1 + F dom

Proof

Step Hyp Ref Expression
1 prmrec.1 F = n if n 1 n 0
2 nnuz = 1
3 1zzd 1
4 nnrecre n 1 n
5 4 adantl n 1 n
6 0re 0
7 ifcl 1 n 0 if n 1 n 0
8 5 6 7 sylancl n if n 1 n 0
9 8 1 fmptd F :
10 9 ffvelrnda j F j
11 2 3 10 serfre seq 1 + F :
12 11 mptru seq 1 + F :
13 frn seq 1 + F : ran seq 1 + F
14 12 13 mp1i seq 1 + F dom ran seq 1 + F
15 1nn 1
16 12 fdmi dom seq 1 + F =
17 15 16 eleqtrri 1 dom seq 1 + F
18 ne0i 1 dom seq 1 + F dom seq 1 + F
19 dm0rn0 dom seq 1 + F = ran seq 1 + F =
20 19 necon3bii dom seq 1 + F ran seq 1 + F
21 18 20 sylib 1 dom seq 1 + F ran seq 1 + F
22 17 21 mp1i seq 1 + F dom ran seq 1 + F
23 1zzd seq 1 + F dom 1
24 climdm seq 1 + F dom seq 1 + F seq 1 + F
25 24 biimpi seq 1 + F dom seq 1 + F seq 1 + F
26 12 a1i seq 1 + F dom seq 1 + F :
27 26 ffvelrnda seq 1 + F dom k seq 1 + F k
28 2 23 25 27 climrecl seq 1 + F dom seq 1 + F
29 simpr seq 1 + F dom k k
30 25 adantr seq 1 + F dom k seq 1 + F seq 1 + F
31 eleq1w n = j n j
32 oveq2 n = j 1 n = 1 j
33 31 32 ifbieq1d n = j if n 1 n 0 = if j 1 j 0
34 prmnn j j
35 34 adantl j j
36 35 nnrecred j 1 j
37 6 a1i ¬ j 0
38 36 37 ifclda if j 1 j 0
39 38 mptru if j 1 j 0
40 39 elexi if j 1 j 0 V
41 33 1 40 fvmpt j F j = if j 1 j 0
42 41 adantl seq 1 + F dom j F j = if j 1 j 0
43 39 a1i seq 1 + F dom j if j 1 j 0
44 42 43 eqeltrd seq 1 + F dom j F j
45 44 adantlr seq 1 + F dom k j F j
46 nnrp j j +
47 46 adantl seq 1 + F dom j j +
48 47 rpreccld seq 1 + F dom j 1 j +
49 48 rpge0d seq 1 + F dom j 0 1 j
50 0le0 0 0
51 breq2 1 j = if j 1 j 0 0 1 j 0 if j 1 j 0
52 breq2 0 = if j 1 j 0 0 0 0 if j 1 j 0
53 51 52 ifboth 0 1 j 0 0 0 if j 1 j 0
54 49 50 53 sylancl seq 1 + F dom j 0 if j 1 j 0
55 54 42 breqtrrd seq 1 + F dom j 0 F j
56 55 adantlr seq 1 + F dom k j 0 F j
57 2 29 30 45 56 climserle seq 1 + F dom k seq 1 + F k seq 1 + F
58 57 ralrimiva seq 1 + F dom k seq 1 + F k seq 1 + F
59 brralrspcev seq 1 + F k seq 1 + F k seq 1 + F x k seq 1 + F k x
60 28 58 59 syl2anc seq 1 + F dom x k seq 1 + F k x
61 ffn seq 1 + F : seq 1 + F Fn
62 breq1 z = seq 1 + F k z x seq 1 + F k x
63 62 ralrn seq 1 + F Fn z ran seq 1 + F z x k seq 1 + F k x
64 12 61 63 mp2b z ran seq 1 + F z x k seq 1 + F k x
65 64 rexbii x z ran seq 1 + F z x x k seq 1 + F k x
66 60 65 sylibr seq 1 + F dom x z ran seq 1 + F z x
67 14 22 66 suprcld seq 1 + F dom sup ran seq 1 + F <
68 2rp 2 +
69 rpreccl 2 + 1 2 +
70 68 69 ax-mp 1 2 +
71 ltsubrp sup ran seq 1 + F < 1 2 + sup ran seq 1 + F < 1 2 < sup ran seq 1 + F <
72 67 70 71 sylancl seq 1 + F dom sup ran seq 1 + F < 1 2 < sup ran seq 1 + F <
73 halfre 1 2
74 resubcl sup ran seq 1 + F < 1 2 sup ran seq 1 + F < 1 2
75 67 73 74 sylancl seq 1 + F dom sup ran seq 1 + F < 1 2
76 suprlub ran seq 1 + F ran seq 1 + F x z ran seq 1 + F z x sup ran seq 1 + F < 1 2 sup ran seq 1 + F < 1 2 < sup ran seq 1 + F < y ran seq 1 + F sup ran seq 1 + F < 1 2 < y
77 14 22 66 75 76 syl31anc seq 1 + F dom sup ran seq 1 + F < 1 2 < sup ran seq 1 + F < y ran seq 1 + F sup ran seq 1 + F < 1 2 < y
78 72 77 mpbid seq 1 + F dom y ran seq 1 + F sup ran seq 1 + F < 1 2 < y
79 breq2 y = seq 1 + F k sup ran seq 1 + F < 1 2 < y sup ran seq 1 + F < 1 2 < seq 1 + F k
80 79 rexrn seq 1 + F Fn y ran seq 1 + F sup ran seq 1 + F < 1 2 < y k sup ran seq 1 + F < 1 2 < seq 1 + F k
81 12 61 80 mp2b y ran seq 1 + F sup ran seq 1 + F < 1 2 < y k sup ran seq 1 + F < 1 2 < seq 1 + F k
82 78 81 sylib seq 1 + F dom k sup ran seq 1 + F < 1 2 < seq 1 + F k
83 2re 2
84 2nn 2
85 nnmulcl 2 k 2 k
86 84 29 85 sylancr seq 1 + F dom k 2 k
87 86 peano2nnd seq 1 + F dom k 2 k + 1
88 87 nnnn0d seq 1 + F dom k 2 k + 1 0
89 reexpcl 2 2 k + 1 0 2 2 k + 1
90 83 88 89 sylancr seq 1 + F dom k 2 2 k + 1
91 90 ltnrd seq 1 + F dom k ¬ 2 2 k + 1 < 2 2 k + 1
92 29 adantr seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 k
93 peano2nn k k + 1
94 93 adantl seq 1 + F dom k k + 1
95 94 nnnn0d seq 1 + F dom k k + 1 0
96 nnexpcl 2 k + 1 0 2 k + 1
97 84 95 96 sylancr seq 1 + F dom k 2 k + 1
98 97 nnsqcld seq 1 + F dom k 2 k + 1 2
99 98 adantr seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 2 k + 1 2
100 breq1 p = w p r w r
101 100 notbid p = w ¬ p r ¬ w r
102 101 cbvralvw p 1 k ¬ p r w 1 k ¬ w r
103 breq2 r = n w r w n
104 103 notbid r = n ¬ w r ¬ w n
105 104 ralbidv r = n w 1 k ¬ w r w 1 k ¬ w n
106 102 105 syl5bb r = n p 1 k ¬ p r w 1 k ¬ w n
107 106 cbvrabv r 1 2 k + 1 2 | p 1 k ¬ p r = n 1 2 k + 1 2 | w 1 k ¬ w n
108 simpll seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 seq 1 + F dom
109 eleq1w m = j m j
110 oveq2 m = j 1 m = 1 j
111 109 110 ifbieq1d m = j if m 1 m 0 = if j 1 j 0
112 111 cbvsumv m k + 1 if m 1 m 0 = j k + 1 if j 1 j 0
113 simpr seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 j k + 1 if j 1 j 0 < 1 2
114 112 113 eqbrtrid seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 m k + 1 if m 1 m 0 < 1 2
115 eqid w n 1 2 k + 1 2 | w w n = w n 1 2 k + 1 2 | w w n
116 1 92 99 107 108 114 115 prmreclem5 seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 2 k + 1 2 2 < 2 k 2 k + 1 2
117 116 ex seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 2 k + 1 2 2 < 2 k 2 k + 1 2
118 eqid k + 1 = k + 1
119 94 nnzd seq 1 + F dom k k + 1
120 eluznn k + 1 j k + 1 j
121 94 120 sylan seq 1 + F dom k j k + 1 j
122 121 41 syl seq 1 + F dom k j k + 1 F j = if j 1 j 0
123 39 a1i seq 1 + F dom k j k + 1 if j 1 j 0
124 simpl seq 1 + F dom k seq 1 + F dom
125 41 adantl seq 1 + F dom k j F j = if j 1 j 0
126 39 recni if j 1 j 0
127 126 a1i seq 1 + F dom k j if j 1 j 0
128 125 127 eqeltrd seq 1 + F dom k j F j
129 2 94 128 iserex seq 1 + F dom k seq 1 + F dom seq k + 1 + F dom
130 124 129 mpbid seq 1 + F dom k seq k + 1 + F dom
131 118 119 122 123 130 isumrecl seq 1 + F dom k j k + 1 if j 1 j 0
132 73 a1i seq 1 + F dom k 1 2
133 elfznn j 1 k j
134 133 adantl seq 1 + F dom k j 1 k j
135 134 41 syl seq 1 + F dom k j 1 k F j = if j 1 j 0
136 29 2 eleqtrdi seq 1 + F dom k k 1
137 126 a1i seq 1 + F dom k j 1 k if j 1 j 0
138 135 136 137 fsumser seq 1 + F dom k j = 1 k if j 1 j 0 = seq 1 + F k
139 138 27 eqeltrd seq 1 + F dom k j = 1 k if j 1 j 0
140 131 132 139 ltadd2d seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 j = 1 k if j 1 j 0 + j k + 1 if j 1 j 0 < j = 1 k if j 1 j 0 + 1 2
141 2 118 94 125 127 124 isumsplit seq 1 + F dom k j if j 1 j 0 = j = 1 k + 1 - 1 if j 1 j 0 + j k + 1 if j 1 j 0
142 nncn k k
143 142 adantl seq 1 + F dom k k
144 ax-1cn 1
145 pncan k 1 k + 1 - 1 = k
146 143 144 145 sylancl seq 1 + F dom k k + 1 - 1 = k
147 146 oveq2d seq 1 + F dom k 1 k + 1 - 1 = 1 k
148 147 sumeq1d seq 1 + F dom k j = 1 k + 1 - 1 if j 1 j 0 = j = 1 k if j 1 j 0
149 148 oveq1d seq 1 + F dom k j = 1 k + 1 - 1 if j 1 j 0 + j k + 1 if j 1 j 0 = j = 1 k if j 1 j 0 + j k + 1 if j 1 j 0
150 141 149 eqtrd seq 1 + F dom k j if j 1 j 0 = j = 1 k if j 1 j 0 + j k + 1 if j 1 j 0
151 150 breq1d seq 1 + F dom k j if j 1 j 0 < j = 1 k if j 1 j 0 + 1 2 j = 1 k if j 1 j 0 + j k + 1 if j 1 j 0 < j = 1 k if j 1 j 0 + 1 2
152 140 151 bitr4d seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 j if j 1 j 0 < j = 1 k if j 1 j 0 + 1 2
153 eqid seq 1 + F = seq 1 + F
154 2 153 23 42 43 54 60 isumsup seq 1 + F dom j if j 1 j 0 = sup ran seq 1 + F <
155 154 67 eqeltrd seq 1 + F dom j if j 1 j 0
156 155 adantr seq 1 + F dom k j if j 1 j 0
157 156 132 139 ltsubaddd seq 1 + F dom k j if j 1 j 0 1 2 < j = 1 k if j 1 j 0 j if j 1 j 0 < j = 1 k if j 1 j 0 + 1 2
158 154 adantr seq 1 + F dom k j if j 1 j 0 = sup ran seq 1 + F <
159 158 oveq1d seq 1 + F dom k j if j 1 j 0 1 2 = sup ran seq 1 + F < 1 2
160 159 138 breq12d seq 1 + F dom k j if j 1 j 0 1 2 < j = 1 k if j 1 j 0 sup ran seq 1 + F < 1 2 < seq 1 + F k
161 152 157 160 3bitr2d seq 1 + F dom k j k + 1 if j 1 j 0 < 1 2 sup ran seq 1 + F < 1 2 < seq 1 + F k
162 2cn 2
163 162 a1i seq 1 + F dom k 2
164 144 a1i seq 1 + F dom k 1
165 163 143 164 adddid seq 1 + F dom k 2 k + 1 = 2 k + 2 1
166 94 nncnd seq 1 + F dom k k + 1
167 mulcom k + 1 2 k + 1 2 = 2 k + 1
168 166 162 167 sylancl seq 1 + F dom k k + 1 2 = 2 k + 1
169 86 nncnd seq 1 + F dom k 2 k
170 169 164 164 addassd seq 1 + F dom k 2 k + 1 + 1 = 2 k + 1 + 1
171 144 2timesi 2 1 = 1 + 1
172 171 oveq2i 2 k + 2 1 = 2 k + 1 + 1
173 170 172 eqtr4di seq 1 + F dom k 2 k + 1 + 1 = 2 k + 2 1
174 165 168 173 3eqtr4d seq 1 + F dom k k + 1 2 = 2 k + 1 + 1
175 174 oveq2d seq 1 + F dom k 2 k + 1 2 = 2 2 k + 1 + 1
176 2nn0 2 0
177 176 a1i seq 1 + F dom k 2 0
178 163 177 95 expmuld seq 1 + F dom k 2 k + 1 2 = 2 k + 1 2
179 expp1 2 2 k + 1 0 2 2 k + 1 + 1 = 2 2 k + 1 2
180 162 88 179 sylancr seq 1 + F dom k 2 2 k + 1 + 1 = 2 2 k + 1 2
181 175 178 180 3eqtr3d seq 1 + F dom k 2 k + 1 2 = 2 2 k + 1 2
182 181 oveq1d seq 1 + F dom k 2 k + 1 2 2 = 2 2 k + 1 2 2
183 expcl 2 2 k + 1 0 2 2 k + 1
184 162 88 183 sylancr seq 1 + F dom k 2 2 k + 1
185 2ne0 2 0
186 divcan4 2 2 k + 1 2 2 0 2 2 k + 1 2 2 = 2 2 k + 1
187 162 185 186 mp3an23 2 2 k + 1 2 2 k + 1 2 2 = 2 2 k + 1
188 184 187 syl seq 1 + F dom k 2 2 k + 1 2 2 = 2 2 k + 1
189 182 188 eqtrd seq 1 + F dom k 2 k + 1 2 2 = 2 2 k + 1
190 nnnn0 k k 0
191 190 adantl seq 1 + F dom k k 0
192 163 95 191 expaddd seq 1 + F dom k 2 k + k + 1 = 2 k 2 k + 1
193 143 2timesd seq 1 + F dom k 2 k = k + k
194 193 oveq1d seq 1 + F dom k 2 k + 1 = k + k + 1
195 143 143 164 addassd seq 1 + F dom k k + k + 1 = k + k + 1
196 194 195 eqtrd seq 1 + F dom k 2 k + 1 = k + k + 1
197 196 oveq2d seq 1 + F dom k 2 2 k + 1 = 2 k + k + 1
198 97 nnrpd seq 1 + F dom k 2 k + 1 +
199 198 rprege0d seq 1 + F dom k 2 k + 1 0 2 k + 1
200 sqrtsq 2 k + 1 0 2 k + 1 2 k + 1 2 = 2 k + 1
201 199 200 syl seq 1 + F dom k 2 k + 1 2 = 2 k + 1
202 201 oveq2d seq 1 + F dom k 2 k 2 k + 1 2 = 2 k 2 k + 1
203 192 197 202 3eqtr4rd seq 1 + F dom k 2 k 2 k + 1 2 = 2 2 k + 1
204 189 203 breq12d seq 1 + F dom k 2 k + 1 2 2 < 2 k 2 k + 1 2 2 2 k + 1 < 2 2 k + 1
205 117 161 204 3imtr3d seq 1 + F dom k sup ran seq 1 + F < 1 2 < seq 1 + F k 2 2 k + 1 < 2 2 k + 1
206 91 205 mtod seq 1 + F dom k ¬ sup ran seq 1 + F < 1 2 < seq 1 + F k
207 206 nrexdv seq 1 + F dom ¬ k sup ran seq 1 + F < 1 2 < seq 1 + F k
208 82 207 pm2.65i ¬ seq 1 + F dom