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

Theorem prmreclem6 14439
 Description: Lemma for prmrec 14440. 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 14438 to produce the contradictory bound N 2 (2 ) N, which is false for N=2 (2 2). (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 11145 . . . . . . . . 9
2 1zzd 10920 . . . . . . . . 9
3 nnrecre 10597 . . . . . . . . . . . . 13
43adantl 466 . . . . . . . . . . . 12
5 0re 9617 . . . . . . . . . . . 12
6 ifcl 3983 . . . . . . . . . . . 12
74, 5, 6sylancl 662 . . . . . . . . . . 11
8 prmrec.1 . . . . . . . . . . 11
97, 8fmptd 6055 . . . . . . . . . 10
109ffvelrnda 6031 . . . . . . . . 9
111, 2, 10serfre 12136 . . . . . . . 8
1211trud 1404 . . . . . . 7
13 frn 5742 . . . . . . 7
1412, 13mp1i 12 . . . . . 6
15 1nn 10572 . . . . . . . 8
1612fdmi 5741 . . . . . . . 8
1715, 16eleqtrri 2544 . . . . . . 7
18 ne0i 3790 . . . . . . . 8
19 dm0rn0 5224 . . . . . . . . 9
2019necon3bii 2725 . . . . . . . 8
2118, 20sylib 196 . . . . . . 7
2217, 21mp1i 12 . . . . . 6
23 1zzd 10920 . . . . . . . . 9
24 climdm 13377 . . . . . . . . . 10
2524biimpi 194 . . . . . . . . 9
2612a1i 11 . . . . . . . . . 10
2726ffvelrnda 6031 . . . . . . . . 9
281, 23, 25, 27climrecl 13406 . . . . . . . 8
29 simpr 461 . . . . . . . . . 10
3025adantr 465 . . . . . . . . . 10
31 eleq1 2529 . . . . . . . . . . . . . . 15
32 oveq2 6304 . . . . . . . . . . . . . . 15
3331, 32ifbieq1d 3964 . . . . . . . . . . . . . 14
34 prmnn 14220 . . . . . . . . . . . . . . . . . . 19
3534adantl 466 . . . . . . . . . . . . . . . . . 18
3635nnrecred 10606 . . . . . . . . . . . . . . . . 17
375a1i 11 . . . . . . . . . . . . . . . . 17
3836, 37ifclda 3973 . . . . . . . . . . . . . . . 16
3938trud 1404 . . . . . . . . . . . . . . 15
4039elexi 3119 . . . . . . . . . . . . . 14
4133, 8, 40fvmpt 5956 . . . . . . . . . . . . 13
4241adantl 466 . . . . . . . . . . . 12
4339a1i 11 . . . . . . . . . . . 12
4442, 43eqeltrd 2545 . . . . . . . . . . 11
4544adantlr 714 . . . . . . . . . 10
46 nnrp 11258 . . . . . . . . . . . . . . . 16
4746adantl 466 . . . . . . . . . . . . . . 15
4847rpreccld 11295 . . . . . . . . . . . . . 14
4948rpge0d 11289 . . . . . . . . . . . . 13
50 0le0 10650 . . . . . . . . . . . . 13
51 breq2 4456 . . . . . . . . . . . . . 14
52 breq2 4456 . . . . . . . . . . . . . 14
5351, 52ifboth 3977 . . . . . . . . . . . . 13
5449, 50, 53sylancl 662 . . . . . . . . . . . 12
5554, 42breqtrrd 4478 . . . . . . . . . . 11
5655adantlr 714 . . . . . . . . . 10
571, 29, 30, 45, 56climserle 13485 . . . . . . . . 9
5857ralrimiva 2871 . . . . . . . 8
59 breq2 4456 . . . . . . . . . 10
6059ralbidv 2896 . . . . . . . . 9
6160rspcev 3210 . . . . . . . 8
6228, 58, 61syl2anc 661 . . . . . . 7
63 ffn 5736 . . . . . . . . 9
64 breq1 4455 . . . . . . . . . 10
6564ralrn 6034 . . . . . . . . 9
6612, 63, 65mp2b 10 . . . . . . . 8
6766rexbii 2959 . . . . . . 7
6862, 67sylibr 212 . . . . . 6
69 suprcl 10528 . . . . . 6
7014, 22, 68, 69syl3anc 1228 . . . . 5
71 2rp 11254 . . . . . 6
72 rpreccl 11272 . . . . . 6
7371, 72ax-mp 5 . . . . 5
74 ltsubrp 11280 . . . . 5
7570, 73, 74sylancl 662 . . . 4
76 halfre 10779 . . . . . 6
77 resubcl 9906 . . . . . 6
7870, 76, 77sylancl 662 . . . . 5
79 suprlub 10530 . . . . 5
8014, 22, 68, 78, 79syl31anc 1231 . . . 4
8175, 80mpbid 210 . . 3
82 breq2 4456 . . . . 5
8382rexrn 6033 . . . 4
8412, 63, 83mp2b 10 . . 3
8581, 84sylib 196 . 2
86 2re 10630 . . . . . 6
87 2nn 10718 . . . . . . . . 9
88 nnmulcl 10584 . . . . . . . . 9
8987, 29, 88sylancr 663 . . . . . . . 8
9089peano2nnd 10578 . . . . . . 7
9190nnnn0d 10877 . . . . . 6
92 reexpcl 12183 . . . . . 6
9386, 91, 92sylancr 663 . . . . 5
9493ltnrd 9740 . . . 4
9529adantr 465 . . . . . . 7
96 peano2nn 10573 . . . . . . . . . . . 12
9796adantl 466 . . . . . . . . . . 11
9897nnnn0d 10877 . . . . . . . . . 10
99 nnexpcl 12179 . . . . . . . . . 10
10087, 98, 99sylancr 663 . . . . . . . . 9
101100nnsqcld 12330 . . . . . . . 8
102101adantr 465 . . . . . . 7
103 breq1 4455 . . . . . . . . . . 11
104103notbid 294 . . . . . . . . . 10
105104cbvralv 3084 . . . . . . . . 9
106 breq2 4456 . . . . . . . . . . 11
107106notbid 294 . . . . . . . . . 10
108107ralbidv 2896 . . . . . . . . 9
109105, 108syl5bb 257 . . . . . . . 8
110109cbvrabv 3108 . . . . . . 7
111 simpll 753 . . . . . . 7
112 eleq1 2529 . . . . . . . . . 10
113 oveq2 6304 . . . . . . . . . 10
114112, 113ifbieq1d 3964 . . . . . . . . 9
115114cbvsumv 13518 . . . . . . . 8
116 simpr 461 . . . . . . . 8
117115, 116syl5eqbr 4485 . . . . . . 7
118 eqid 2457 . . . . . . 7
1198, 95, 102, 110, 111, 117, 118prmreclem5 14438 . . . . . 6
120119ex 434 . . . . 5
121 eqid 2457 . . . . . . . . 9
12297nnzd 10993 . . . . . . . . 9
123 eluznn 11181 . . . . . . . . . . 11
12497, 123sylan 471 . . . . . . . . . 10
125124, 41syl 16 . . . . . . . . 9
12639a1i 11 . . . . . . . . 9
127 simpl 457 . . . . . . . . . 10
12841adantl 466 . . . . . . . . . . . 12
12939recni 9629 . . . . . . . . . . . . 13
130129a1i 11 . . . . . . . . . . . 12
131128, 130eqeltrd 2545 . . . . . . . . . . 11
1321, 97, 131iserex 13479 . . . . . . . . . 10
133127, 132mpbid 210 . . . . . . . . 9
134121, 122, 125, 126, 133isumrecl 13580 . . . . . . . 8
13576a1i 11 . . . . . . . 8
136 elfznn 11743 . . . . . . . . . . . 12
137136adantl 466 . . . . . . . . . . 11
138137, 41syl 16 . . . . . . . . . 10
13929, 1syl6eleq 2555 . . . . . . . . . 10
140129a1i 11 . . . . . . . . . 10
141138, 139, 140fsumser 13552 . . . . . . . . 9
142141, 27eqeltrd 2545 . . . . . . . 8
143134, 135, 142ltadd2d 9759 . . . . . . 7
1441, 121, 97, 128, 130, 127isumsplit 13652 . . . . . . . . 9
145 nncn 10569 . . . . . . . . . . . . . 14
146145adantl 466 . . . . . . . . . . . . 13
147 ax-1cn 9571 . . . . . . . . . . . . 13
148 pncan 9849 . . . . . . . . . . . . 13
149146, 147, 148sylancl 662 . . . . . . . . . . . 12
150149oveq2d 6312 . . . . . . . . . . 11
151150sumeq1d 13523 . . . . . . . . . 10
152151oveq1d 6311 . . . . . . . . 9
153144, 152eqtrd 2498 . . . . . . . 8
154153breq1d 4462 . . . . . . 7
155143, 154bitr4d 256 . . . . . 6
156 eqid 2457 . . . . . . . . . 10
1571, 156, 23, 42, 43, 54, 62isumsup 13659 . . . . . . . . 9
158157, 70eqeltrd 2545 . . . . . . . 8
159158adantr 465 . . . . . . 7
160159, 135, 142ltsubaddd 10173 . . . . . 6
161157adantr 465 . . . . . . . 8
162161oveq1d 6311 . . . . . . 7
163162, 141breq12d 4465 . . . . . 6
164155, 160, 1633bitr2d 281 . . . . 5
165 2cn 10631 . . . . . . . . . . . . 13
166165a1i 11 . . . . . . . . . . . 12
167147a1i 11 . . . . . . . . . . . 12
168166, 146, 167adddid 9641 . . . . . . . . . . 11
16997nncnd 10577 . . . . . . . . . . . 12
170 mulcom 9599 . . . . . . . . . . . 12
171169, 165, 170sylancl 662 . . . . . . . . . . 11
17289nncnd 10577 . . . . . . . . . . . . 13
173172, 167, 167addassd 9639 . . . . . . . . . . . 12
1741472timesi 10681 . . . . . . . . . . . . 13
175174oveq2i 6307 . . . . . . . . . . . 12
176173, 175syl6eqr 2516 . . . . . . . . . . 11
177168, 171, 1763eqtr4d 2508 . . . . . . . . . 10
178177oveq2d 6312 . . . . . . . . 9
179 2nn0 10837 . . . . . . . . . . 11
180179a1i 11 . . . . . . . . . 10
181166, 180, 98expmuld 12313 . . . . . . . . 9
182 expp1 12173 . . . . . . . . . 10
183165, 91, 182sylancr 663 . . . . . . . . 9