Step Hyp Ref
Expression 1 eftl.5 . . . 4
2 eftl.4 . . . . 5
3 2 nnnn0d 10877 . . . 4
4 eftl.1 . . . . 5
5 4 eftlcl 13842 . . . 4
6 1 , 3 , 5 syl2anc 661 . . 3
7 6 abscld 13267 . 2
8 1 abscld 13267 . . 3
9 eftl.2 . . . 4
10 9 reeftlcl 13843 . . 3
11 8 , 3 , 10 syl2anc 661 . 2
12 8 , 3 reexpcld 12327 . . 3
13 peano2nn0 10861 . . . . . 6
14 3 , 13 syl 16 . . . . 5
15 14 nn0red 10878 . . . 4
16 faccl 12363 . . . . . 6
17 3 , 16 syl 16 . . . . 5
18 17 , 2 nnmulcld 10608 . . . 4
19 15 , 18 nndivred 10609 . . 3
20 12 , 19 remulcld 9645 . 2
21 eqid 2457 . . 3
22 2 nnzd 10993 . . . 4
23 eqidd 2458 . . . 4
24 eluznn0 11180 . . . . . 6
25 3 , 24 sylan 471 . . . . 5
26 4 eftval 13812 . . . . . . 7
27 26 adantl 466 . . . . . 6
28 eftcl 13809 . . . . . . 7
29 1 , 28 sylan 471 . . . . . 6
30 27 , 29 eqeltrd 2545 . . . . 5
31 25 , 30 syldan 470 . . . 4
32 4 eftlcvg 13841 . . . . 5
33 1 , 3 , 32 syl2anc 661 . . . 4
34 21 , 22 , 23 , 31 , 33 isumclim2 13573 . . 3
35 eqidd 2458 . . . 4
36 9 eftval 13812 . . . . . . . 8
37 36 adantl 466 . . . . . . 7
38 reeftcl 13810 . . . . . . . 8
39 8 , 38 sylan 471 . . . . . . 7
40 37 , 39 eqeltrd 2545 . . . . . 6
41 25 , 40 syldan 470 . . . . 5
42 41 recnd 9643 . . . 4
43 8 recnd 9643 . . . . 5
44 9 eftlcvg 13841 . . . . 5
45 43 , 3 , 44 syl2anc 661 . . . 4
46 21 , 22 , 35 , 42 , 45 isumclim2 13573 . . 3
47 eftabs 13811 . . . . . 6
48 1 , 47 sylan 471 . . . . 5
49 27 fveq2d 5875 . . . . 5
50 48 , 49 , 37 3eqtr4rd 2509 . . . 4
51 25 , 50 syldan 470 . . 3
52 21 , 34 , 46 , 22 , 31 , 51 iserabs 13629 . 2
53 nn0uz 11144 . . . 4
54 0zd 10901 . . . 4
55 2 nncnd 10577 . . . . 5
56 nn0cn 10830 . . . . 5
57 nn0ex 10826 . . . . . . . 8
58 57 mptex 6143 . . . . . . 7
59 9 , 58 eqeltri 2541 . . . . . 6
60 59 shftval4 12910 . . . . 5
61 55 , 56 , 60 syl2an 477 . . . 4
62 nn0addcl 10856 . . . . . . 7
63 3 , 62 sylan 471 . . . . . 6
64 9 eftval 13812 . . . . . 6
65 63 , 64 syl 16 . . . . 5
66 8 adantr 465 . . . . . 6
67 reeftcl 13810 . . . . . 6
68 66 , 63 , 67 syl2anc 661 . . . . 5
69 65 , 68 eqeltrd 2545 . . . 4
70 oveq2 6304 . . . . . . 7
71 70 oveq2d 6312 . . . . . 6
72 eftl.3 . . . . . 6
73 ovex 6324 . . . . . 6
74 71 , 72 , 73 fvmpt 5956 . . . . 5
75 74 adantl 466 . . . 4
76 12 , 17 nndivred 10609 . . . . . 6
77 76 adantr 465 . . . . 5
78 2 peano2nnd 10578 . . . . . . 7
79 78 nnrecred 10606 . . . . . 6
80 reexpcl 12183 . . . . . 6
81 79 , 80 sylan 471 . . . . 5
82 77 , 81 remulcld 9645 . . . 4
83 66 , 63 reexpcld 12327 . . . . . . 7
84 12 adantr 465 . . . . . . 7
85 faccl 12363 . . . . . . . . . 10
86 63 , 85 syl 16 . . . . . . . . 9
87 86 nnred 10576 . . . . . . . 8
88 87 , 82 remulcld 9645 . . . . . . 7
89 3 adantr 465 . . . . . . . 8
90 uzid 11124 . . . . . . . . . 10
91 22 , 90 syl 16 . . . . . . . . 9
92 uzaddcl 11166 . . . . . . . . 9
93 91 , 92 sylan 471 . . . . . . . 8
94 1 absge0d 13275 . . . . . . . . 9
95 94 adantr 465 . . . . . . . 8
96 eftl.6 . . . . . . . . 9
97 96 adantr 465 . . . . . . . 8
98 66 , 89 , 93 , 95 , 97 leexp2rd 12343 . . . . . . 7
99 17 adantr 465 . . . . . . . . . . . 12
100 nnexpcl 12179 . . . . . . . . . . . . 13
101 78 , 100 sylan 471 . . . . . . . . . . . 12
102 99 , 101 nnmulcld 10608 . . . . . . . . . . 11
103 102 nnred 10576 . . . . . . . . . 10
104 8 , 3 , 94 expge0d 12328 . . . . . . . . . . . 12
105 12 , 104 jca 532 . . . . . . . . . . 11
106 105 adantr 465 . . . . . . . . . 10
107 faclbnd6 12377 . . . . . . . . . . 11
108 3 , 107 sylan 471 . . . . . . . . . 10
109 lemul1a 10421 . . . . . . . . . 10
110 103 , 87 , 106 , 108 , 109 syl31anc 1231 . . . . . . . . 9
111 87 , 84 remulcld 9645 . . . . . . . . . 10
112 102 nnrpd 11284 . . . . . . . . . 10
113 84 , 111 , 112 lemuldiv2d 11331 . . . . . . . . 9
114 110 , 113 mpbid 210 . . . . . . . 8
115 86 nncnd 10577 . . . . . . . . . 10
116 12 recnd 9643 . . . . . . . . . . 11
117 116 adantr 465 . . . . . . . . . 10
118 102 nncnd 10577 . . . . . . . . . 10
119 102 nnne0d 10605 . . . . . . . . . 10
120 115 , 117 ,
118 , 119 divassd 10380 . . . . . . . . 9
121 78 nncnd 10577 . . . . . . . . . . . . . 14
122 121 adantr 465 . . . . . . . . . . . . 13
123 78 adantr 465 . . . . . . . . . . . . . 14
124 123 nnne0d 10605 . . . . . . . . . . . . 13
125 nn0z 10912 . . . . . . . . . . . . . 14
126 125 adantl 466 . . . . . . . . . . . . 13
127 122 , 124 ,
126 exprecd 12318 . . . . . . . . . . . 12
128 127 oveq2d 6312 . . . . . . . . . . 11
129 76 recnd 9643 . . . . . . . . . . . . 13
130 129 adantr 465 . . . . . . . . . . . 12
131 101 nncnd 10577 . . . . . . . . . . . 12
132 101 nnne0d 10605 . . . . . . . . . . . 12
133 130 , 131 ,
132 divrecd 10348 . . . . . . . . . . 11
134 17 nncnd 10577 . . . . . . . . . . . . 13
135 134 adantr 465 . . . . . . . . . . . 12
136 facne0 12364 . . . . . . . . . . . . . 14
137 3 , 136 syl 16 . . . . . . . . . . . . 13
138 137 adantr 465 . . . . . . . . . . . 12
139 117 , 135 ,
131 , 138 , 132 divdiv1d 10376 . . . . . . . . . . 11
140 128 , 133 ,
139 3eqtr2rd 2505 . . . . . . . . . 10
141 140 oveq2d 6312 . . . . . . . . 9
142 120 , 141 eqtrd 2498 . . . . . . . 8
143 114 , 142 breqtrd 4476 . . . . . . 7
144 83 , 84 , 88 , 98 , 143 letrd 9760 . . . . . 6
145 86 nngt0d 10604 . . . . . . 7
146 ledivmul 10443 . . . . . . 7
147 83 , 82 , 87 , 145 , 146 syl112anc 1232 . . . . . 6
148 144 , 147 mpbird 232 . . . . 5
149 65 , 148 eqbrtrd 4472 . . . 4
150 0z 10900 . . . . . 6
151 22 znegcld 10996 . . . . . 6
152 59 seqshft 12918 . . . . . 6
153 150 , 151 ,
152 sylancr 663 . . . . 5
154 0cn 9609 . . . . . . . . . . . 12
155 subneg 9891 . . . . . . . . . . . 12
156 154 , 155 mpan 670 . . . . . . . . . . 11
157 addid2 9784 . . . . . . . . . . 11
158 156 , 157 eqtrd 2498 . . . . . . . . . 10
159 55 , 158 syl 16 . . . . . . . . 9
160 159 seqeq1d 12113 . . . . . . . 8
161 160 , 46 eqbrtrd 4472 . . . . . . 7
162 seqex 12109 . . . . . . . 8
163 climshft 13399 . . . . . . . 8
164 151 , 162 ,
163 sylancl 662 . . . . . . 7
165 161 , 164 mpbird 232 . . . . . 6
166 ovex 6324 . . . . . . 7
167 sumex 13510 . . . . . . 7
168 166 , 167 breldm 5212 . . . . . 6
169 165 , 168 syl 16 . . . . 5
170 153 , 169 eqeltrd 2545 . . . 4
171 2 nnge1d 10603 . . . . . . . . . 10
172 1nn 10572 . . . . . . . . . . 11
173 nnleltp1 10943 . . . . . . . . . . 11
174 172 , 2 , 173 sylancr 663 . . . . . . . . . 10
175 171 , 174 mpbid 210 . . . . . . . . 9
176 14 nn0ge0d 10880 . . . . . . . . . 10
177 15 , 176 absidd 13254 . . . . . . . . 9
178 175 , 177 breqtrrd 4478 . . . . . . . 8
179 eqid 2457 . . . . . . . . . 10
180 ovex 6324 . . . . . . . . . 10
181 70 , 179 , 180 fvmpt 5956 . . . . . . . . 9
182 181 adantl 466 . . . . . . . 8
183 121 , 178 ,
182 georeclim 13681 . . . . . . 7
184 81 recnd 9643 . . . . . . . 8
185 182 , 184 eqeltrd 2545 . . . . . . 7
186 182 oveq2d 6312 . . . . . . . 8
187 75 , 186 eqtr4d 2501 . . . . . . 7
188 53 , 54 , 129 , 183 , 185 , 187 isermulc2 13480 . . . . . 6
189 ax-1cn 9571 . . . . . . . . . . 11
190 pncan 9849 . . . . . . . . . . 11
191 55 , 189 , 190 sylancl 662 . . . . . . . . . 10
192 191 oveq2d 6312 . . . . . . . . 9
193 192 oveq2d 6312 . . . . . . . 8
194 15 , 2 nndivred 10609 . . . . . . . . . 10
195 194 recnd 9643 . . . . . . . . 9
196 116 , 195 ,
134 , 137 div23d 10382 . . . . . . . 8
197 193 , 196 eqtr4d 2501 . . . . . . 7
198 116 , 195 ,
134 , 137 divassd 10380 . . . . . . 7
199 2 nnne0d 10605 . . . . . . . . . 10
200 121 , 55 , 134 , 199 , 137 divdiv1d 10376 . . . . . . . . 9
201 55 , 134 mulcomd 9638 . . . . . . . . . 10
202 201 oveq2d 6312 . . . . . . . . 9
203 200 , 202 eqtrd 2498 . . . . . . . 8
204 203 oveq2d 6312 . . . . . . 7
205 197 , 198 ,
204 3eqtrd 2502 . . . . . 6
206 188 , 205 breqtrd 4476 . . . . 5
207 seqex 12109 . . . . . 6
208 ovex 6324 . . . . . 6
209 207 , 208 breldm 5212 . . . . 5
210 206 , 209 syl 16 . . . 4
211 53 , 54 , 61 , 69 , 75 , 82 , 149 , 170 , 210 isumle 13656 . . 3
212 eqid 2457 . . . . 5
213 fveq2 5871 . . . . 5
214 55 addid2d 9802 . . . . . . . . 9
215 214 fveq2d 5875 . . . . . . . 8
216 215 eleq2d 2527 . . . . . . 7
217 216 biimpa 484 . . . . . 6
218 217 , 42 syldan 470 . . . . 5
219 53 , 212 , 213 , 22 , 54 , 218 isumshft 13651 . . . 4
220 215 sumeq1d 13523 . . . 4
221 219 , 220 eqtr3d 2500 . . 3
222 82 recnd 9643 . . . 4
223 53 , 54 , 75 , 222 , 206 isumclim 13572 . . 3
224 211 , 221 ,
223 3brtr3d 4481 . 2
225 7 , 11 , 20 , 52 , 224 letrd 9760 1
