Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . 7
ψ |
2 | | pntlem1.a |
. . . . . . 7
|
3 | | pntlem1.b |
. . . . . . 7
|
4 | | pntlem1.l |
. . . . . . 7
|
5 | | pntlem1.d |
. . . . . . 7
|
6 | | pntlem1.f |
. . . . . . 7
; |
7 | | pntlem1.u |
. . . . . . 7
|
8 | | pntlem1.u2 |
. . . . . . 7
|
9 | | pntlem1.e |
. . . . . . 7
|
10 | | pntlem1.k |
. . . . . . 7
|
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 25284 |
. . . . . 6
|
12 | 11 | simp3d 1075 |
. . . . 5
|
13 | 12 | simp3d 1075 |
. . . 4
|
14 | 1, 2, 3, 4, 5, 6 | pntlemd 25283 |
. . . . . . . 8
|
15 | 14 | simp1d 1073 |
. . . . . . 7
|
16 | 11 | simp1d 1073 |
. . . . . . . 8
|
17 | | 2z 11409 |
. . . . . . . 8
|
18 | | rpexpcl 12879 |
. . . . . . . 8
|
19 | 16, 17, 18 | sylancl 694 |
. . . . . . 7
|
20 | 15, 19 | rpmulcld 11888 |
. . . . . 6
|
21 | | 3nn0 11310 |
. . . . . . . . 9
|
22 | | 2nn 11185 |
. . . . . . . . 9
|
23 | 21, 22 | decnncl 11518 |
. . . . . . . 8
; |
24 | | nnrp 11842 |
. . . . . . . 8
; ; |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
; |
26 | | rpmulcl 11855 |
. . . . . . 7
; ; |
27 | 25, 3, 26 | sylancr 695 |
. . . . . 6
; |
28 | 20, 27 | rpdivcld 11889 |
. . . . 5
; |
29 | | pntlem1.y |
. . . . . . . . . 10
|
30 | | pntlem1.x |
. . . . . . . . . 10
|
31 | | pntlem1.c |
. . . . . . . . . 10
|
32 | | pntlem1.w |
. . . . . . . . . 10
; |
33 | | pntlem1.z |
. . . . . . . . . 10
|
34 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33 | pntlemb 25286 |
. . . . . . . . 9
; |
35 | 34 | simp1d 1073 |
. . . . . . . 8
|
36 | 35 | rpred 11872 |
. . . . . . 7
|
37 | 34 | simp2d 1074 |
. . . . . . . 8
|
38 | 37 | simp1d 1073 |
. . . . . . 7
|
39 | 36, 38 | rplogcld 24375 |
. . . . . 6
|
40 | | rpexpcl 12879 |
. . . . . 6
|
41 | 39, 17, 40 | sylancl 694 |
. . . . 5
|
42 | 28, 41 | rpmulcld 11888 |
. . . 4
; |
43 | 13, 42 | rpmulcld 11888 |
. . 3
; |
44 | 43 | rpred 11872 |
. 2
; |
45 | 15, 16 | rpmulcld 11888 |
. . . . . . 7
|
46 | | 8re 11105 |
. . . . . . . 8
|
47 | | 8pos 11121 |
. . . . . . . 8
|
48 | 46, 47 | elrpii 11835 |
. . . . . . 7
|
49 | | rpdivcl 11856 |
. . . . . . 7
|
50 | 45, 48, 49 | sylancl 694 |
. . . . . 6
|
51 | 50, 39 | rpmulcld 11888 |
. . . . 5
|
52 | 13, 51 | rpmulcld 11888 |
. . . 4
|
53 | 52 | rpred 11872 |
. . 3
|
54 | | pntlem1.m |
. . . . . . . 8
|
55 | | pntlem1.n |
. . . . . . . 8
|
56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemg 25287 |
. . . . . . 7
|
57 | 56 | simp1d 1073 |
. . . . . 6
|
58 | 56 | simp2d 1074 |
. . . . . 6
|
59 | | eluznn 11758 |
. . . . . 6
|
60 | 57, 58, 59 | syl2anc 693 |
. . . . 5
|
61 | 60 | nnred 11035 |
. . . 4
|
62 | 57 | nnred 11035 |
. . . 4
|
63 | 61, 62 | resubcld 10458 |
. . 3
|
64 | 53, 63 | remulcld 10070 |
. 2
|
65 | | fzfid 12772 |
. . 3
|
66 | 7 | rpred 11872 |
. . . . . 6
|
67 | | elfznn 12370 |
. . . . . 6
|
68 | | nndivre 11056 |
. . . . . 6
|
69 | 66, 67, 68 | syl2an 494 |
. . . . 5
|
70 | 35 | adantr 481 |
. . . . . . . . . 10
|
71 | 67 | adantl 482 |
. . . . . . . . . . 11
|
72 | 71 | nnrpd 11870 |
. . . . . . . . . 10
|
73 | 70, 72 | rpdivcld 11889 |
. . . . . . . . 9
|
74 | 1 | pntrf 25252 |
. . . . . . . . . 10
|
75 | 74 | ffvelrni 6358 |
. . . . . . . . 9
|
76 | 73, 75 | syl 17 |
. . . . . . . 8
|
77 | 76, 70 | rerpdivcld 11903 |
. . . . . . 7
|
78 | 77 | recnd 10068 |
. . . . . 6
|
79 | 78 | abscld 14175 |
. . . . 5
|
80 | 69, 79 | resubcld 10458 |
. . . 4
|
81 | 72 | relogcld 24369 |
. . . 4
|
82 | 80, 81 | remulcld 10070 |
. . 3
|
83 | 65, 82 | fsumrecl 14465 |
. 2
|
84 | 45 | rpcnd 11874 |
. . . . . . . . 9
|
85 | 11 | simp2d 1074 |
. . . . . . . . . . . . 13
|
86 | 85 | rpred 11872 |
. . . . . . . . . . . 12
|
87 | 12 | simp2d 1074 |
. . . . . . . . . . . 12
|
88 | 86, 87 | rplogcld 24375 |
. . . . . . . . . . 11
|
89 | 39, 88 | rpdivcld 11889 |
. . . . . . . . . 10
|
90 | 89 | rpcnd 11874 |
. . . . . . . . 9
|
91 | | rpcnne0 11850 |
. . . . . . . . . 10
|
92 | 48, 91 | mp1i 13 |
. . . . . . . . 9
|
93 | | 4re 11097 |
. . . . . . . . . . 11
|
94 | | 4pos 11116 |
. . . . . . . . . . 11
|
95 | 93, 94 | elrpii 11835 |
. . . . . . . . . 10
|
96 | | rpcnne0 11850 |
. . . . . . . . . 10
|
97 | 95, 96 | mp1i 13 |
. . . . . . . . 9
|
98 | | divmuldiv 10725 |
. . . . . . . . 9
|
99 | 84, 90, 92, 97, 98 | syl22anc 1327 |
. . . . . . . 8
|
100 | 10 | fveq2i 6194 |
. . . . . . . . . . . . . 14
|
101 | 3, 16 | rpdivcld 11889 |
. . . . . . . . . . . . . . . 16
|
102 | 101 | rpred 11872 |
. . . . . . . . . . . . . . 15
|
103 | 102 | relogefd 24374 |
. . . . . . . . . . . . . 14
|
104 | 100, 103 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
105 | 104 | oveq2d 6666 |
. . . . . . . . . . . 12
|
106 | 39 | rpcnd 11874 |
. . . . . . . . . . . . 13
|
107 | 3 | rpcnne0d 11881 |
. . . . . . . . . . . . 13
|
108 | 16 | rpcnne0d 11881 |
. . . . . . . . . . . . 13
|
109 | | divdiv2 10737 |
. . . . . . . . . . . . 13
|
110 | 106, 107,
108, 109 | syl3anc 1326 |
. . . . . . . . . . . 12
|
111 | 105, 110 | eqtrd 2656 |
. . . . . . . . . . 11
|
112 | 111 | oveq2d 6666 |
. . . . . . . . . 10
|
113 | 16 | rpcnd 11874 |
. . . . . . . . . . . 12
|
114 | 106, 113 | mulcld 10060 |
. . . . . . . . . . 11
|
115 | | divass 10703 |
. . . . . . . . . . 11
|
116 | 84, 114, 107, 115 | syl3anc 1326 |
. . . . . . . . . 10
|
117 | 15 | rpcnd 11874 |
. . . . . . . . . . . . 13
|
118 | 117, 113,
106, 113 | mul4d 10248 |
. . . . . . . . . . . 12
|
119 | 113 | sqvald 13005 |
. . . . . . . . . . . . 13
|
120 | 119 | oveq2d 6666 |
. . . . . . . . . . . 12
|
121 | 113 | sqcld 13006 |
. . . . . . . . . . . . 13
|
122 | 117, 106,
121 | mul32d 10246 |
. . . . . . . . . . . 12
|
123 | 118, 120,
122 | 3eqtr2d 2662 |
. . . . . . . . . . 11
|
124 | 123 | oveq1d 6665 |
. . . . . . . . . 10
|
125 | 112, 116,
124 | 3eqtr2d 2662 |
. . . . . . . . 9
|
126 | | 8t4e32 11656 |
. . . . . . . . . 10
; |
127 | 126 | a1i 11 |
. . . . . . . . 9
; |
128 | 125, 127 | oveq12d 6668 |
. . . . . . . 8
; |
129 | 20 | rpcnd 11874 |
. . . . . . . . . . 11
|
130 | 129, 106 | mulcld 10060 |
. . . . . . . . . 10
|
131 | | rpcnne0 11850 |
. . . . . . . . . . 11
; ; ; |
132 | 25, 131 | mp1i 13 |
. . . . . . . . . 10
; ; |
133 | | divdiv1 10736 |
. . . . . . . . . 10
; ;
;
; |
134 | 130, 107,
132, 133 | syl3anc 1326 |
. . . . . . . . 9
;
; |
135 | 23 | nncni 11030 |
. . . . . . . . . . 11
; |
136 | 3 | rpcnd 11874 |
. . . . . . . . . . 11
|
137 | | mulcom 10022 |
. . . . . . . . . . 11
;
; ; |
138 | 135, 136,
137 | sylancr 695 |
. . . . . . . . . 10
; ; |
139 | 138 | oveq2d 6666 |
. . . . . . . . 9
;
; |
140 | 27 | rpcnne0d 11881 |
. . . . . . . . . 10
; ; |
141 | | div23 10704 |
. . . . . . . . . 10
; ; ; ; |
142 | 129, 106,
140, 141 | syl3anc 1326 |
. . . . . . . . 9
; ; |
143 | 134, 139,
142 | 3eqtr2d 2662 |
. . . . . . . 8
; ; |
144 | 99, 128, 143 | 3eqtrd 2660 |
. . . . . . 7
; |
145 | 144 | oveq1d 6665 |
. . . . . 6
; |
146 | 50 | rpcnd 11874 |
. . . . . . 7
|
147 | 89 | rpred 11872 |
. . . . . . . . 9
|
148 | | 4nn 11187 |
. . . . . . . . 9
|
149 | | nndivre 11056 |
. . . . . . . . 9
|
150 | 147, 148,
149 | sylancl 694 |
. . . . . . . 8
|
151 | 150 | recnd 10068 |
. . . . . . 7
|
152 | 146, 106,
151 | mul32d 10246 |
. . . . . 6
|
153 | 106 | sqvald 13005 |
. . . . . . . 8
|
154 | 153 | oveq2d 6666 |
. . . . . . 7
; ; |
155 | 28 | rpcnd 11874 |
. . . . . . . 8
; |
156 | 155, 106,
106 | mulassd 10063 |
. . . . . . 7
; ; |
157 | 154, 156 | eqtr4d 2659 |
. . . . . 6
; ; |
158 | 145, 152,
157 | 3eqtr4d 2666 |
. . . . 5
; |
159 | 56 | simp3d 1075 |
. . . . . 6
|
160 | 150, 63, 51 | lemul2d 11916 |
. . . . . 6
|
161 | 159, 160 | mpbid 222 |
. . . . 5
|
162 | 158, 161 | eqbrtrrd 4677 |
. . . 4
;
|
163 | 42 | rpred 11872 |
. . . . 5
; |
164 | 51 | rpred 11872 |
. . . . . 6
|
165 | 164, 63 | remulcld 10070 |
. . . . 5
|
166 | 163, 165,
13 | lemul2d 11916 |
. . . 4
;
; |
167 | 162, 166 | mpbid 222 |
. . 3
; |
168 | 13 | rpcnd 11874 |
. . . 4
|
169 | 51 | rpcnd 11874 |
. . . 4
|
170 | 63 | recnd 10068 |
. . . 4
|
171 | 168, 169,
170 | mulassd 10063 |
. . 3
|
172 | 167, 171 | breqtrrd 4681 |
. 2
; |
173 | | fzfid 12772 |
. . . 4
|
174 | 60 | nnzd 11481 |
. . . . . . . . . . . 12
|
175 | 85, 174 | rpexpcld 13032 |
. . . . . . . . . . 11
|
176 | 35, 175 | rpdivcld 11889 |
. . . . . . . . . 10
|
177 | 176 | rprege0d 11879 |
. . . . . . . . 9
|
178 | | flge0nn0 12621 |
. . . . . . . . 9
|
179 | | nn0p1nn 11332 |
. . . . . . . . 9
|
180 | 177, 178,
179 | 3syl 18 |
. . . . . . . 8
|
181 | | nnuz 11723 |
. . . . . . . 8
|
182 | 180, 181 | syl6eleq 2711 |
. . . . . . 7
|
183 | | fzss1 12380 |
. . . . . . 7
|
184 | 182, 183 | syl 17 |
. . . . . 6
|
185 | 184 | sselda 3603 |
. . . . 5
|
186 | 185, 82 | syldan 487 |
. . . 4
|
187 | 173, 186 | fsumrecl 14465 |
. . 3
|
188 | | eluzfz2 12349 |
. . . . 5
|
189 | 58, 188 | syl 17 |
. . . 4
|
190 | | oveq1 6657 |
. . . . . . . 8
|
191 | 190 | oveq2d 6666 |
. . . . . . 7
|
192 | | oveq2 6658 |
. . . . . . . . . . . 12
|
193 | 192 | oveq2d 6666 |
. . . . . . . . . . 11
|
194 | 193 | fveq2d 6195 |
. . . . . . . . . 10
|
195 | 194 | oveq1d 6665 |
. . . . . . . . 9
|
196 | 195 | oveq1d 6665 |
. . . . . . . 8
|
197 | 196 | sumeq1d 14431 |
. . . . . . 7
|
198 | 191, 197 | breq12d 4666 |
. . . . . 6
|
199 | 198 | imbi2d 330 |
. . . . 5
|
200 | | oveq1 6657 |
. . . . . . . 8
|
201 | 200 | oveq2d 6666 |
. . . . . . 7
|
202 | | oveq2 6658 |
. . . . . . . . . . . 12
|
203 | 202 | oveq2d 6666 |
. . . . . . . . . . 11
|
204 | 203 | fveq2d 6195 |
. . . . . . . . . 10
|
205 | 204 | oveq1d 6665 |
. . . . . . . . 9
|
206 | 205 | oveq1d 6665 |
. . . . . . . 8
|
207 | 206 | sumeq1d 14431 |
. . . . . . 7
|
208 | 201, 207 | breq12d 4666 |
. . . . . 6
|
209 | 208 | imbi2d 330 |
. . . . 5
|
210 | | oveq1 6657 |
. . . . . . . 8
|
211 | 210 | oveq2d 6666 |
. . . . . . 7
|
212 | | oveq2 6658 |
. . . . . . . . . . . 12
|
213 | 212 | oveq2d 6666 |
. . . . . . . . . . 11
|
214 | 213 | fveq2d 6195 |
. . . . . . . . . 10
|
215 | 214 | oveq1d 6665 |
. . . . . . . . 9
|
216 | 215 | oveq1d 6665 |
. . . . . . . 8
|
217 | 216 | sumeq1d 14431 |
. . . . . . 7
|
218 | 211, 217 | breq12d 4666 |
. . . . . 6
|
219 | 218 | imbi2d 330 |
. . . . 5
|
220 | | oveq1 6657 |
. . . . . . . 8
|
221 | 220 | oveq2d 6666 |
. . . . . . 7
|
222 | | oveq2 6658 |
. . . . . . . . . . . 12
|
223 | 222 | oveq2d 6666 |
. . . . . . . . . . 11
|
224 | 223 | fveq2d 6195 |
. . . . . . . . . 10
|
225 | 224 | oveq1d 6665 |
. . . . . . . . 9
|
226 | 225 | oveq1d 6665 |
. . . . . . . 8
|
227 | 226 | sumeq1d 14431 |
. . . . . . 7
|
228 | 221, 227 | breq12d 4666 |
. . . . . 6
|
229 | 228 | imbi2d 330 |
. . . . 5
|
230 | 57 | nncnd 11036 |
. . . . . . . . . 10
|
231 | 230 | subidd 10380 |
. . . . . . . . 9
|
232 | 231 | oveq2d 6666 |
. . . . . . . 8
|
233 | 52 | rpcnd 11874 |
. . . . . . . . 9
|
234 | 233 | mul01d 10235 |
. . . . . . . 8
|
235 | 232, 234 | eqtrd 2656 |
. . . . . . 7
|
236 | | fzfid 12772 |
. . . . . . . 8
|
237 | 57 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
|
238 | 85, 237 | rpexpcld 13032 |
. . . . . . . . . . . . . . 15
|
239 | 35, 238 | rpdivcld 11889 |
. . . . . . . . . . . . . 14
|
240 | 239 | rprege0d 11879 |
. . . . . . . . . . . . 13
|
241 | | flge0nn0 12621 |
. . . . . . . . . . . . 13
|
242 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
|
243 | 240, 241,
242 | 3syl 18 |
. . . . . . . . . . . 12
|
244 | 243, 181 | syl6eleq 2711 |
. . . . . . . . . . 11
|
245 | | fzss1 12380 |
. . . . . . . . . . 11
|
246 | 244, 245 | syl 17 |
. . . . . . . . . 10
|
247 | 246 | sselda 3603 |
. . . . . . . . 9
|
248 | 247, 82 | syldan 487 |
. . . . . . . 8
|
249 | | elfzle2 12345 |
. . . . . . . . . . . . 13
|
250 | 249 | adantl 482 |
. . . . . . . . . . . 12
|
251 | 29 | simpld 475 |
. . . . . . . . . . . . . . 15
|
252 | 35, 251 | rpdivcld 11889 |
. . . . . . . . . . . . . 14
|
253 | 252 | rpred 11872 |
. . . . . . . . . . . . 13
|
254 | | elfzelz 12342 |
. . . . . . . . . . . . 13
|
255 | | flge 12606 |
. . . . . . . . . . . . 13
|
256 | 253, 254,
255 | syl2an 494 |
. . . . . . . . . . . 12
|
257 | 250, 256 | mpbird 247 |
. . . . . . . . . . 11
|
258 | 71, 257 | jca 554 |
. . . . . . . . . 10
|
259 | | pntlem1.U |
. . . . . . . . . . 11
|
260 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259 | pntlemn 25289 |
. . . . . . . . . 10
|
261 | 258, 260 | syldan 487 |
. . . . . . . . 9
|
262 | 247, 261 | syldan 487 |
. . . . . . . 8
|
263 | 236, 248,
262 | fsumge0 14527 |
. . . . . . 7
|
264 | 235, 263 | eqbrtrd 4675 |
. . . . . 6
|
265 | 264 | a1i 11 |
. . . . 5
|
266 | | pntlem1.K |
. . . . . . . . . 10
|
267 | | eqid 2622 |
. . . . . . . . . 10
|
268 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259, 266, 267 | pntlemi 25293 |
. . . . . . . . 9
..^
|
269 | 52 | adantr 481 |
. . . . . . . . . . 11
..^ |
270 | 269 | rpred 11872 |
. . . . . . . . . 10
..^ |
271 | | elfzoelz 12470 |
. . . . . . . . . . . . . 14
..^
|
272 | 271 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
273 | 272 | zred 11482 |
. . . . . . . . . . . 12
..^ |
274 | 57 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
275 | 274 | nnred 11035 |
. . . . . . . . . . . 12
..^ |
276 | 273, 275 | resubcld 10458 |
. . . . . . . . . . 11
..^ |
277 | 270, 276 | remulcld 10070 |
. . . . . . . . . 10
..^ |
278 | | fzfid 12772 |
. . . . . . . . . . 11
..^ |
279 | | ssun1 3776 |
. . . . . . . . . . . . . . 15
|
280 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
281 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
282 | 272 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
283 | 281, 282 | rpexpcld 13032 |
. . . . . . . . . . . . . . . . . . 19
..^ |
284 | 280, 283 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . 18
..^ |
285 | 281, 272 | rpexpcld 13032 |
. . . . . . . . . . . . . . . . . . 19
..^ |
286 | 280, 285 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . 18
..^ |
287 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
288 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
289 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
290 | 288, 86, 289 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
|
291 | 87, 290 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
|
292 | 291 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
293 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . 21
|
294 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . . 21
|
295 | 272, 293,
294 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
296 | 287, 292,
295 | leexp2ad 13041 |
. . . . . . . . . . . . . . . . . . 19
..^ |
297 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
298 | 285, 283,
297 | lediv2d 11896 |
. . . . . . . . . . . . . . . . . . 19
..^ |
299 | 296, 298 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
..^ |
300 | | flword2 12614 |
. . . . . . . . . . . . . . . . . 18
|
301 | 284, 286,
299, 300 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
..^
|
302 | | eluzp1p1 11713 |
. . . . . . . . . . . . . . . . 17
|
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ |
304 | 286 | flcld 12599 |
. . . . . . . . . . . . . . . . 17
..^
|
305 | 252 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ |
306 | 305 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
..^ |
307 | 306 | flcld 12599 |
. . . . . . . . . . . . . . . . 17
..^
|
308 | 251 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
309 | 308 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
310 | 285 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
311 | 30 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
312 | 311 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . 22
|
313 | 312 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
314 | 30 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . 22
|
315 | 314 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
316 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
317 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemh 25288 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
318 | 316, 317 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
319 | 318 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
320 | 309, 313,
310, 315, 319 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
321 | 309, 310,
320 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
..^ |
322 | 308, 285,
297 | lediv2d 11896 |
. . . . . . . . . . . . . . . . . . 19
..^ |
323 | 321, 322 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
..^ |
324 | | flwordi 12613 |
. . . . . . . . . . . . . . . . . 18
|
325 | 286, 306,
323, 324 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
..^
|
326 | | eluz2 11693 |
. . . . . . . . . . . . . . . . 17
|
327 | 304, 307,
325, 326 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . 16
..^
|
328 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . 16
|
329 | 303, 327,
328 | syl2anc 693 |
. . . . . . . . . . . . . . 15
..^
|
330 | 279, 329 | syl5sseqr 3654 |
. . . . . . . . . . . . . 14
..^
|
331 | 297, 283 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . 18
..^ |
332 | 331 | rprege0d 11879 |
. . . . . . . . . . . . . . . . 17
..^ |
333 | | flge0nn0 12621 |
. . . . . . . . . . . . . . . . 17
|
334 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . 17
|
335 | 332, 333,
334 | 3syl 18 |
. . . . . . . . . . . . . . . 16
..^ |
336 | 335, 181 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
..^ |
337 | | fzss1 12380 |
. . . . . . . . . . . . . . 15
|
338 | 336, 337 | syl 17 |
. . . . . . . . . . . . . 14
..^
|
339 | 330, 338 | sstrd 3613 |
. . . . . . . . . . . . 13
..^
|
340 | 339 | sselda 3603 |
. . . . . . . . . . . 12
..^
|
341 | 82 | adantlr 751 |
. . . . . . . . . . . 12
..^
|
342 | 340, 341 | syldan 487 |
. . . . . . . . . . 11
..^
|
343 | 278, 342 | fsumrecl 14465 |
. . . . . . . . . 10
..^
|
344 | | fzfid 12772 |
. . . . . . . . . . 11
..^ |
345 | | ssun2 3777 |
. . . . . . . . . . . . . . 15
|
346 | 345, 329 | syl5sseqr 3654 |
. . . . . . . . . . . . . 14
..^
|
347 | 346, 338 | sstrd 3613 |
. . . . . . . . . . . . 13
..^
|
348 | 347 | sselda 3603 |
. . . . . . . . . . . 12
..^
|
349 | 348, 341 | syldan 487 |
. . . . . . . . . . 11
..^
|
350 | 344, 349 | fsumrecl 14465 |
. . . . . . . . . 10
..^
|
351 | | le2add 10510 |
. . . . . . . . . 10
|
352 | 270, 277,
343, 350, 351 | syl22anc 1327 |
. . . . . . . . 9
..^
|
353 | 268, 352 | mpand 711 |
. . . . . . . 8
..^
|
354 | 233 | adantr 481 |
. . . . . . . . . . 11
..^ |
355 | | 1cnd 10056 |
. . . . . . . . . . 11
..^ |
356 | 272 | zcnd 11483 |
. . . . . . . . . . . 12
..^ |
357 | 230 | adantr 481 |
. . . . . . . . . . . 12
..^ |
358 | 356, 357 | subcld 10392 |
. . . . . . . . . . 11
..^ |
359 | 354, 355,
358 | adddid 10064 |
. . . . . . . . . 10
..^ |
360 | 355, 358 | addcomd 10238 |
. . . . . . . . . . . 12
..^ |
361 | 356, 355,
357 | addsubd 10413 |
. . . . . . . . . . . 12
..^ |
362 | 360, 361 | eqtr4d 2659 |
. . . . . . . . . . 11
..^ |
363 | 362 | oveq2d 6666 |
. . . . . . . . . 10
..^ |
364 | 354 | mulid1d 10057 |
. . . . . . . . . . 11
..^ |
365 | 364 | oveq1d 6665 |
. . . . . . . . . 10
..^ |
366 | 359, 363,
365 | 3eqtr3d 2664 |
. . . . . . . . 9
..^ |
367 | | reflcl 12597 |
. . . . . . . . . . . . 13
|
368 | 286, 367 | syl 17 |
. . . . . . . . . . . 12
..^
|
369 | 368 | ltp1d 10954 |
. . . . . . . . . . 11
..^
|
370 | | fzdisj 12368 |
. . . . . . . . . . 11
|
371 | 369, 370 | syl 17 |
. . . . . . . . . 10
..^ |
372 | | fzfid 12772 |
. . . . . . . . . 10
..^ |
373 | 338 | sselda 3603 |
. . . . . . . . . . . 12
..^
|
374 | 373, 341 | syldan 487 |
. . . . . . . . . . 11
..^
|
375 | 374 | recnd 10068 |
. . . . . . . . . 10
..^
|
376 | 371, 329,
372, 375 | fsumsplit 14471 |
. . . . . . . . 9
..^
|
377 | 366, 376 | breq12d 4666 |
. . . . . . . 8
..^
|
378 | 353, 377 | sylibrd 249 |
. . . . . . 7
..^
|
379 | 378 | expcom 451 |
. . . . . 6
..^
|
380 | 379 | a2d 29 |
. . . . 5
..^
|
381 | 199, 209,
219, 229, 265, 380 | fzind2 12586 |
. . . 4
|
382 | 189, 381 | mpcom 38 |
. . 3
|
383 | 65, 82, 261, 184 | fsumless 14528 |
. . 3
|
384 | 64, 187, 83, 382, 383 | letrd 10194 |
. 2
|
385 | 44, 64, 83, 172, 384 | letrd 10194 |
1
; |