Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . . 5
|
2 | | 1zzd 11408 |
. . . . 5
|
3 | | 1zzd 11408 |
. . . . . . 7
|
4 | | nnnn0 11299 |
. . . . . . . 8
|
5 | | climcnds.4 |
. . . . . . . . 9
|
6 | | 2nn 11185 |
. . . . . . . . . . . 12
|
7 | | simpr 477 |
. . . . . . . . . . . 12
|
8 | | nnexpcl 12873 |
. . . . . . . . . . . 12
|
9 | 6, 7, 8 | sylancr 695 |
. . . . . . . . . . 11
|
10 | 9 | nnred 11035 |
. . . . . . . . . 10
|
11 | | climcnds.1 |
. . . . . . . . . . . . 13
|
12 | 11 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
13 | 12 | adantr 481 |
. . . . . . . . . . 11
|
14 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
15 | 14 | eleq1d 2686 |
. . . . . . . . . . . 12
|
16 | 15 | rspcv 3305 |
. . . . . . . . . . 11
|
17 | 9, 13, 16 | sylc 65 |
. . . . . . . . . 10
|
18 | 10, 17 | remulcld 10070 |
. . . . . . . . 9
|
19 | 5, 18 | eqeltrd 2701 |
. . . . . . . 8
|
20 | 4, 19 | sylan2 491 |
. . . . . . 7
|
21 | 1, 3, 20 | serfre 12830 |
. . . . . 6
|
22 | 21 | adantr 481 |
. . . . 5
|
23 | | simpr 477 |
. . . . . . . 8
|
24 | 23, 1 | syl6eleq 2711 |
. . . . . . 7
|
25 | | nnz 11399 |
. . . . . . . . 9
|
26 | 25 | adantl 482 |
. . . . . . . 8
|
27 | | uzid 11702 |
. . . . . . . 8
|
28 | | peano2uz 11741 |
. . . . . . . 8
|
29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
|
30 | | simpl 473 |
. . . . . . . 8
|
31 | | elfznn 12370 |
. . . . . . . 8
|
32 | 30, 31, 20 | syl2an 494 |
. . . . . . 7
|
33 | | simpll 790 |
. . . . . . . 8
|
34 | | elfz1eq 12352 |
. . . . . . . . . 10
|
35 | 34 | adantl 482 |
. . . . . . . . 9
|
36 | | nnnn0 11299 |
. . . . . . . . . . 11
|
37 | | peano2nn0 11333 |
. . . . . . . . . . 11
|
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
|
39 | 38 | ad2antlr 763 |
. . . . . . . . 9
|
40 | 35, 39 | eqeltrd 2701 |
. . . . . . . 8
|
41 | 9 | nnnn0d 11351 |
. . . . . . . . . . 11
|
42 | 41 | nn0ge0d 11354 |
. . . . . . . . . 10
|
43 | | climcnds.2 |
. . . . . . . . . . . . 13
|
44 | 43 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
45 | 44 | adantr 481 |
. . . . . . . . . . 11
|
46 | 14 | breq2d 4665 |
. . . . . . . . . . . 12
|
47 | 46 | rspcv 3305 |
. . . . . . . . . . 11
|
48 | 9, 45, 47 | sylc 65 |
. . . . . . . . . 10
|
49 | 10, 17, 42, 48 | mulge0d 10604 |
. . . . . . . . 9
|
50 | 49, 5 | breqtrrd 4681 |
. . . . . . . 8
|
51 | 33, 40, 50 | syl2anc 693 |
. . . . . . 7
|
52 | 24, 29, 32, 51 | sermono 12833 |
. . . . . 6
|
53 | 52 | adantlr 751 |
. . . . 5
|
54 | | 2re 11090 |
. . . . . . 7
|
55 | | eqidd 2623 |
. . . . . . . 8
|
56 | 11 | adantlr 751 |
. . . . . . . 8
|
57 | | simpr 477 |
. . . . . . . 8
|
58 | 1, 2, 55, 56, 57 | isumrecl 14496 |
. . . . . . 7
|
59 | | remulcl 10021 |
. . . . . . 7
|
60 | 54, 58, 59 | sylancr 695 |
. . . . . 6
|
61 | 22 | ffvelrnda 6359 |
. . . . . . . 8
|
62 | 1, 3, 11 | serfre 12830 |
. . . . . . . . . . 11
|
63 | 62 | ad2antrr 762 |
. . . . . . . . . 10
|
64 | 36 | adantl 482 |
. . . . . . . . . . 11
|
65 | | nnexpcl 12873 |
. . . . . . . . . . 11
|
66 | 6, 64, 65 | sylancr 695 |
. . . . . . . . . 10
|
67 | 63, 66 | ffvelrnd 6360 |
. . . . . . . . 9
|
68 | | remulcl 10021 |
. . . . . . . . 9
|
69 | 54, 67, 68 | sylancr 695 |
. . . . . . . 8
|
70 | 60 | adantr 481 |
. . . . . . . 8
|
71 | | climcnds.3 |
. . . . . . . . . 10
|
72 | 11, 43, 71, 5 | climcndslem2 14582 |
. . . . . . . . 9
|
73 | 72 | adantlr 751 |
. . . . . . . 8
|
74 | | eqidd 2623 |
. . . . . . . . . . 11
|
75 | 66, 1 | syl6eleq 2711 |
. . . . . . . . . . 11
|
76 | | simpll 790 |
. . . . . . . . . . . 12
|
77 | | elfznn 12370 |
. . . . . . . . . . . 12
|
78 | 11 | recnd 10068 |
. . . . . . . . . . . 12
|
79 | 76, 77, 78 | syl2an 494 |
. . . . . . . . . . 11
|
80 | 74, 75, 79 | fsumser 14461 |
. . . . . . . . . 10
|
81 | | 1zzd 11408 |
. . . . . . . . . . 11
|
82 | | fzfid 12772 |
. . . . . . . . . . 11
|
83 | 77 | ssriv 3607 |
. . . . . . . . . . . 12
|
84 | 83 | a1i 11 |
. . . . . . . . . . 11
|
85 | | eqidd 2623 |
. . . . . . . . . . 11
|
86 | 56 | adantlr 751 |
. . . . . . . . . . 11
|
87 | 76, 43 | sylan 488 |
. . . . . . . . . . 11
|
88 | | simplr 792 |
. . . . . . . . . . 11
|
89 | 1, 81, 82, 84, 85, 86, 87, 88 | isumless 14577 |
. . . . . . . . . 10
|
90 | 80, 89 | eqbrtrrd 4677 |
. . . . . . . . 9
|
91 | 58 | adantr 481 |
. . . . . . . . . 10
|
92 | 54 | a1i 11 |
. . . . . . . . . 10
|
93 | | 2pos 11112 |
. . . . . . . . . . 11
|
94 | 93 | a1i 11 |
. . . . . . . . . 10
|
95 | | lemul2 10876 |
. . . . . . . . . 10
|
96 | 67, 91, 92, 94, 95 | syl112anc 1330 |
. . . . . . . . 9
|
97 | 90, 96 | mpbid 222 |
. . . . . . . 8
|
98 | 61, 69, 70, 73, 97 | letrd 10194 |
. . . . . . 7
|
99 | 98 | ralrimiva 2966 |
. . . . . 6
|
100 | | breq2 4657 |
. . . . . . . 8
|
101 | 100 | ralbidv 2986 |
. . . . . . 7
|
102 | 101 | rspcev 3309 |
. . . . . 6
|
103 | 60, 99, 102 | syl2anc 693 |
. . . . 5
|
104 | 1, 2, 22, 53, 103 | climsup 14400 |
. . . 4
|
105 | | climrel 14223 |
. . . . 5
|
106 | 105 | releldmi 5362 |
. . . 4
|
107 | 104, 106 | syl 17 |
. . 3
|
108 | | nn0uz 11722 |
. . . . 5
|
109 | | 1nn0 11308 |
. . . . . 6
|
110 | 109 | a1i 11 |
. . . . 5
|
111 | 19 | recnd 10068 |
. . . . 5
|
112 | 108, 110,
111 | iserex 14387 |
. . . 4
|
113 | 112 | biimpar 502 |
. . 3
|
114 | 107, 113 | syldan 487 |
. 2
|
115 | | 1zzd 11408 |
. . . 4
|
116 | 62 | adantr 481 |
. . . 4
|
117 | | elfznn 12370 |
. . . . . . 7
|
118 | 30, 117, 11 | syl2an 494 |
. . . . . 6
|
119 | | simpll 790 |
. . . . . . 7
|
120 | | peano2nn 11032 |
. . . . . . . . 9
|
121 | 120 | adantl 482 |
. . . . . . . 8
|
122 | | elfz1eq 12352 |
. . . . . . . 8
|
123 | | eleq1 2689 |
. . . . . . . . 9
|
124 | 123 | biimparc 504 |
. . . . . . . 8
|
125 | 121, 122,
124 | syl2an 494 |
. . . . . . 7
|
126 | 119, 125,
43 | syl2anc 693 |
. . . . . 6
|
127 | 24, 29, 118, 126 | sermono 12833 |
. . . . 5
|
128 | 127 | adantlr 751 |
. . . 4
|
129 | | 0zd 11389 |
. . . . . 6
|
130 | | eqidd 2623 |
. . . . . 6
|
131 | 19 | adantlr 751 |
. . . . . 6
|
132 | | simpr 477 |
. . . . . 6
|
133 | 108, 129,
130, 131, 132 | isumrecl 14496 |
. . . . 5
|
134 | 116 | ffvelrnda 6359 |
. . . . . . 7
|
135 | | 0zd 11389 |
. . . . . . . . . 10
|
136 | 108, 135,
19 | serfre 12830 |
. . . . . . . . 9
|
137 | 136 | adantr 481 |
. . . . . . . 8
|
138 | | ffvelrn 6357 |
. . . . . . . 8
|
139 | 137, 36, 138 | syl2an 494 |
. . . . . . 7
|
140 | 133 | adantr 481 |
. . . . . . 7
|
141 | 116 | adantr 481 |
. . . . . . . . 9
|
142 | | simpr 477 |
. . . . . . . . . 10
|
143 | 25 | adantl 482 |
. . . . . . . . . . 11
|
144 | 38 | adantl 482 |
. . . . . . . . . . . . . 14
|
145 | 144 | nn0red 11352 |
. . . . . . . . . . . . 13
|
146 | | nnexpcl 12873 |
. . . . . . . . . . . . . . 15
|
147 | 6, 144, 146 | sylancr 695 |
. . . . . . . . . . . . . 14
|
148 | 147 | nnred 11035 |
. . . . . . . . . . . . 13
|
149 | | 2z 11409 |
. . . . . . . . . . . . . . 15
|
150 | | uzid 11702 |
. . . . . . . . . . . . . . 15
|
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
152 | | bernneq3 12992 |
. . . . . . . . . . . . . 14
|
153 | 151, 144,
152 | sylancr 695 |
. . . . . . . . . . . . 13
|
154 | 145, 148,
153 | ltled 10185 |
. . . . . . . . . . . 12
|
155 | 143 | peano2zd 11485 |
. . . . . . . . . . . . 13
|
156 | 147 | nnzd 11481 |
. . . . . . . . . . . . 13
|
157 | | eluz 11701 |
. . . . . . . . . . . . 13
|
158 | 155, 156,
157 | syl2anc 693 |
. . . . . . . . . . . 12
|
159 | 154, 158 | mpbird 247 |
. . . . . . . . . . 11
|
160 | | eluzp1m1 11711 |
. . . . . . . . . . 11
|
161 | 143, 159,
160 | syl2anc 693 |
. . . . . . . . . 10
|
162 | | eluznn 11758 |
. . . . . . . . . 10
|
163 | 142, 161,
162 | syl2anc 693 |
. . . . . . . . 9
|
164 | 141, 163 | ffvelrnd 6360 |
. . . . . . . 8
|
165 | 24 | adantlr 751 |
. . . . . . . . 9
|
166 | | simpll 790 |
. . . . . . . . . 10
|
167 | | elfznn 12370 |
. . . . . . . . . 10
|
168 | 166, 167,
11 | syl2an 494 |
. . . . . . . . 9
|
169 | 166 | adantr 481 |
. . . . . . . . . 10
|
170 | 120 | adantl 482 |
. . . . . . . . . . 11
|
171 | | elfzuz 12338 |
. . . . . . . . . . 11
|
172 | | eluznn 11758 |
. . . . . . . . . . 11
|
173 | 170, 171,
172 | syl2an 494 |
. . . . . . . . . 10
|
174 | 169, 173,
43 | syl2anc 693 |
. . . . . . . . 9
|
175 | 165, 161,
168, 174 | sermono 12833 |
. . . . . . . 8
|
176 | 36 | adantl 482 |
. . . . . . . . 9
|
177 | 11, 43, 71, 5 | climcndslem1 14581 |
. . . . . . . . 9
|
178 | 166, 176,
177 | syl2anc 693 |
. . . . . . . 8
|
179 | 134, 164,
139, 175, 178 | letrd 10194 |
. . . . . . 7
|
180 | | eqidd 2623 |
. . . . . . . . 9
|
181 | 176, 108 | syl6eleq 2711 |
. . . . . . . . 9
|
182 | | elfznn0 12433 |
. . . . . . . . . 10
|
183 | 166, 182,
111 | syl2an 494 |
. . . . . . . . 9
|
184 | 180, 181,
183 | fsumser 14461 |
. . . . . . . 8
|
185 | | 0zd 11389 |
. . . . . . . . 9
|
186 | | fzfid 12772 |
. . . . . . . . 9
|
187 | 182 | ssriv 3607 |
. . . . . . . . . 10
|
188 | 187 | a1i 11 |
. . . . . . . . 9
|
189 | | eqidd 2623 |
. . . . . . . . 9
|
190 | 166, 19 | sylan 488 |
. . . . . . . . 9
|
191 | 166, 50 | sylan 488 |
. . . . . . . . 9
|
192 | | simplr 792 |
. . . . . . . . 9
|
193 | 108, 185,
186, 188, 189, 190, 191, 192 | isumless 14577 |
. . . . . . . 8
|
194 | 184, 193 | eqbrtrrd 4677 |
. . . . . . 7
|
195 | 134, 139,
140, 179, 194 | letrd 10194 |
. . . . . 6
|
196 | 195 | ralrimiva 2966 |
. . . . 5
|
197 | | breq2 4657 |
. . . . . . 7
|
198 | 197 | ralbidv 2986 |
. . . . . 6
|
199 | 198 | rspcev 3309 |
. . . . 5
|
200 | 133, 196,
199 | syl2anc 693 |
. . . 4
|
201 | 1, 115, 116, 128, 200 | climsup 14400 |
. . 3
|
202 | 105 | releldmi 5362 |
. . 3
|
203 | 201, 202 | syl 17 |
. 2
|
204 | 114, 203 | impbida 877 |
1
|