Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmreclem6 Structured version   Unicode version

Theorem prmreclem6 13289
 Description: Lemma for prmrec 13290. If the series was convergent, there would be some such that the sum starting from sums to less than ; this is a sufficient hypothesis for prmreclem5 13288 to produce the contradictory bound , which is false for . (Contributed by Mario Carneiro, 6-Aug-2014.)
Hypothesis
Ref Expression
prmrec.1
Assertion
Ref Expression
prmreclem6
Distinct variable group:   ,

Proof of Theorem prmreclem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10521 . . . . . . . . . 10
2 1z 10311 . . . . . . . . . . 11
32a1i 11 . . . . . . . . . 10
4 nnrecre 10036 . . . . . . . . . . . . . 14
54adantl 453 . . . . . . . . . . . . 13
6 0re 9091 . . . . . . . . . . . . 13
7 ifcl 3775 . . . . . . . . . . . . 13
85, 6, 7sylancl 644 . . . . . . . . . . . 12
9 prmrec.1 . . . . . . . . . . . 12
108, 9fmptd 5893 . . . . . . . . . . 11
1110ffvelrnda 5870 . . . . . . . . . 10
121, 3, 11serfre 11352 . . . . . . . . 9
1312trud 1332 . . . . . . . 8
14 frn 5597 . . . . . . . 8
1513, 14ax-mp 8 . . . . . . 7
1615a1i 11 . . . . . 6
17 1nn 10011 . . . . . . . . 9
1813fdmi 5596 . . . . . . . . 9
1917, 18eleqtrri 2509 . . . . . . . 8
20 ne0i 3634 . . . . . . . . 9
21 dm0rn0 5086 . . . . . . . . . 10
2221necon3bii 2633 . . . . . . . . 9
2320, 22sylib 189 . . . . . . . 8
2419, 23ax-mp 8 . . . . . . 7
2524a1i 11 . . . . . 6
262a1i 11 . . . . . . . . 9
27 climdm 12348 . . . . . . . . . 10
2827biimpi 187 . . . . . . . . 9
2913a1i 11 . . . . . . . . . 10
3029ffvelrnda 5870 . . . . . . . . 9
311, 26, 28, 30climrecl 12377 . . . . . . . 8
32 simpr 448 . . . . . . . . . 10
3328adantr 452 . . . . . . . . . 10
34 eleq1 2496 . . . . . . . . . . . . . . 15
35 oveq2 6089 . . . . . . . . . . . . . . 15
36 eqidd 2437 . . . . . . . . . . . . . . 15
3734, 35, 36ifbieq12d 3761 . . . . . . . . . . . . . 14
38 prmnn 13082 . . . . . . . . . . . . . . . . . . 19
3938adantl 453 . . . . . . . . . . . . . . . . . 18
4039nnrecred 10045 . . . . . . . . . . . . . . . . 17
416a1i 11 . . . . . . . . . . . . . . . . 17
4240, 41ifclda 3766 . . . . . . . . . . . . . . . 16
4342trud 1332 . . . . . . . . . . . . . . 15
4443elexi 2965 . . . . . . . . . . . . . 14
4537, 9, 44fvmpt 5806 . . . . . . . . . . . . 13
4645adantl 453 . . . . . . . . . . . 12
4743a1i 11 . . . . . . . . . . . 12
4846, 47eqeltrd 2510 . . . . . . . . . . 11
4948adantlr 696 . . . . . . . . . 10
50 nnrp 10621 . . . . . . . . . . . . . . . 16
5150adantl 453 . . . . . . . . . . . . . . 15
5251rpreccld 10658 . . . . . . . . . . . . . 14
5352rpge0d 10652 . . . . . . . . . . . . 13
54 0le0 10081 . . . . . . . . . . . . 13
55 breq2 4216 . . . . . . . . . . . . . 14
56 breq2 4216 . . . . . . . . . . . . . 14
5755, 56ifboth 3770 . . . . . . . . . . . . 13
5853, 54, 57sylancl 644 . . . . . . . . . . . 12
5958, 46breqtrrd 4238 . . . . . . . . . . 11
6059adantlr 696 . . . . . . . . . 10
611, 32, 33, 49, 60climserle 12456 . . . . . . . . 9
6261ralrimiva 2789 . . . . . . . 8
63 breq2 4216 . . . . . . . . . 10
6463ralbidv 2725 . . . . . . . . 9
6564rspcev 3052 . . . . . . . 8
6631, 62, 65syl2anc 643 . . . . . . 7
67 ffn 5591 . . . . . . . . 9
68 breq1 4215 . . . . . . . . . 10
6968ralrn 5873 . . . . . . . . 9
7013, 67, 69mp2b 10 . . . . . . . 8
7170rexbii 2730 . . . . . . 7
7266, 71sylibr 204 . . . . . 6
73 suprcl 9968 . . . . . 6
7416, 25, 72, 73syl3anc 1184 . . . . 5
75 2rp 10617 . . . . . 6
76 rpreccl 10635 . . . . . 6
7775, 76ax-mp 8 . . . . 5
78 ltsubrp 10643 . . . . 5
7974, 77, 78sylancl 644 . . . 4
80 rpre 10618 . . . . . . 7
8177, 80ax-mp 8 . . . . . 6
82 resubcl 9365 . . . . . 6
8374, 81, 82sylancl 644 . . . . 5
84 suprlub 9970 . . . . 5
8516, 25, 72, 83, 84syl31anc 1187 . . . 4
8679, 85mpbid 202 . . 3
87 breq2 4216 . . . . 5
8887rexrn 5872 . . . 4
8913, 67, 88mp2b 10 . . 3
9086, 89sylib 189 . 2
91 2re 10069 . . . . . 6
92 2nn 10133 . . . . . . . . 9
93 nnmulcl 10023 . . . . . . . . 9
9492, 32, 93sylancr 645 . . . . . . . 8
9594peano2nnd 10017 . . . . . . 7
9695nnnn0d 10274 . . . . . 6
97 reexpcl 11398 . . . . . 6
9891, 96, 97sylancr 645 . . . . 5
9998ltnrd 9207 . . . 4
10032adantr 452 . . . . . . 7
101 peano2nn 10012 . . . . . . . . . . . 12
102101adantl 453 . . . . . . . . . . 11
103102nnnn0d 10274 . . . . . . . . . 10
104 nnexpcl 11394 . . . . . . . . . 10
10592, 103, 104sylancr 645 . . . . . . . . 9
106105nnsqcld 11543 . . . . . . . 8
107106adantr 452 . . . . . . 7
108 breq1 4215 . . . . . . . . . . 11
109108notbid 286 . . . . . . . . . 10
110109cbvralv 2932 . . . . . . . . 9
111 breq2 4216 . . . . . . . . . . 11
112111notbid 286 . . . . . . . . . 10
113112ralbidv 2725 . . . . . . . . 9
114110, 113syl5bb 249 . . . . . . . 8
115114cbvrabv 2955 . . . . . . 7
116 simpll 731 . . . . . . 7
117 eleq1 2496 . . . . . . . . . 10
118 oveq2 6089 . . . . . . . . . 10
119 eqidd 2437 . . . . . . . . . 10
120117, 118, 119ifbieq12d 3761 . . . . . . . . 9
121120cbvsumv 12490 . . . . . . . 8
122 simpr 448 . . . . . . . 8
123121, 122syl5eqbr 4245 . . . . . . 7
124 eqid 2436 . . . . . . 7
1259, 100, 107, 115, 116, 123, 124prmreclem5 13288 . . . . . 6
126125ex 424 . . . . 5
127 eqid 2436 . . . . . . . . 9
128102nnzd 10374 . . . . . . . . 9
1291uztrn2 10503 . . . . . . . . . . 11
130102, 129sylan 458 . . . . . . . . . 10
131130, 45syl 16 . . . . . . . . 9
13243a1i 11 . . . . . . . . 9
133 simpl 444 . . . . . . . . . 10
13445adantl 453 . . . . . . . . . . . 12
13543recni 9102 . . . . . . . . . . . . 13
136135a1i 11 . . . . . . . . . . . 12
137134, 136eqeltrd 2510 . . . . . . . . . . 11
1381, 102, 137iserex 12450 . . . . . . . . . 10
139133, 138mpbid 202 . . . . . . . . 9
140127, 128, 131, 132, 139isumrecl 12549 . . . . . . . 8
14181a1i 11 . . . . . . . 8
142 elfznn 11080 . . . . . . . . . . . 12
143142adantl 453 . . . . . . . . . . 11
144143, 45syl 16 . . . . . . . . . 10
14532, 1syl6eleq 2526 . . . . . . . . . 10
146135a1i 11 . . . . . . . . . 10
147144, 145, 146fsumser 12524 . . . . . . . . 9
148147, 30eqeltrd 2510 . . . . . . . 8
149140, 141, 148ltadd2d 9226 . . . . . . 7
1501, 127, 102, 134, 136, 133isumsplit 12620 . . . . . . . . 9
151 nncn 10008 . . . . . . . . . . . . . 14
152151adantl 453 . . . . . . . . . . . . 13
153 ax-1cn 9048 . . . . . . . . . . . . 13
154 pncan 9311 . . . . . . . . . . . . 13
155152, 153, 154sylancl 644 . . . . . . . . . . . 12
156155oveq2d 6097 . . . . . . . . . . 11
157156sumeq1d 12495 . . . . . . . . . 10
158157oveq1d 6096 . . . . . . . . 9
159150, 158eqtrd 2468 . . . . . . . 8
160159breq1d 4222 . . . . . . 7
161149, 160bitr4d 248 . . . . . 6
162 eqid 2436 . . . . . . . . . 10
1631, 162, 26, 46, 47, 58, 66isumsup 12627 . . . . . . . . 9
164163, 74eqeltrd 2510 . . . . . . . 8
165164adantr 452 . . . . . . 7
166165, 141, 148ltsubaddd 9622 . . . . . 6
167163adantr 452 . . . . . . . 8
168167oveq1d 6096 . . . . . . 7
169168, 147breq12d 4225 . . . . . 6
170161, 166, 1693bitr2d 273 . . . . 5
171 2cn 10070 . . . . . . . . . . . . 13
172171a1i 11 . . . . . . . . . . . 12
173153a1i 11 . . . . . . . . . . . 12
174172, 152, 173adddid 9112 . . . . . . . . . . 11
175102nncnd 10016 . . . . . . . . . . . 12
176 mulcom 9076 . . . . . . . . . . . 12
177175, 171, 176sylancl 644 . . . . . . . . . . 11
17894nncnd 10016 . . . . . . . . . . . . 13
179178, 173, 173addassd 9110 . . . . . . . . . . . 12
1801532timesi 10101 . . . . . . . . . . . . 13
181180oveq2i 6092 . . . . . . . . . . . 12
182179, 181syl6eqr 2486 . . . . . . . . . . 11
183174, 177, 1823eqtr4d 2478 . . . . . . . . . 10
184183oveq2d 6097 . . . . . . . . 9
185 2nn0 10238 . . . . . . . . . . 11
186185a1i 11 . . . . . . . . . 10
187172, 186, 103expmuld 11526 . . . . . . . . 9
188 expp1 11388 . . . . . . . . . 10
189171, 96, 188sylancr 645 . . . . . . . . 9
190184, 187, 1893eqtr3d 2476 . . . . . . . 8
191190oveq1d 6096 . . . . . . 7
192 expcl 11399 . . . . . . . . 9
193171, 96, 192sylancr 645 . . . . . . . 8
194 2ne0 10083 . . . . . . . . 9
195 divcan4 9703 . . . . . . . . 9
196171, 194, 195mp3an23 1271 . . . . . . . 8
197193, 196syl 16 . . . . . . 7
198191, 197eqtrd 2468 . . . . . 6
199 nnnn0 10228 . . . . . . . . 9
200199adantl 453 . . . . . . . 8
201172, 103, 200expaddd 11525 . . . . . . 7
2021522timesd 10210 . . . . . . . . . 10
203202oveq1d 6096 . . . . . . . . 9
204152, 152, 173addassd 9110 . . . . . . . . 9
205203, 204eqtrd 2468 . . . . . . . 8
206205oveq2d 6097 . . . . . . 7
207105nnrpd 10647 . . . . . . . . . 10
208207rprege0d 10655 . . . . . . . . 9
209 sqrsq 12075 . . . . . . . . 9
210208, 209syl 16 . . . . . . . 8
211210oveq2d 6097 . . . . . . 7
212201, 206, 2113eqtr4rd 2479 . . . . . 6
213198, 212breq12d 4225 . . . . 5
214126, 170, 2133imtr3d 259 . . . 4
21599, 214mtod 170 . . 3
216215nrexdv 2809 . 2
21790, 216pm2.65i 167 1
 Colors of variables: wff set class Syntax hints:   wn 3   wb 177   wa 359   wtru 1325   wceq 1652   wcel 1725   wne 2599  wral 2705  wrex 2706  crab 2709   cdif 3317   wss 3320  c0 3628  cif 3739   class class class wbr 4212   cmpt 4266   cdm 4878   crn 4879   wfn 5449  wf 5450  cfv 5454  (class class class)co 6081  csup 7445  cc 8988  cr 8989  cc0 8990  c1 8991   caddc 8993   cmul 8995   clt 9120   cle 9121   cmin 9291   cdiv 9677  cn 10000  c2 10049  cn0 10221  cz 10282  cuz 10488  crp 10612  cfz 11043   cseq 11323  cexp 11382  csqr 12038   cli 12278  csu 12479   cdivides 12852  cprime 13079 This theorem is referenced by:  prmrec  13290 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-inf2 7596  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067  ax-pre-sup 9068 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-se 4542  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-isom 5463  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-2o 6725  df-oadd 6728  df-er 6905  df-map 7020  df-pm 7021  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-sup 7446  df-oi 7479  df-card 7826  df-cda 8048  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-div 9678  df-nn 10001  df-2 10058  df-3 10059  df-n0 10222  df-z 10283  df-uz 10489  df-q 10575  df-rp 10613  df-fz 11044  df-fzo 11136  df-fl 11202  df-mod 11251  df-seq 11324  df-exp 11383  df-hash 11619  df-cj 11904  df-re 11905  df-im 11906  df-sqr 12040  df-abs 12041  df-clim 12282  df-rlim 12283  df-sum 12480  df-dvds 12853  df-gcd 13007  df-prm 13080  df-pc 13211
 Copyright terms: Public domain W3C validator