Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . 6
|
2 | | ioossre 12235 |
. . . . . . . . . . . . . 14
|
3 | | pntpbnd1.y |
. . . . . . . . . . . . . 14
|
4 | 2, 3 | sseldi 3601 |
. . . . . . . . . . . . 13
|
5 | | 0red 10041 |
. . . . . . . . . . . . . 14
|
6 | | pntpbnd1.x |
. . . . . . . . . . . . . . . 16
|
7 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
|
8 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . 20
|
9 | | pntpbnd1.e |
. . . . . . . . . . . . . . . . . . . 20
|
10 | 8, 9 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . 19
|
11 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . . . 21
|
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
13 | 12 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
14 | 10, 13 | elrpd 11869 |
. . . . . . . . . . . . . . . . . 18
|
15 | | rerpdivcl 11861 |
. . . . . . . . . . . . . . . . . 18
|
16 | 7, 14, 15 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
|
17 | 16 | reefcld 14818 |
. . . . . . . . . . . . . . . 16
|
18 | 6, 17 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
|
19 | | efgt0 14833 |
. . . . . . . . . . . . . . . . 17
|
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
|
21 | 20, 6 | syl6breqr 4695 |
. . . . . . . . . . . . . . 15
|
22 | | eliooord 12233 |
. . . . . . . . . . . . . . . . 17
|
23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | simpld 475 |
. . . . . . . . . . . . . . 15
|
25 | 5, 18, 4, 21, 24 | lttrd 10198 |
. . . . . . . . . . . . . 14
|
26 | 5, 4, 25 | ltled 10185 |
. . . . . . . . . . . . 13
|
27 | | flge0nn0 12621 |
. . . . . . . . . . . . 13
|
28 | 4, 26, 27 | syl2anc 693 |
. . . . . . . . . . . 12
|
29 | | nn0p1nn 11332 |
. . . . . . . . . . . 12
|
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
|
31 | | elfzuz 12338 |
. . . . . . . . . . 11
|
32 | | eluznn 11758 |
. . . . . . . . . . 11
|
33 | 30, 31, 32 | syl2an 494 |
. . . . . . . . . 10
|
34 | 33 | nnrpd 11870 |
. . . . . . . . 9
|
35 | | pntpbnd.r |
. . . . . . . . . . 11
ψ |
36 | 35 | pntrf 25252 |
. . . . . . . . . 10
|
37 | 36 | ffvelrni 6358 |
. . . . . . . . 9
|
38 | 34, 37 | syl 17 |
. . . . . . . 8
|
39 | 33 | peano2nnd 11037 |
. . . . . . . . 9
|
40 | 33, 39 | nnmulcld 11068 |
. . . . . . . 8
|
41 | 38, 40 | nndivred 11069 |
. . . . . . 7
|
42 | 41 | adantlr 751 |
. . . . . 6
|
43 | 1, 42 | fsumrecl 14465 |
. . . . 5
|
44 | 38 | adantlr 751 |
. . . . . . 7
|
45 | | fveq2 6191 |
. . . . . . . . . 10
|
46 | 45 | breq2d 4665 |
. . . . . . . . 9
|
47 | 46 | rspccva 3308 |
. . . . . . . 8
|
48 | 47 | adantll 750 |
. . . . . . 7
|
49 | 40 | adantlr 751 |
. . . . . . . 8
|
50 | 49 | nnred 11035 |
. . . . . . 7
|
51 | 49 | nngt0d 11064 |
. . . . . . 7
|
52 | | divge0 10892 |
. . . . . . 7
|
53 | 44, 48, 50, 51, 52 | syl22anc 1327 |
. . . . . 6
|
54 | 1, 42, 53 | fsumge0 14527 |
. . . . 5
|
55 | 43, 54 | absidd 14161 |
. . . 4
|
56 | 42, 53 | absidd 14161 |
. . . . 5
|
57 | 56 | sumeq2dv 14433 |
. . . 4
|
58 | 55, 57 | eqtr4d 2659 |
. . 3
|
59 | | fzfid 12772 |
. . . . 5
|
60 | 41 | adantlr 751 |
. . . . . 6
|
61 | 60 | recnd 10068 |
. . . . 5
|
62 | 59, 61 | fsumneg 14519 |
. . . 4
|
63 | 38 | adantlr 751 |
. . . . . . . . . 10
|
64 | 63 | renegcld 10457 |
. . . . . . . . 9
|
65 | 45 | breq1d 4663 |
. . . . . . . . . . . 12
|
66 | 65 | rspccva 3308 |
. . . . . . . . . . 11
|
67 | 66 | adantll 750 |
. . . . . . . . . 10
|
68 | 63 | le0neg1d 10599 |
. . . . . . . . . 10
|
69 | 67, 68 | mpbid 222 |
. . . . . . . . 9
|
70 | 40 | adantlr 751 |
. . . . . . . . . 10
|
71 | 70 | nnred 11035 |
. . . . . . . . 9
|
72 | 70 | nngt0d 11064 |
. . . . . . . . 9
|
73 | | divge0 10892 |
. . . . . . . . 9
|
74 | 64, 69, 71, 72, 73 | syl22anc 1327 |
. . . . . . . 8
|
75 | 38 | recnd 10068 |
. . . . . . . . . 10
|
76 | 40 | nncnd 11036 |
. . . . . . . . . 10
|
77 | 40 | nnne0d 11065 |
. . . . . . . . . 10
|
78 | 75, 76, 77 | divnegd 10814 |
. . . . . . . . 9
|
79 | 78 | adantlr 751 |
. . . . . . . 8
|
80 | 74, 79 | breqtrrd 4681 |
. . . . . . 7
|
81 | 60 | le0neg1d 10599 |
. . . . . . 7
|
82 | 80, 81 | mpbird 247 |
. . . . . 6
|
83 | 60, 82 | absnidd 14152 |
. . . . 5
|
84 | 83 | sumeq2dv 14433 |
. . . 4
|
85 | 59, 60 | fsumrecl 14465 |
. . . . 5
|
86 | 60 | renegcld 10457 |
. . . . . . . 8
|
87 | 59, 86, 80 | fsumge0 14527 |
. . . . . . 7
|
88 | 87, 62 | breqtrd 4679 |
. . . . . 6
|
89 | 85 | le0neg1d 10599 |
. . . . . 6
|
90 | 88, 89 | mpbird 247 |
. . . . 5
|
91 | 85, 90 | absnidd 14152 |
. . . 4
|
92 | 62, 84, 91 | 3eqtr4rd 2667 |
. . 3
|
93 | | pntpbnd1.c |
. . . . . . . . . . . . 13
|
94 | | pntpbnd1.1 |
. . . . . . . . . . . . . 14
|
95 | | 2rp 11837 |
. . . . . . . . . . . . . 14
|
96 | | rpaddcl 11854 |
. . . . . . . . . . . . . 14
|
97 | 94, 95, 96 | sylancl 694 |
. . . . . . . . . . . . 13
|
98 | 93, 97 | syl5eqel 2705 |
. . . . . . . . . . . 12
|
99 | 98, 14 | rpdivcld 11889 |
. . . . . . . . . . 11
|
100 | 99 | rpred 11872 |
. . . . . . . . . 10
|
101 | 100 | reefcld 14818 |
. . . . . . . . 9
|
102 | | pnfxr 10092 |
. . . . . . . . 9
|
103 | | icossre 12254 |
. . . . . . . . 9
|
104 | 101, 102,
103 | sylancl 694 |
. . . . . . . 8
|
105 | | pntpbnd1.k |
. . . . . . . 8
|
106 | 104, 105 | sseldd 3604 |
. . . . . . 7
|
107 | 106, 4 | remulcld 10070 |
. . . . . 6
|
108 | 4 | recnd 10068 |
. . . . . . . . 9
|
109 | 108 | mulid2d 10058 |
. . . . . . . 8
|
110 | | 1red 10055 |
. . . . . . . . . 10
|
111 | | efgt1 14846 |
. . . . . . . . . . 11
|
112 | 99, 111 | syl 17 |
. . . . . . . . . 10
|
113 | | elicopnf 12269 |
. . . . . . . . . . . . 13
|
114 | 101, 113 | syl 17 |
. . . . . . . . . . . 12
|
115 | 114 | simplbda 654 |
. . . . . . . . . . 11
|
116 | 105, 115 | mpdan 702 |
. . . . . . . . . 10
|
117 | 110, 101,
106, 112, 116 | ltletrd 10197 |
. . . . . . . . 9
|
118 | | ltmul1 10873 |
. . . . . . . . . 10
|
119 | 110, 106,
4, 25, 118 | syl112anc 1330 |
. . . . . . . . 9
|
120 | 117, 119 | mpbid 222 |
. . . . . . . 8
|
121 | 109, 120 | eqbrtrrd 4677 |
. . . . . . 7
|
122 | 4, 107, 121 | ltled 10185 |
. . . . . 6
|
123 | | flword2 12614 |
. . . . . 6
|
124 | 4, 107, 122, 123 | syl3anc 1326 |
. . . . 5
|
125 | 107 | flcld 12599 |
. . . . . 6
|
126 | | uzid 11702 |
. . . . . 6
|
127 | 125, 126 | syl 17 |
. . . . 5
|
128 | | elfzuzb 12336 |
. . . . 5
|
129 | 124, 127,
128 | sylanbrc 698 |
. . . 4
|
130 | | oveq2 6658 |
. . . . . . . 8
|
131 | 130 | raleqdv 3144 |
. . . . . . 7
|
132 | 130 | raleqdv 3144 |
. . . . . . 7
|
133 | 131, 132 | orbi12d 746 |
. . . . . 6
|
134 | 133 | imbi2d 330 |
. . . . 5
|
135 | | oveq2 6658 |
. . . . . . . 8
|
136 | 135 | raleqdv 3144 |
. . . . . . 7
|
137 | 135 | raleqdv 3144 |
. . . . . . 7
|
138 | 136, 137 | orbi12d 746 |
. . . . . 6
|
139 | 138 | imbi2d 330 |
. . . . 5
|
140 | | oveq2 6658 |
. . . . . . . 8
|
141 | 140 | raleqdv 3144 |
. . . . . . 7
|
142 | 140 | raleqdv 3144 |
. . . . . . 7
|
143 | 141, 142 | orbi12d 746 |
. . . . . 6
|
144 | 143 | imbi2d 330 |
. . . . 5
|
145 | | oveq2 6658 |
. . . . . . . 8
|
146 | 145 | raleqdv 3144 |
. . . . . . 7
|
147 | 145 | raleqdv 3144 |
. . . . . . 7
|
148 | 146, 147 | orbi12d 746 |
. . . . . 6
|
149 | 148 | imbi2d 330 |
. . . . 5
|
150 | | elfzle3 12347 |
. . . . . . . . 9
|
151 | | elfzel2 12340 |
. . . . . . . . . . . 12
|
152 | 151 | zred 11482 |
. . . . . . . . . . 11
|
153 | 152 | ltp1d 10954 |
. . . . . . . . . 10
|
154 | | peano2re 10209 |
. . . . . . . . . . . 12
|
155 | 152, 154 | syl 17 |
. . . . . . . . . . 11
|
156 | 152, 155 | ltnled 10184 |
. . . . . . . . . 10
|
157 | 153, 156 | mpbid 222 |
. . . . . . . . 9
|
158 | 150, 157 | pm2.21dd 186 |
. . . . . . . 8
|
159 | 158 | rgen 2922 |
. . . . . . 7
|
160 | 159 | olci 406 |
. . . . . 6
|
161 | 160 | 2a1i 12 |
. . . . 5
|
162 | | elfzofz 12485 |
. . . . . . . . . 10
..^
|
163 | | elfzp12 12419 |
. . . . . . . . . . 11
|
164 | 124, 163 | syl 17 |
. . . . . . . . . 10
|
165 | 162, 164 | syl5ib 234 |
. . . . . . . . 9
..^
|
166 | 165 | imp 445 |
. . . . . . . 8
..^
|
167 | 30 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
168 | 36 | ffvelrni 6358 |
. . . . . . . . . . . . . 14
|
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . 13
|
170 | 5, 169 | letrid 10189 |
. . . . . . . . . . . 12
|
171 | 170 | adantr 481 |
. . . . . . . . . . 11
|
172 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
173 | 172 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
174 | 4 | flcld 12599 |
. . . . . . . . . . . . . . . . 17
|
175 | 174 | peano2zd 11485 |
. . . . . . . . . . . . . . . 16
|
176 | | fzsn 12383 |
. . . . . . . . . . . . . . . 16
|
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . 15
|
178 | 173, 177 | sylan9eqr 2678 |
. . . . . . . . . . . . . 14
|
179 | 178 | raleqdv 3144 |
. . . . . . . . . . . . 13
|
180 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
181 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
182 | 181 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
183 | 180, 182 | ralsn 4222 |
. . . . . . . . . . . . 13
|
184 | 179, 183 | syl6bb 276 |
. . . . . . . . . . . 12
|
185 | 178 | raleqdv 3144 |
. . . . . . . . . . . . 13
|
186 | 181 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
187 | 180, 186 | ralsn 4222 |
. . . . . . . . . . . . 13
|
188 | 185, 187 | syl6bb 276 |
. . . . . . . . . . . 12
|
189 | 184, 188 | orbi12d 746 |
. . . . . . . . . . 11
|
190 | 171, 189 | mpbird 247 |
. . . . . . . . . 10
|
191 | 190 | a1d 25 |
. . . . . . . . 9
|
192 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . 17
|
193 | 192 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
194 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . 16
|
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . 15
|
196 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
197 | 196 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
|
198 | 197 | rspcv 3305 |
. . . . . . . . . . . . . . 15
|
199 | 195, 198 | syl 17 |
. . . . . . . . . . . . . 14
|
200 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . . . 19
|
201 | 200 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
202 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . . . . 21
|
203 | 30, 192, 202 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
|
204 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
205 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
206 | 205 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
207 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
208 | | zltp1le 11427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
209 | 174, 207,
208 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
210 | 206, 209 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
|
211 | | fllt 12607 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
212 | 4, 207, 211 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
213 | 210, 212 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
|
214 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
215 | 214 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
216 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
217 | 107, 207,
216 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
218 | 215, 217 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
|
219 | 213, 218 | jca 554 |
. . . . . . . . . . . . . . . . . . . 20
|
220 | 219 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
221 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
222 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
223 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
224 | 35, 221, 6, 222, 204, 220, 223 | pntpbnd1a 25274 |
. . . . . . . . . . . . . . . . . . 19
|
225 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
226 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
227 | 225, 226 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
|
228 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
229 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
230 | 228, 229 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
231 | 230 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
232 | 231 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
|
233 | 227, 232 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
234 | 233 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
|
235 | 204, 220,
224, 234 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . 18
|
236 | 201, 235 | mtand 691 |
. . . . . . . . . . . . . . . . 17
|
237 | 236 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
238 | 203 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
239 | 36 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
241 | 240 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
242 | 241 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
243 | 242 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . 19
|
244 | 203 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
245 | 244 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . 22
|
246 | 36 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . . . 22
|
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
248 | 247 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
249 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . 20
|
250 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
251 | | letric 10137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
252 | 250, 247,
251 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
253 | 252 | ord 392 |
. . . . . . . . . . . . . . . . . . . . . 22
|
254 | 253 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
|
255 | 254 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . 20
|
256 | 248, 249,
241, 255 | lesub2dd 10644 |
. . . . . . . . . . . . . . . . . . 19
|
257 | 243, 256 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . 18
|
258 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
|
259 | 241, 258 | absidd 14161 |
. . . . . . . . . . . . . . . . . 18
|
260 | 248, 249,
241, 255, 258 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
|
261 | 248, 241,
260 | abssuble0d 14171 |
. . . . . . . . . . . . . . . . . 18
|
262 | 257, 259,
261 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
|
263 | 262 | expr 643 |
. . . . . . . . . . . . . . . 16
|
264 | 237, 263 | mt3d 140 |
. . . . . . . . . . . . . . 15
|
265 | 264 | ex 450 |
. . . . . . . . . . . . . 14
|
266 | 199, 265 | syld 47 |
. . . . . . . . . . . . 13
|
267 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
268 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
269 | 268 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
270 | 267, 269 | ralsn 4222 |
. . . . . . . . . . . . 13
|
271 | 266, 270 | syl6ibr 242 |
. . . . . . . . . . . 12
|
272 | 271 | ancld 576 |
. . . . . . . . . . 11
|
273 | | fzsuc 12388 |
. . . . . . . . . . . . . 14
|
274 | 193, 273 | syl 17 |
. . . . . . . . . . . . 13
|
275 | 274 | raleqdv 3144 |
. . . . . . . . . . . 12
|
276 | | ralunb 3794 |
. . . . . . . . . . . 12
|
277 | 275, 276 | syl6bb 276 |
. . . . . . . . . . 11
|
278 | 272, 277 | sylibrd 249 |
. . . . . . . . . 10
|
279 | 196 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
280 | 279 | rspcv 3305 |
. . . . . . . . . . . . . . 15
|
281 | 195, 280 | syl 17 |
. . . . . . . . . . . . . 14
|
282 | 236 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
283 | 253 | con1d 139 |
. . . . . . . . . . . . . . . . . . . . . 22
|
284 | 283 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
|
285 | 284 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . 20
|
286 | 240 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
287 | 286 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . . 21
|
288 | 247 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
289 | 287, 288 | addge02d 10616 |
. . . . . . . . . . . . . . . . . . . 20
|
290 | 285, 289 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
|
291 | 288 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
292 | 286 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
293 | 291, 292 | negsubd 10398 |
. . . . . . . . . . . . . . . . . . 19
|
294 | 290, 293 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
|
295 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
|
296 | 286, 295 | absnidd 14152 |
. . . . . . . . . . . . . . . . . 18
|
297 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . 20
|
298 | 286, 297,
288, 295, 285 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
|
299 | 286, 288,
298 | abssubge0d 14170 |
. . . . . . . . . . . . . . . . . 18
|
300 | 294, 296,
299 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
|
301 | 300 | expr 643 |
. . . . . . . . . . . . . . . 16
|
302 | 282, 301 | mt3d 140 |
. . . . . . . . . . . . . . 15
|
303 | 302 | ex 450 |
. . . . . . . . . . . . . 14
|
304 | 281, 303 | syld 47 |
. . . . . . . . . . . . 13
|
305 | 268 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
306 | 267, 305 | ralsn 4222 |
. . . . . . . . . . . . 13
|
307 | 304, 306 | syl6ibr 242 |
. . . . . . . . . . . 12
|
308 | 307 | ancld 576 |
. . . . . . . . . . 11
|
309 | 274 | raleqdv 3144 |
. . . . . . . . . . . 12
|
310 | | ralunb 3794 |
. . . . . . . . . . . 12
|
311 | 309, 310 | syl6bb 276 |
. . . . . . . . . . 11
|
312 | 308, 311 | sylibrd 249 |
. . . . . . . . . 10
|
313 | 278, 312 | orim12d 883 |
. . . . . . . . 9
|
314 | 191, 313 | jaodan 826 |
. . . . . . . 8
|
315 | 166, 314 | syldan 487 |
. . . . . . 7
..^
|
316 | 315 | expcom 451 |
. . . . . 6
..^
|
317 | 316 | a2d 29 |
. . . . 5
..^
|
318 | 134, 139,
144, 149, 161, 317 | fzind2 12586 |
. . . 4
|
319 | 129, 318 | mpcom 38 |
. . 3
|
320 | 58, 92, 319 | mpjaodan 827 |
. 2
|
321 | | pntpbnd1.2 |
. . 3
|
322 | | fveq2 6191 |
. . . . . . . . 9
|
323 | | id 22 |
. . . . . . . . . 10
|
324 | | oveq1 6657 |
. . . . . . . . . 10
|
325 | 323, 324 | oveq12d 6668 |
. . . . . . . . 9
|
326 | 322, 325 | oveq12d 6668 |
. . . . . . . 8
|
327 | 326 | cbvsumv 14426 |
. . . . . . 7
|
328 | | oveq1 6657 |
. . . . . . . 8
|
329 | 328 | sumeq1d 14431 |
. . . . . . 7
|
330 | 327, 329 | syl5eq 2668 |
. . . . . 6
|
331 | 330 | fveq2d 6195 |
. . . . 5
|
332 | 331 | breq1d 4663 |
. . . 4
|
333 | | oveq2 6658 |
. . . . . . 7
|
334 | 333 | sumeq1d 14431 |
. . . . . 6
|
335 | 334 | fveq2d 6195 |
. . . . 5
|
336 | 335 | breq1d 4663 |
. . . 4
|
337 | 332, 336 | rspc2va 3323 |
. . 3
|
338 | 30, 125, 321, 337 | syl21anc 1325 |
. 2
|
339 | 320, 338 | eqbrtrrd 4677 |
1
|