Step | Hyp | Ref
| Expression |
1 | | reex 10027 |
. . . . . 6
|
2 | | rpssre 11843 |
. . . . . 6
|
3 | 1, 2 | ssexi 4803 |
. . . . 5
|
4 | 3 | a1i 11 |
. . . 4
|
5 | | fzfid 12772 |
. . . . . . 7
|
6 | | elfznn 12370 |
. . . . . . . . . . 11
|
7 | 6 | adantl 482 |
. . . . . . . . . 10
|
8 | | vmacl 24844 |
. . . . . . . . . 10
Λ |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
Λ |
10 | 9, 7 | nndivred 11069 |
. . . . . . . 8
Λ |
11 | 10 | recnd 10068 |
. . . . . . 7
Λ |
12 | 5, 11 | fsumcl 14464 |
. . . . . 6
Λ |
13 | 12 | adantr 481 |
. . . . 5
Λ |
14 | | relogcl 24322 |
. . . . . . 7
|
15 | 14 | adantl 482 |
. . . . . 6
|
16 | 15 | recnd 10068 |
. . . . 5
|
17 | 13, 16 | subcld 10392 |
. . . 4
Λ |
18 | | 1re 10039 |
. . . . . . . . 9
|
19 | | rpvmasum.g |
. . . . . . . . . . . 12
DChr |
20 | | rpvmasum.z |
. . . . . . . . . . . 12
ℤ/nℤ |
21 | | rpvmasum.1 |
. . . . . . . . . . . 12
|
22 | | eqid 2622 |
. . . . . . . . . . . 12
|
23 | | rpvmasum.a |
. . . . . . . . . . . 12
|
24 | 19, 20, 21, 22, 23 | dchr1re 24988 |
. . . . . . . . . . 11
|
25 | 24 | adantr 481 |
. . . . . . . . . 10
|
26 | 23 | nnnn0d 11351 |
. . . . . . . . . . . 12
|
27 | | rpvmasum.l |
. . . . . . . . . . . . 13
RHom |
28 | 20, 22, 27 | znzrhfo 19896 |
. . . . . . . . . . . 12
|
29 | | fof 6115 |
. . . . . . . . . . . 12
|
30 | 26, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
|
31 | | elfzelz 12342 |
. . . . . . . . . . 11
|
32 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
33 | 30, 31, 32 | syl2an 494 |
. . . . . . . . . 10
|
34 | 25, 33 | ffvelrnd 6360 |
. . . . . . . . 9
|
35 | | resubcl 10345 |
. . . . . . . . 9
|
36 | 18, 34, 35 | sylancr 695 |
. . . . . . . 8
|
37 | 36, 10 | remulcld 10070 |
. . . . . . 7
Λ |
38 | 37 | recnd 10068 |
. . . . . 6
Λ |
39 | 5, 38 | fsumcl 14464 |
. . . . 5
Λ |
40 | 39 | adantr 481 |
. . . 4
Λ |
41 | | eqidd 2623 |
. . . 4
Λ Λ |
42 | | eqidd 2623 |
. . . 4
Λ Λ |
43 | 4, 17, 40, 41, 42 | offval2 6914 |
. . 3
Λ
Λ
Λ Λ |
44 | 13, 16, 40 | sub32d 10424 |
. . . . 5
Λ Λ Λ Λ |
45 | 5, 11, 38 | fsumsub 14520 |
. . . . . . . 8
Λ Λ Λ Λ |
46 | | 1cnd 10056 |
. . . . . . . . . . 11
|
47 | 36 | recnd 10068 |
. . . . . . . . . . 11
|
48 | 46, 47, 11 | subdird 10487 |
. . . . . . . . . 10
Λ Λ Λ |
49 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
50 | 34 | recnd 10068 |
. . . . . . . . . . . 12
|
51 | | nncan 10310 |
. . . . . . . . . . . 12
|
52 | 49, 50, 51 | sylancr 695 |
. . . . . . . . . . 11
|
53 | 52 | oveq1d 6665 |
. . . . . . . . . 10
Λ Λ |
54 | 11 | mulid2d 10058 |
. . . . . . . . . . 11
Λ Λ |
55 | 54 | oveq1d 6665 |
. . . . . . . . . 10
Λ Λ Λ Λ |
56 | 48, 53, 55 | 3eqtr3rd 2665 |
. . . . . . . . 9
Λ Λ Λ |
57 | 56 | sumeq2dv 14433 |
. . . . . . . 8
Λ Λ Λ |
58 | 45, 57 | eqtr3d 2658 |
. . . . . . 7
Λ Λ Λ |
59 | 58 | oveq1d 6665 |
. . . . . 6
Λ Λ
Λ |
60 | 59 | adantr 481 |
. . . . 5
Λ Λ Λ |
61 | 44, 60 | eqtrd 2656 |
. . . 4
Λ Λ Λ |
62 | 61 | mpteq2dva 4744 |
. . 3
Λ Λ Λ |
63 | 43, 62 | eqtrd 2656 |
. 2
Λ
Λ
Λ |
64 | | vmadivsum 25171 |
. . 3
Λ |
65 | 2 | a1i 11 |
. . . 4
|
66 | | 1red 10055 |
. . . 4
|
67 | | prmdvdsfi 24833 |
. . . . . 6
|
68 | 23, 67 | syl 17 |
. . . . 5
|
69 | | elrabi 3359 |
. . . . . 6
|
70 | | prmnn 15388 |
. . . . . . . . . 10
|
71 | 70 | adantl 482 |
. . . . . . . . 9
|
72 | 71 | nnrpd 11870 |
. . . . . . . 8
|
73 | 72 | relogcld 24369 |
. . . . . . 7
|
74 | | prmuz2 15408 |
. . . . . . . . 9
|
75 | 74 | adantl 482 |
. . . . . . . 8
|
76 | | uz2m1nn 11763 |
. . . . . . . 8
|
77 | 75, 76 | syl 17 |
. . . . . . 7
|
78 | 73, 77 | nndivred 11069 |
. . . . . 6
|
79 | 69, 78 | sylan2 491 |
. . . . 5
|
80 | 68, 79 | fsumrecl 14465 |
. . . 4
|
81 | | fzfid 12772 |
. . . . . . 7
|
82 | | simpr 477 |
. . . . . . . . . . 11
|
83 | | 0re 10040 |
. . . . . . . . . . 11
|
84 | 82, 83 | syl6eqel 2709 |
. . . . . . . . . 10
|
85 | | eqid 2622 |
. . . . . . . . . . . 12
Unit Unit |
86 | 23 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
87 | | rpvmasum.d |
. . . . . . . . . . . . . 14
|
88 | 19 | dchrabl 24979 |
. . . . . . . . . . . . . . . 16
|
89 | | ablgrp 18198 |
. . . . . . . . . . . . . . . 16
|
90 | 87, 21 | grpidcl 17450 |
. . . . . . . . . . . . . . . 16
|
91 | 23, 88, 89, 90 | 4syl 19 |
. . . . . . . . . . . . . . 15
|
92 | 91 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
93 | 33 | adantlr 751 |
. . . . . . . . . . . . . 14
|
94 | 19, 20, 87, 22, 85, 92, 93 | dchrn0 24975 |
. . . . . . . . . . . . 13
Unit |
95 | 94 | biimpa 501 |
. . . . . . . . . . . 12
Unit |
96 | 19, 20, 21, 85, 86, 95 | dchr1 24982 |
. . . . . . . . . . 11
|
97 | 96, 18 | syl6eqel 2709 |
. . . . . . . . . 10
|
98 | 84, 97 | pm2.61dane 2881 |
. . . . . . . . 9
|
99 | 18, 98, 35 | sylancr 695 |
. . . . . . . 8
|
100 | 10 | adantlr 751 |
. . . . . . . 8
Λ |
101 | 99, 100 | remulcld 10070 |
. . . . . . 7
Λ |
102 | 81, 101 | fsumrecl 14465 |
. . . . . 6
Λ |
103 | | 0le1 10551 |
. . . . . . . . . . 11
|
104 | 82, 103 | syl6eqbr 4692 |
. . . . . . . . . 10
|
105 | 18 | leidi 10562 |
. . . . . . . . . . 11
|
106 | 96, 105 | syl6eqbr 4692 |
. . . . . . . . . 10
|
107 | 104, 106 | pm2.61dane 2881 |
. . . . . . . . 9
|
108 | | subge0 10541 |
. . . . . . . . . 10
|
109 | 18, 98, 108 | sylancr 695 |
. . . . . . . . 9
|
110 | 107, 109 | mpbird 247 |
. . . . . . . 8
|
111 | 9 | adantlr 751 |
. . . . . . . . 9
Λ |
112 | 6 | adantl 482 |
. . . . . . . . . 10
|
113 | | vmage0 24847 |
. . . . . . . . . 10
Λ |
114 | 112, 113 | syl 17 |
. . . . . . . . 9
Λ |
115 | 112 | nnred 11035 |
. . . . . . . . 9
|
116 | 112 | nngt0d 11064 |
. . . . . . . . 9
|
117 | | divge0 10892 |
. . . . . . . . 9
Λ Λ
Λ |
118 | 111, 114,
115, 116, 117 | syl22anc 1327 |
. . . . . . . 8
Λ |
119 | 99, 100, 110, 118 | mulge0d 10604 |
. . . . . . 7
Λ |
120 | 81, 101, 119 | fsumge0 14527 |
. . . . . 6
Λ |
121 | 102, 120 | absidd 14161 |
. . . . 5
Λ Λ |
122 | 68 | adantr 481 |
. . . . . . . 8
|
123 | | inss2 3834 |
. . . . . . . . 9
|
124 | | rabss2 3685 |
. . . . . . . . 9
|
125 | 123, 124 | mp1i 13 |
. . . . . . . 8
|
126 | | ssfi 8180 |
. . . . . . . 8
|
127 | 122, 125,
126 | syl2anc 693 |
. . . . . . 7
|
128 | | ssrab2 3687 |
. . . . . . . . . 10
|
129 | 128, 123 | sstri 3612 |
. . . . . . . . 9
|
130 | 129 | sseli 3599 |
. . . . . . . 8
|
131 | 78 | adantlr 751 |
. . . . . . . 8
|
132 | 130, 131 | sylan2 491 |
. . . . . . 7
|
133 | 127, 132 | fsumrecl 14465 |
. . . . . 6
|
134 | 80 | adantr 481 |
. . . . . 6
|
135 | | fveq2 6191 |
. . . . . . . . . . . 12
|
136 | 135 | fveq2d 6195 |
. . . . . . . . . . 11
|
137 | 136 | oveq2d 6666 |
. . . . . . . . . 10
|
138 | | fveq2 6191 |
. . . . . . . . . . 11
Λ Λ |
139 | | id 22 |
. . . . . . . . . . 11
|
140 | 138, 139 | oveq12d 6668 |
. . . . . . . . . 10
Λ Λ |
141 | 137, 140 | oveq12d 6668 |
. . . . . . . . 9
Λ Λ |
142 | | rpre 11839 |
. . . . . . . . . 10
|
143 | 142 | ad2antrl 764 |
. . . . . . . . 9
|
144 | 38 | adantlr 751 |
. . . . . . . . 9
Λ |
145 | | simprr 796 |
. . . . . . . . . . . . 13
Λ Λ |
146 | 145 | oveq1d 6665 |
. . . . . . . . . . . 12
Λ Λ |
147 | 6 | ad2antrl 764 |
. . . . . . . . . . . . . 14
Λ
|
148 | 147 | nncnd 11036 |
. . . . . . . . . . . . 13
Λ
|
149 | 147 | nnne0d 11065 |
. . . . . . . . . . . . 13
Λ |
150 | 148, 149 | div0d 10800 |
. . . . . . . . . . . 12
Λ |
151 | 146, 150 | eqtrd 2656 |
. . . . . . . . . . 11
Λ Λ |
152 | 151 | oveq2d 6666 |
. . . . . . . . . 10
Λ Λ |
153 | 47 | ad2ant2r 783 |
. . . . . . . . . . 11
Λ |
154 | 153 | mul01d 10235 |
. . . . . . . . . 10
Λ |
155 | 152, 154 | eqtrd 2656 |
. . . . . . . . 9
Λ Λ |
156 | 141, 143,
144, 155 | fsumvma2 24939 |
. . . . . . . 8
Λ Λ |
157 | 128 | a1i 11 |
. . . . . . . . 9
|
158 | | fzfid 12772 |
. . . . . . . . . . 11
|
159 | 24 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
160 | 30 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
161 | 70 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
|
162 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
|
163 | 162 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | 163 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 161, 164 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . 18
|
166 | 165 | nnzd 11481 |
. . . . . . . . . . . . . . . . 17
|
167 | 160, 166 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
168 | 159, 167 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
|
169 | | resubcl 10345 |
. . . . . . . . . . . . . . 15
|
170 | 18, 168, 169 | sylancr 695 |
. . . . . . . . . . . . . 14
|
171 | | vmacl 24844 |
. . . . . . . . . . . . . . . 16
Λ |
172 | 165, 171 | syl 17 |
. . . . . . . . . . . . . . 15
Λ |
173 | 172, 165 | nndivred 11069 |
. . . . . . . . . . . . . 14
Λ |
174 | 170, 173 | remulcld 10070 |
. . . . . . . . . . . . 13
Λ |
175 | 174 | anassrs 680 |
. . . . . . . . . . . 12
Λ |
176 | 175 | recnd 10068 |
. . . . . . . . . . 11
Λ |
177 | 158, 176 | fsumcl 14464 |
. . . . . . . . . 10
Λ |
178 | 130, 177 | sylan2 491 |
. . . . . . . . 9
Λ |
179 | | breq1 4656 |
. . . . . . . . . . . 12
|
180 | 179 | notbid 308 |
. . . . . . . . . . 11
|
181 | | notrab 3904 |
. . . . . . . . . . 11
|
182 | 180, 181 | elrab2 3366 |
. . . . . . . . . 10
|
183 | 123 | sseli 3599 |
. . . . . . . . . . 11
|
184 | 23 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
|
185 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . 21
|
186 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . 22
|
187 | 184 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
188 | | coprm 15423 |
. . . . . . . . . . . . . . . . . . . . . 22
|
189 | 186, 187,
188 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
190 | 185, 189 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
191 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . 22
|
192 | 186, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
193 | 162 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
194 | 193 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . 21
|
195 | | rpexp1i 15433 |
. . . . . . . . . . . . . . . . . . . . 21
|
196 | 192, 187,
194, 195 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
197 | 190, 196 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
|
198 | 184 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . 20
|
199 | 166 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . 21
|
200 | 199 | adantlrr 757 |
. . . . . . . . . . . . . . . . . . . 20
|
201 | 20, 85, 27 | znunit 19912 |
. . . . . . . . . . . . . . . . . . . 20
Unit
|
202 | 198, 200,
201 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
Unit
|
203 | 197, 202 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
Unit |
204 | 19, 20, 21, 85, 184, 203 | dchr1 24982 |
. . . . . . . . . . . . . . . . 17
|
205 | 204 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
206 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . 16
|
207 | 205, 206 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
208 | 207 | oveq1d 6665 |
. . . . . . . . . . . . . 14
Λ Λ |
209 | 173 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
Λ |
210 | 209 | anassrs 680 |
. . . . . . . . . . . . . . . 16
Λ |
211 | 210 | adantlrr 757 |
. . . . . . . . . . . . . . 15
Λ |
212 | 211 | mul02d 10234 |
. . . . . . . . . . . . . 14
Λ |
213 | 208, 212 | eqtrd 2656 |
. . . . . . . . . . . . 13
Λ |
214 | 213 | sumeq2dv 14433 |
. . . . . . . . . . . 12
Λ |
215 | | fzfid 12772 |
. . . . . . . . . . . . . 14
|
216 | 215 | olcd 408 |
. . . . . . . . . . . . 13
|
217 | | sumz 14453 |
. . . . . . . . . . . . 13
|
218 | 216, 217 | syl 17 |
. . . . . . . . . . . 12
|
219 | 214, 218 | eqtrd 2656 |
. . . . . . . . . . 11
Λ |
220 | 183, 219 | sylanr1 684 |
. . . . . . . . . 10
Λ |
221 | 182, 220 | sylan2b 492 |
. . . . . . . . 9
Λ |
222 | | ppifi 24832 |
. . . . . . . . . 10
|
223 | 143, 222 | syl 17 |
. . . . . . . . 9
|
224 | 157, 178,
221, 223 | fsumss 14456 |
. . . . . . . 8
Λ Λ |
225 | 156, 224 | eqtr4d 2659 |
. . . . . . 7
Λ
Λ |
226 | 158, 175 | fsumrecl 14465 |
. . . . . . . . 9
Λ |
227 | 130, 226 | sylan2 491 |
. . . . . . . 8
Λ |
228 | 73 | adantlr 751 |
. . . . . . . . . . 11
|
229 | 70 | adantl 482 |
. . . . . . . . . . . . . 14
|
230 | 229 | nnrecred 11066 |
. . . . . . . . . . . . 13
|
231 | 229 | nnrpd 11870 |
. . . . . . . . . . . . . . . 16
|
232 | 231 | rpreccld 11882 |
. . . . . . . . . . . . . . 15
|
233 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
|
234 | 233 | relogcld 24369 |
. . . . . . . . . . . . . . . . . 18
|
235 | 229 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
|
236 | 74 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
237 | | eluz2b2 11761 |
. . . . . . . . . . . . . . . . . . . . 21
|
238 | 237 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . 20
|
239 | 236, 238 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
240 | 235, 239 | rplogcld 24375 |
. . . . . . . . . . . . . . . . . 18
|
241 | 234, 240 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . 17
|
242 | 241 | flcld 12599 |
. . . . . . . . . . . . . . . 16
|
243 | 242 | peano2zd 11485 |
. . . . . . . . . . . . . . 15
|
244 | 232, 243 | rpexpcld 13032 |
. . . . . . . . . . . . . 14
|
245 | 244 | rpred 11872 |
. . . . . . . . . . . . 13
|
246 | 230, 245 | resubcld 10458 |
. . . . . . . . . . . 12
|
247 | 236, 76 | syl 17 |
. . . . . . . . . . . . . 14
|
248 | 247 | nnrpd 11870 |
. . . . . . . . . . . . 13
|
249 | 248, 231 | rpdivcld 11889 |
. . . . . . . . . . . 12
|
250 | 246, 249 | rerpdivcld 11903 |
. . . . . . . . . . 11
|
251 | 228, 250 | remulcld 10070 |
. . . . . . . . . 10
|
252 | 172 | recnd 10068 |
. . . . . . . . . . . . . . . 16
Λ |
253 | 165 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
254 | 165 | nnne0d 11065 |
. . . . . . . . . . . . . . . 16
|
255 | 252, 253,
254 | divrecd 10804 |
. . . . . . . . . . . . . . 15
Λ Λ |
256 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
|
257 | | vmappw 24842 |
. . . . . . . . . . . . . . . . 17
Λ |
258 | 256, 163,
257 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
Λ |
259 | 161 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
260 | 161 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . 18
|
261 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . 19
|
262 | 261 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
|
263 | 259, 260,
262 | exprecd 13016 |
. . . . . . . . . . . . . . . . 17
|
264 | 263 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
265 | 258, 264 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
Λ |
266 | 255, 265 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Λ |
267 | 266, 173 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
|
268 | 267 | anassrs 680 |
. . . . . . . . . . . 12
|
269 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
270 | | vmage0 24847 |
. . . . . . . . . . . . . . . . 17
Λ |
271 | 165, 270 | syl 17 |
. . . . . . . . . . . . . . . 16
Λ |
272 | 165 | nnred 11035 |
. . . . . . . . . . . . . . . 16
|
273 | 165 | nngt0d 11064 |
. . . . . . . . . . . . . . . 16
|
274 | | divge0 10892 |
. . . . . . . . . . . . . . . 16
Λ Λ
Λ |
275 | 172, 271,
272, 273, 274 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
Λ |
276 | 83 | leidi 10562 |
. . . . . . . . . . . . . . . . . 18
|
277 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
278 | 276, 277 | syl5breqr 4691 |
. . . . . . . . . . . . . . . . 17
|
279 | 23 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
|
280 | 91 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
281 | 19, 20, 87, 22, 85, 280, 167 | dchrn0 24975 |
. . . . . . . . . . . . . . . . . . . 20
Unit |
282 | 281 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
Unit |
283 | 19, 20, 21, 85, 279, 282 | dchr1 24982 |
. . . . . . . . . . . . . . . . . 18
|
284 | 103, 283 | syl5breqr 4691 |
. . . . . . . . . . . . . . . . 17
|
285 | 278, 284 | pm2.61dane 2881 |
. . . . . . . . . . . . . . . 16
|
286 | | subge02 10544 |
. . . . . . . . . . . . . . . . 17
|
287 | 18, 168, 286 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
288 | 285, 287 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
289 | 170, 269,
173, 275, 288 | lemul1ad 10963 |
. . . . . . . . . . . . . 14
Λ Λ |
290 | 209 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
Λ Λ |
291 | 290, 266 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Λ |
292 | 289, 291 | breqtrd 4679 |
. . . . . . . . . . . . 13
Λ |
293 | 292 | anassrs 680 |
. . . . . . . . . . . 12
Λ
|
294 | 158, 175,
268, 293 | fsumle 14531 |
. . . . . . . . . . 11
Λ |
295 | 228 | recnd 10068 |
. . . . . . . . . . . . 13
|
296 | 161 | nnrecred 11066 |
. . . . . . . . . . . . . . . 16
|
297 | 296, 164 | reexpcld 13025 |
. . . . . . . . . . . . . . 15
|
298 | 297 | recnd 10068 |
. . . . . . . . . . . . . 14
|
299 | 298 | anassrs 680 |
. . . . . . . . . . . . 13
|
300 | 158, 295,
299 | fsummulc2 14516 |
. . . . . . . . . . . 12
|
301 | | fzval3 12536 |
. . . . . . . . . . . . . . . 16
..^ |
302 | 242, 301 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
303 | 302 | sumeq1d 14431 |
. . . . . . . . . . . . . 14
..^ |
304 | 230 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
305 | 229 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . 18
|
306 | | recgt1 10919 |
. . . . . . . . . . . . . . . . . 18
|
307 | 235, 305,
306 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
308 | 239, 307 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
309 | 230, 308 | ltned 10173 |
. . . . . . . . . . . . . . 15
|
310 | | 1nn0 11308 |
. . . . . . . . . . . . . . . 16
|
311 | 310 | a1i 11 |
. . . . . . . . . . . . . . 15
|
312 | | log1 24332 |
. . . . . . . . . . . . . . . . . . . . 21
|
313 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
|
314 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
315 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
316 | | logleb 24349 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
317 | 314, 315,
316 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
|
318 | 313, 317 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
|
319 | 312, 318 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . . 20
|
320 | 319 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
321 | 234, 240,
320 | divge0d 11912 |
. . . . . . . . . . . . . . . . . 18
|
322 | | flge0nn0 12621 |
. . . . . . . . . . . . . . . . . 18
|
323 | 241, 321,
322 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
324 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . 17
|
325 | 323, 324 | syl 17 |
. . . . . . . . . . . . . . . 16
|
326 | | nnuz 11723 |
. . . . . . . . . . . . . . . 16
|
327 | 325, 326 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
|
328 | 304, 309,
311, 327 | geoserg 14598 |
. . . . . . . . . . . . . 14
..^ |
329 | 304 | exp1d 13003 |
. . . . . . . . . . . . . . . 16
|
330 | 329 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
331 | 229 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
332 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
|
333 | 231 | rpcnne0d 11881 |
. . . . . . . . . . . . . . . . 17
|
334 | | divsubdir 10721 |
. . . . . . . . . . . . . . . . 17
|
335 | 331, 332,
333, 334 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
336 | | divid 10714 |
. . . . . . . . . . . . . . . . . 18
|
337 | 333, 336 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
338 | 337 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
339 | 335, 338 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
|
340 | 330, 339 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
341 | 303, 328,
340 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
342 | 341 | oveq2d 6666 |
. . . . . . . . . . . 12
|
343 | 300, 342 | eqtr3d 2658 |
. . . . . . . . . . 11
|
344 | 294, 343 | breqtrd 4679 |
. . . . . . . . . 10
Λ |
345 | 244 | rpge0d 11876 |
. . . . . . . . . . . . . . 15
|
346 | 230, 245 | subge02d 10619 |
. . . . . . . . . . . . . . 15
|
347 | 345, 346 | mpbid 222 |
. . . . . . . . . . . . . 14
|
348 | 248 | rpcnne0d 11881 |
. . . . . . . . . . . . . . 15
|
349 | | dmdcan 10735 |
. . . . . . . . . . . . . . 15
|
350 | 348, 333,
332, 349 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
351 | 347, 350 | breqtrrd 4681 |
. . . . . . . . . . . . 13
|
352 | 247 | nnrecred 11066 |
. . . . . . . . . . . . . 14
|
353 | 246, 352,
249 | ledivmuld 11925 |
. . . . . . . . . . . . 13
|
354 | 351, 353 | mpbird 247 |
. . . . . . . . . . . 12
|
355 | 250, 352,
240 | lemul2d 11916 |
. . . . . . . . . . . 12
|
356 | 354, 355 | mpbid 222 |
. . . . . . . . . . 11
|
357 | 247 | nncnd 11036 |
. . . . . . . . . . . 12
|
358 | 247 | nnne0d 11065 |
. . . . . . . . . . . 12
|
359 | 295, 357,
358 | divrecd 10804 |
. . . . . . . . . . 11
|
360 | 356, 359 | breqtrrd 4681 |
. . . . . . . . . 10
|
361 | 226, 251,
131, 344, 360 | letrd 10194 |
. . . . . . . . 9
Λ |
362 | 130, 361 | sylan2 491 |
. . . . . . . 8
Λ
|
363 | 127, 227,
132, 362 | fsumle 14531 |
. . . . . . 7
Λ
|
364 | 225, 363 | eqbrtrd 4675 |
. . . . . 6
Λ
|
365 | 79 | adantlr 751 |
. . . . . . 7
|
366 | 240, 248 | rpdivcld 11889 |
. . . . . . . . 9
|
367 | 366 | rpge0d 11876 |
. . . . . . . 8
|
368 | 69, 367 | sylan2 491 |
. . . . . . 7
|
369 | 122, 365,
368, 125 | fsumless 14528 |
. . . . . 6
|
370 | 102, 133,
134, 364, 369 | letrd 10194 |
. . . . 5
Λ
|
371 | 121, 370 | eqbrtrd 4675 |
. . . 4
Λ |
372 | 65, 40, 66, 80, 371 | elo1d 14267 |
. . 3
Λ |
373 | | o1sub 14346 |
. . 3
Λ Λ Λ
Λ |
374 | 64, 372, 373 | sylancr 695 |
. 2
Λ
Λ |
375 | 63, 374 | eqeltrrd 2702 |
1
Λ |