Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . 3
|
2 | | 1zzd 11408 |
. . 3
|
3 | | oveq1 6657 |
. . . . 5
|
4 | | eqid 2622 |
. . . . 5
|
5 | | ovex 6678 |
. . . . 5
|
6 | 3, 4, 5 | fvmpt 6282 |
. . . 4
|
7 | 6 | adantl 482 |
. . 3
|
8 | | nnre 11027 |
. . . . . . . . 9
|
9 | | nnne0 11053 |
. . . . . . . . 9
|
10 | | 2z 11409 |
. . . . . . . . . . 11
|
11 | | znegcl 11412 |
. . . . . . . . . . 11
|
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
|
13 | 12 | a1i 11 |
. . . . . . . . 9
|
14 | 8, 9, 13 | reexpclzd 13034 |
. . . . . . . 8
|
15 | 14 | adantl 482 |
. . . . . . 7
|
16 | 15, 4 | fmptd 6385 |
. . . . . 6
|
17 | 16 | ffvelrnda 6359 |
. . . . 5
|
18 | 7, 17 | eqeltrrd 2702 |
. . . 4
|
19 | 18 | recnd 10068 |
. . 3
|
20 | 1, 2, 17 | serfre 12830 |
. . . . . . . . . . 11
|
21 | | basel.f |
. . . . . . . . . . . 12
|
22 | 21 | feq1i 6036 |
. . . . . . . . . . 11
|
23 | 20, 22 | sylibr 224 |
. . . . . . . . . 10
|
24 | 23 | ffvelrnda 6359 |
. . . . . . . . 9
|
25 | 24 | recnd 10068 |
. . . . . . . 8
|
26 | | remulcl 10021 |
. . . . . . . . . . . . 13
|
27 | 26 | adantl 482 |
. . . . . . . . . . . 12
|
28 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
29 | 28 | fconst 6091 |
. . . . . . . . . . . . . . 15
|
30 | | pire 24210 |
. . . . . . . . . . . . . . . . . . 19
|
31 | 30 | resqcli 12949 |
. . . . . . . . . . . . . . . . . 18
|
32 | | 6re 11101 |
. . . . . . . . . . . . . . . . . 18
|
33 | | 6nn 11189 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 33 | nnne0i 11055 |
. . . . . . . . . . . . . . . . . 18
|
35 | 31, 32, 34 | redivcli 10792 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
38 | | fss 6056 |
. . . . . . . . . . . . . . 15
|
39 | 29, 37, 38 | sylancr 695 |
. . . . . . . . . . . . . 14
|
40 | | resubcl 10345 |
. . . . . . . . . . . . . . . 16
|
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . 15
|
42 | | 1ex 10035 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | fconst 6091 |
. . . . . . . . . . . . . . . 16
|
44 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | snssd 4340 |
. . . . . . . . . . . . . . . 16
|
46 | | fss 6056 |
. . . . . . . . . . . . . . . 16
|
47 | 43, 45, 46 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
48 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
|
52 | 51 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . 17
|
53 | 52 | nnrecred 11066 |
. . . . . . . . . . . . . . . 16
|
54 | | basel.g |
. . . . . . . . . . . . . . . 16
|
55 | 53, 54 | fmptd 6385 |
. . . . . . . . . . . . . . 15
|
56 | | nnex 11026 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
|
58 | | inidm 3822 |
. . . . . . . . . . . . . . 15
|
59 | 41, 47, 55, 57, 57, 58 | off 6912 |
. . . . . . . . . . . . . 14
|
60 | 27, 39, 59, 57, 57, 58 | off 6912 |
. . . . . . . . . . . . 13
|
61 | | basel.h |
. . . . . . . . . . . . . 14
|
62 | 61 | feq1i 6036 |
. . . . . . . . . . . . 13
|
63 | 60, 62 | sylibr 224 |
. . . . . . . . . . . 12
|
64 | | readdcl 10019 |
. . . . . . . . . . . . . 14
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . 13
|
66 | | negex 10279 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | fconst 6091 |
. . . . . . . . . . . . . . 15
|
68 | 12 | zrei 11383 |
. . . . . . . . . . . . . . . . 17
|
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
71 | | fss 6056 |
. . . . . . . . . . . . . . 15
|
72 | 67, 70, 71 | sylancr 695 |
. . . . . . . . . . . . . 14
|
73 | 27, 72, 55, 57, 57, 58 | off 6912 |
. . . . . . . . . . . . 13
|
74 | 65, 47, 73, 57, 57, 58 | off 6912 |
. . . . . . . . . . . 12
|
75 | 27, 63, 74, 57, 57, 58 | off 6912 |
. . . . . . . . . . 11
|
76 | | basel.j |
. . . . . . . . . . . 12
|
77 | 76 | feq1i 6036 |
. . . . . . . . . . 11
|
78 | 75, 77 | sylibr 224 |
. . . . . . . . . 10
|
79 | 78 | ffvelrnda 6359 |
. . . . . . . . 9
|
80 | 79 | recnd 10068 |
. . . . . . . 8
|
81 | 25, 80 | npcand 10396 |
. . . . . . 7
|
82 | 81 | mpteq2dva 4744 |
. . . . . 6
|
83 | | ovexd 6680 |
. . . . . . 7
|
84 | 23 | feqmptd 6249 |
. . . . . . . 8
|
85 | 78 | feqmptd 6249 |
. . . . . . . 8
|
86 | 57, 24, 79, 84, 85 | offval2 6914 |
. . . . . . 7
|
87 | 57, 83, 79, 86, 85 | offval2 6914 |
. . . . . 6
|
88 | 82, 87, 84 | 3eqtr4d 2666 |
. . . . 5
|
89 | 65, 47, 55, 57, 57, 58 | off 6912 |
. . . . . . . . . 10
|
90 | | recn 10026 |
. . . . . . . . . . . 12
|
91 | | recn 10026 |
. . . . . . . . . . . 12
|
92 | | recn 10026 |
. . . . . . . . . . . 12
|
93 | | subdi 10463 |
. . . . . . . . . . . 12
|
94 | 90, 91, 92, 93 | syl3an 1368 |
. . . . . . . . . . 11
|
95 | 94 | adantl 482 |
. . . . . . . . . 10
|
96 | 57, 63, 89, 74, 95 | caofdi 6933 |
. . . . . . . . 9
|
97 | | basel.k |
. . . . . . . . . 10
|
98 | 97, 76 | oveq12i 6662 |
. . . . . . . . 9
|
99 | 96, 98 | syl6eqr 2674 |
. . . . . . . 8
|
100 | 35 | recni 10052 |
. . . . . . . . . . . . . 14
|
101 | 1 | eqimss2i 3660 |
. . . . . . . . . . . . . . 15
|
102 | 101, 56 | climconst2 14279 |
. . . . . . . . . . . . . 14
|
103 | 100, 2, 102 | sylancr 695 |
. . . . . . . . . . . . 13
|
104 | | ovexd 6680 |
. . . . . . . . . . . . 13
|
105 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . 16
|
106 | | fss 6056 |
. . . . . . . . . . . . . . . 16
|
107 | 47, 105, 106 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
108 | | fss 6056 |
. . . . . . . . . . . . . . . 16
|
109 | 55, 105, 108 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
110 | | ofnegsub 11018 |
. . . . . . . . . . . . . . 15
|
111 | 57, 107, 109, 110 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
112 | | neg1cn 11124 |
. . . . . . . . . . . . . . 15
|
113 | 54, 112 | basellem7 24813 |
. . . . . . . . . . . . . 14
|
114 | 111, 113 | syl6eqbrr 4693 |
. . . . . . . . . . . . 13
|
115 | 39 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
116 | 115 | recnd 10068 |
. . . . . . . . . . . . 13
|
117 | 59 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
118 | 117 | recnd 10068 |
. . . . . . . . . . . . 13
|
119 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
120 | 39, 119 | syl 17 |
. . . . . . . . . . . . . 14
|
121 | | fnconstg 6093 |
. . . . . . . . . . . . . . . 16
|
122 | 2, 121 | syl 17 |
. . . . . . . . . . . . . . 15
|
123 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
124 | 55, 123 | syl 17 |
. . . . . . . . . . . . . . 15
|
125 | 122, 124,
57, 57, 58 | offn 6908 |
. . . . . . . . . . . . . 14
|
126 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
127 | | eqidd 2623 |
. . . . . . . . . . . . . 14
|
128 | 120, 125,
57, 57, 58, 126, 127 | ofval 6906 |
. . . . . . . . . . . . 13
|
129 | 1, 2, 103, 104, 114, 116, 118, 128 | climmul 14363 |
. . . . . . . . . . . 12
|
130 | 100 | mulid1i 10042 |
. . . . . . . . . . . 12
|
131 | 129, 130 | syl6breq 4694 |
. . . . . . . . . . 11
|
132 | 61, 131 | syl5eqbr 4688 |
. . . . . . . . . 10
|
133 | | ovexd 6680 |
. . . . . . . . . 10
|
134 | | 3cn 11095 |
. . . . . . . . . . . . 13
|
135 | 101, 56 | climconst2 14279 |
. . . . . . . . . . . . 13
|
136 | 134, 2, 135 | sylancr 695 |
. . . . . . . . . . . 12
|
137 | | ovexd 6680 |
. . . . . . . . . . . 12
|
138 | 54 | basellem6 24812 |
. . . . . . . . . . . . 13
|
139 | 138 | a1i 11 |
. . . . . . . . . . . 12
|
140 | | 3ex 11096 |
. . . . . . . . . . . . . . . 16
|
141 | 140 | fconst 6091 |
. . . . . . . . . . . . . . 15
|
142 | | 3re 11094 |
. . . . . . . . . . . . . . . . 17
|
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
144 | 143 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
145 | | fss 6056 |
. . . . . . . . . . . . . . 15
|
146 | 141, 144,
145 | sylancr 695 |
. . . . . . . . . . . . . 14
|
147 | 146 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
148 | 147 | recnd 10068 |
. . . . . . . . . . . 12
|
149 | 55 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
150 | 149 | recnd 10068 |
. . . . . . . . . . . 12
|
151 | | ffn 6045 |
. . . . . . . . . . . . . 14
|
152 | 146, 151 | syl 17 |
. . . . . . . . . . . . 13
|
153 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
154 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
155 | 152, 124,
57, 57, 58, 153, 154 | ofval 6906 |
. . . . . . . . . . . 12
|
156 | 1, 2, 136, 137, 139, 148, 150, 155 | climmul 14363 |
. . . . . . . . . . 11
|
157 | 134 | mul01i 10226 |
. . . . . . . . . . 11
|
158 | 156, 157 | syl6breq 4694 |
. . . . . . . . . 10
|
159 | 63 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
160 | 159 | recnd 10068 |
. . . . . . . . . 10
|
161 | 27, 146, 55, 57, 57, 58 | off 6912 |
. . . . . . . . . . . 12
|
162 | 161 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
163 | 162 | recnd 10068 |
. . . . . . . . . 10
|
164 | | ffn 6045 |
. . . . . . . . . . . 12
|
165 | 63, 164 | syl 17 |
. . . . . . . . . . 11
|
166 | 41, 89, 74, 57, 57, 58 | off 6912 |
. . . . . . . . . . . 12
|
167 | | ffn 6045 |
. . . . . . . . . . . 12
|
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
|
169 | | eqidd 2623 |
. . . . . . . . . . 11
|
170 | 150 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
171 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . 18
|
172 | | mulneg1 10466 |
. . . . . . . . . . . . . . . . . 18
|
173 | 171, 150,
172 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
174 | 173 | negeqd 10275 |
. . . . . . . . . . . . . . . 16
|
175 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . 18
|
176 | 171, 150,
175 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
177 | 176 | negnegd 10383 |
. . . . . . . . . . . . . . . 16
|
178 | 174, 177 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
|
179 | 170, 178 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
180 | | remulcl 10021 |
. . . . . . . . . . . . . . . . 17
|
181 | 68, 149, 180 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
182 | 181 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
183 | 150, 182 | negsubd 10398 |
. . . . . . . . . . . . . 14
|
184 | 179, 183 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
185 | | df-3 11080 |
. . . . . . . . . . . . . . . 16
|
186 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
|
187 | 171, 186 | addcomi 10227 |
. . . . . . . . . . . . . . . 16
|
188 | 185, 187 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
189 | 188 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
190 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
191 | 171 | a1i 11 |
. . . . . . . . . . . . . . 15
|
192 | 190, 191,
150 | adddird 10065 |
. . . . . . . . . . . . . 14
|
193 | 189, 192 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
194 | 190, 150,
182 | pnpcand 10429 |
. . . . . . . . . . . . 13
|
195 | 184, 193,
194 | 3eqtr4rd 2667 |
. . . . . . . . . . . 12
|
196 | 122, 124,
57, 57, 58 | offn 6908 |
. . . . . . . . . . . . 13
|
197 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
198 | | fnconstg 6093 |
. . . . . . . . . . . . . . . 16
|
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . . 15
|
200 | 199, 124,
57, 57, 58 | offn 6908 |
. . . . . . . . . . . . . 14
|
201 | 122, 200,
57, 57, 58 | offn 6908 |
. . . . . . . . . . . . 13
|
202 | 57, 44, 124, 154 | ofc1 6920 |
. . . . . . . . . . . . 13
|
203 | 57, 69, 124, 154 | ofc1 6920 |
. . . . . . . . . . . . . 14
|
204 | 57, 44, 200, 203 | ofc1 6920 |
. . . . . . . . . . . . 13
|
205 | 196, 201,
57, 57, 58, 202, 204 | ofval 6906 |
. . . . . . . . . . . 12
|
206 | 57, 143, 124, 154 | ofc1 6920 |
. . . . . . . . . . . 12
|
207 | 195, 205,
206 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
208 | 165, 168,
57, 57, 58, 169, 207 | ofval 6906 |
. . . . . . . . . 10
|
209 | 1, 2, 132, 133, 158, 160, 163, 208 | climmul 14363 |
. . . . . . . . 9
|
210 | 100 | mul01i 10226 |
. . . . . . . . 9
|
211 | 209, 210 | syl6breq 4694 |
. . . . . . . 8
|
212 | 99, 211 | eqbrtrrd 4677 |
. . . . . . 7
|
213 | | ovexd 6680 |
. . . . . . 7
|
214 | 27, 63, 89, 57, 57, 58 | off 6912 |
. . . . . . . . . 10
|
215 | 97 | feq1i 6036 |
. . . . . . . . . 10
|
216 | 214, 215 | sylibr 224 |
. . . . . . . . 9
|
217 | 41, 216, 78, 57, 57, 58 | off 6912 |
. . . . . . . 8
|
218 | 217 | ffvelrnda 6359 |
. . . . . . 7
|
219 | 41, 23, 78, 57, 57, 58 | off 6912 |
. . . . . . . 8
|
220 | 219 | ffvelrnda 6359 |
. . . . . . 7
|
221 | 23 | ffvelrnda 6359 |
. . . . . . . . 9
|
222 | 216 | ffvelrnda 6359 |
. . . . . . . . 9
|
223 | 78 | ffvelrnda 6359 |
. . . . . . . . 9
|
224 | | eqid 2622 |
. . . . . . . . . . . 12
|
225 | 54, 21, 61, 76, 97, 224 | basellem8 24814 |
. . . . . . . . . . 11
|
226 | 225 | adantl 482 |
. . . . . . . . . 10
|
227 | 226 | simprd 479 |
. . . . . . . . 9
|
228 | 221, 222,
223, 227 | lesub1dd 10643 |
. . . . . . . 8
|
229 | | ffn 6045 |
. . . . . . . . . 10
|
230 | 23, 229 | syl 17 |
. . . . . . . . 9
|
231 | | ffn 6045 |
. . . . . . . . . 10
|
232 | 78, 231 | syl 17 |
. . . . . . . . 9
|
233 | | eqidd 2623 |
. . . . . . . . 9
|
234 | | eqidd 2623 |
. . . . . . . . 9
|
235 | 230, 232,
57, 57, 58, 233, 234 | ofval 6906 |
. . . . . . . 8
|
236 | | ffn 6045 |
. . . . . . . . . 10
|
237 | 216, 236 | syl 17 |
. . . . . . . . 9
|
238 | | eqidd 2623 |
. . . . . . . . 9
|
239 | 237, 232,
57, 57, 58, 238, 234 | ofval 6906 |
. . . . . . . 8
|
240 | 228, 235,
239 | 3brtr4d 4685 |
. . . . . . 7
|
241 | 226 | simpld 475 |
. . . . . . . . 9
|
242 | 221, 223 | subge0d 10617 |
. . . . . . . . 9
|
243 | 241, 242 | mpbird 247 |
. . . . . . . 8
|
244 | 243, 235 | breqtrrd 4681 |
. . . . . . 7
|
245 | 1, 2, 212, 213, 218, 220, 240, 244 | climsqz2 14372 |
. . . . . 6
|
246 | | ovexd 6680 |
. . . . . 6
|
247 | | ovexd 6680 |
. . . . . . . . 9
|
248 | 68 | recni 10052 |
. . . . . . . . . . 11
|
249 | 54, 248 | basellem7 24813 |
. . . . . . . . . 10
|
250 | 249 | a1i 11 |
. . . . . . . . 9
|
251 | 74 | ffvelrnda 6359 |
. . . . . . . . . 10
|
252 | 251 | recnd 10068 |
. . . . . . . . 9
|
253 | | eqidd 2623 |
. . . . . . . . . 10
|
254 | 165, 201,
57, 57, 58, 169, 253 | ofval 6906 |
. . . . . . . . 9
|
255 | 1, 2, 132, 247, 250, 160, 252, 254 | climmul 14363 |
. . . . . . . 8
|
256 | 255, 130 | syl6breq 4694 |
. . . . . . 7
|
257 | 76, 256 | syl5eqbr 4688 |
. . . . . 6
|
258 | 220 | recnd 10068 |
. . . . . 6
|
259 | 223 | recnd 10068 |
. . . . . 6
|
260 | | ffn 6045 |
. . . . . . . 8
|
261 | 219, 260 | syl 17 |
. . . . . . 7
|
262 | | eqidd 2623 |
. . . . . . 7
|
263 | 261, 232,
57, 57, 58, 262, 234 | ofval 6906 |
. . . . . 6
|
264 | 1, 2, 245, 246, 257, 258, 259, 263 | climadd 14362 |
. . . . 5
|
265 | 88, 264 | eqbrtrrd 4677 |
. . . 4
|
266 | 100 | addid2i 10224 |
. . . 4
|
267 | 265, 21, 266 | 3brtr3g 4686 |
. . 3
|
268 | 1, 2, 7, 19, 267 | isumclim 14488 |
. 2
|
269 | 268 | trud 1493 |
1
|