Proof of Theorem pntrlog2bndlem5
Step | Hyp | Ref
| Expression |
1 | | elioore 12205 |
. . . . . . . . . . . . 13
|
2 | 1 | adantl 482 |
. . . . . . . . . . . 12
|
3 | | 1rp 11836 |
. . . . . . . . . . . . 13
|
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
|
5 | | 1red 10055 |
. . . . . . . . . . . . 13
|
6 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
|
7 | 6 | adantl 482 |
. . . . . . . . . . . . . 14
|
8 | 7 | simpld 475 |
. . . . . . . . . . . . 13
|
9 | 5, 2, 8 | ltled 10185 |
. . . . . . . . . . . 12
|
10 | 2, 4, 9 | rpgecld 11911 |
. . . . . . . . . . 11
|
11 | | pntrlog2bnd.r |
. . . . . . . . . . . . 13
ψ |
12 | 11 | pntrf 25252 |
. . . . . . . . . . . 12
|
13 | 12 | ffvelrni 6358 |
. . . . . . . . . . 11
|
14 | 10, 13 | syl 17 |
. . . . . . . . . 10
|
15 | 14 | recnd 10068 |
. . . . . . . . 9
|
16 | 15 | abscld 14175 |
. . . . . . . 8
|
17 | 16 | recnd 10068 |
. . . . . . 7
|
18 | 10 | relogcld 24369 |
. . . . . . . 8
|
19 | 18 | recnd 10068 |
. . . . . . 7
|
20 | 17, 19 | mulcld 10060 |
. . . . . 6
|
21 | | 2cnd 11093 |
. . . . . . . 8
|
22 | 2, 8 | rplogcld 24375 |
. . . . . . . . 9
|
23 | 22 | rpne0d 11877 |
. . . . . . . 8
|
24 | 21, 19, 23 | divcld 10801 |
. . . . . . 7
|
25 | | fzfid 12772 |
. . . . . . . 8
|
26 | 10 | adantr 481 |
. . . . . . . . . . . . . 14
|
27 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
|
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . 15
|
29 | 28 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
30 | 26, 29 | rpdivcld 11889 |
. . . . . . . . . . . . 13
|
31 | 12 | ffvelrni 6358 |
. . . . . . . . . . . . 13
|
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
|
33 | 32 | recnd 10068 |
. . . . . . . . . . 11
|
34 | 33 | abscld 14175 |
. . . . . . . . . 10
|
35 | 29 | relogcld 24369 |
. . . . . . . . . . 11
|
36 | | 1red 10055 |
. . . . . . . . . . 11
|
37 | 35, 36 | readdcld 10069 |
. . . . . . . . . 10
|
38 | 34, 37 | remulcld 10070 |
. . . . . . . . 9
|
39 | 38 | recnd 10068 |
. . . . . . . 8
|
40 | 25, 39 | fsumcl 14464 |
. . . . . . 7
|
41 | 24, 40 | mulcld 10060 |
. . . . . 6
|
42 | 20, 41 | subcld 10392 |
. . . . 5
|
43 | 34 | recnd 10068 |
. . . . . . 7
|
44 | 25, 43 | fsumcl 14464 |
. . . . . 6
|
45 | 24, 44 | mulcld 10060 |
. . . . 5
|
46 | 2 | recnd 10068 |
. . . . 5
|
47 | 10 | rpne0d 11877 |
. . . . 5
|
48 | 42, 45, 46, 47 | divdird 10839 |
. . . 4
|
49 | 16, 18 | remulcld 10070 |
. . . . . . . 8
|
50 | 49 | recnd 10068 |
. . . . . . 7
|
51 | 50, 41, 45 | subsubd 10420 |
. . . . . 6
|
52 | 24, 40, 44 | subdid 10486 |
. . . . . . . 8
|
53 | 25, 39, 43 | fsumsub 14520 |
. . . . . . . . . 10
|
54 | 37 | recnd 10068 |
. . . . . . . . . . . . 13
|
55 | | 1cnd 10056 |
. . . . . . . . . . . . 13
|
56 | 43, 54, 55 | subdid 10486 |
. . . . . . . . . . . 12
|
57 | 35 | recnd 10068 |
. . . . . . . . . . . . . 14
|
58 | 57, 55 | pncand 10393 |
. . . . . . . . . . . . 13
|
59 | 58 | oveq2d 6666 |
. . . . . . . . . . . 12
|
60 | 43 | mulid1d 10057 |
. . . . . . . . . . . . 13
|
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . 12
|
62 | 56, 59, 61 | 3eqtr3rd 2665 |
. . . . . . . . . . 11
|
63 | 62 | sumeq2dv 14433 |
. . . . . . . . . 10
|
64 | 53, 63 | eqtr3d 2658 |
. . . . . . . . 9
|
65 | 64 | oveq2d 6666 |
. . . . . . . 8
|
66 | 52, 65 | eqtr3d 2658 |
. . . . . . 7
|
67 | 66 | oveq2d 6666 |
. . . . . 6
|
68 | 51, 67 | eqtr3d 2658 |
. . . . 5
|
69 | 68 | oveq1d 6665 |
. . . 4
|
70 | 48, 69 | eqtr3d 2658 |
. . 3
|
71 | 70 | mpteq2dva 4744 |
. 2
|
72 | | 2re 11090 |
. . . . . . . 8
|
73 | 72 | a1i 11 |
. . . . . . 7
|
74 | 73, 22 | rerpdivcld 11903 |
. . . . . 6
|
75 | 25, 38 | fsumrecl 14465 |
. . . . . 6
|
76 | 74, 75 | remulcld 10070 |
. . . . 5
|
77 | 49, 76 | resubcld 10458 |
. . . 4
|
78 | 77, 10 | rerpdivcld 11903 |
. . 3
|
79 | 25, 34 | fsumrecl 14465 |
. . . . 5
|
80 | 74, 79 | remulcld 10070 |
. . . 4
|
81 | 80, 10 | rerpdivcld 11903 |
. . 3
|
82 | | 1red 10055 |
. . . 4
|
83 | | pntsval.1 |
. . . . . 6
Λ ψ |
84 | | pntrlog2bnd.t |
. . . . . 6
|
85 | 83, 11, 84 | pntrlog2bndlem4 25269 |
. . . . 5
|
86 | 85 | a1i 11 |
. . . 4
|
87 | 28 | nnred 11035 |
. . . . . . . . . . 11
|
88 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
89 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
90 | 89 | relogcld 24369 |
. . . . . . . . . . . . . . 15
|
91 | 88, 90 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
92 | | 0red 10041 |
. . . . . . . . . . . . . 14
|
93 | 91, 92 | ifclda 4120 |
. . . . . . . . . . . . 13
|
94 | 84, 93 | fmpti 6383 |
. . . . . . . . . . . 12
|
95 | 94 | ffvelrni 6358 |
. . . . . . . . . . 11
|
96 | 87, 95 | syl 17 |
. . . . . . . . . 10
|
97 | 87, 36 | resubcld 10458 |
. . . . . . . . . . 11
|
98 | 94 | ffvelrni 6358 |
. . . . . . . . . . 11
|
99 | 97, 98 | syl 17 |
. . . . . . . . . 10
|
100 | 96, 99 | resubcld 10458 |
. . . . . . . . 9
|
101 | 34, 100 | remulcld 10070 |
. . . . . . . 8
|
102 | 25, 101 | fsumrecl 14465 |
. . . . . . 7
|
103 | 74, 102 | remulcld 10070 |
. . . . . 6
|
104 | 49, 103 | resubcld 10458 |
. . . . 5
|
105 | 104, 10 | rerpdivcld 11903 |
. . . 4
|
106 | | 2rp 11837 |
. . . . . . . . . . 11
|
107 | 106 | a1i 11 |
. . . . . . . . . 10
|
108 | 107 | rpge0d 11876 |
. . . . . . . . 9
|
109 | 73, 22, 108 | divge0d 11912 |
. . . . . . . 8
|
110 | 33 | absge0d 14183 |
. . . . . . . . . 10
|
111 | 29 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
112 | 111 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
113 | 57 | adantr 481 |
. . . . . . . . . . . . . . 15
|
114 | 112, 113 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
115 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
116 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . 19
|
117 | 111 | rpred 11872 |
. . . . . . . . . . . . . . . . . . 19
|
118 | | difrp 11868 |
. . . . . . . . . . . . . . . . . . 19
|
119 | 116, 117,
118 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
120 | 115, 119 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | relogcld 24369 |
. . . . . . . . . . . . . . . 16
|
122 | 121 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
123 | 112, 122 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
124 | 114, 123,
122 | subsubd 10420 |
. . . . . . . . . . . . 13
|
125 | | rpre 11839 |
. . . . . . . . . . . . . . . . 17
|
126 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
|
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
|
128 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 127, 128 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
130 | 126, 129 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . 18
|
131 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
|
132 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 131, 132 | ifex 4156 |
. . . . . . . . . . . . . . . . . 18
|
134 | 130, 84, 133 | fvmpt 6282 |
. . . . . . . . . . . . . . . . 17
|
135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . 16
|
136 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
137 | 135, 136 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
138 | 111, 137 | syl 17 |
. . . . . . . . . . . . . 14
|
139 | | rpre 11839 |
. . . . . . . . . . . . . . . . . 18
|
140 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
|
142 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
143 | 141, 142 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | 140, 143 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . 19
|
145 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
|
146 | 145, 132 | ifex 4156 |
. . . . . . . . . . . . . . . . . . 19
|
147 | 144, 84, 146 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
|
148 | 139, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
149 | | iftrue 4092 |
. . . . . . . . . . . . . . . . 17
|
150 | 148, 149 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
151 | 120, 150 | syl 17 |
. . . . . . . . . . . . . . 15
|
152 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
153 | 112, 152,
122 | subdird 10487 |
. . . . . . . . . . . . . . 15
|
154 | 122 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
|
155 | 154 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
156 | 151, 153,
155 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
157 | 138, 156 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
158 | 112, 113,
122 | subdid 10486 |
. . . . . . . . . . . . . 14
|
159 | 158 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
160 | 124, 157,
159 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
|
161 | 111 | relogcld 24369 |
. . . . . . . . . . . . . . . . . 18
|
162 | 161, 121 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
|
163 | 162 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
164 | 112, 152,
163 | subdird 10487 |
. . . . . . . . . . . . . . 15
|
165 | 163 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
|
166 | 165 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
167 | 117, 162 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
|
168 | 167 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
169 | 168, 113,
122 | subsub3d 10422 |
. . . . . . . . . . . . . . 15
|
170 | 164, 166,
169 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
171 | 112, 152 | npcand 10396 |
. . . . . . . . . . . . . . . . . 18
|
172 | 171 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
173 | 172 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
174 | | logdifbnd 24720 |
. . . . . . . . . . . . . . . . 17
|
175 | 120, 174 | syl 17 |
. . . . . . . . . . . . . . . 16
|
176 | 173, 175 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . 15
|
177 | | 1red 10055 |
. . . . . . . . . . . . . . . 16
|
178 | 162, 177,
120 | lemuldiv2d 11922 |
. . . . . . . . . . . . . . 15
|
179 | 176, 178 | mpbird 247 |
. . . . . . . . . . . . . 14
|
180 | 170, 179 | eqbrtrrd 4677 |
. . . . . . . . . . . . 13
|
181 | 167, 121 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
182 | 181, 161,
177 | lesubadd2d 10626 |
. . . . . . . . . . . . 13
|
183 | 180, 182 | mpbid 222 |
. . . . . . . . . . . 12
|
184 | 160, 183 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
185 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
186 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
|
187 | 186, 3 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . . 21
|
188 | 187 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . 20
|
189 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
190 | | log1 24332 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
191 | 189, 190 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
|
192 | 186, 191 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
|
193 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . 22
|
194 | 193 | mul01i 10226 |
. . . . . . . . . . . . . . . . . . . . 21
|
195 | 192, 194 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . 20
|
196 | 188, 195 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
197 | 196, 84, 132 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
|
198 | 116, 197 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
199 | 185, 198 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
200 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
201 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . . . 19
|
202 | 200, 201 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
|
203 | 202 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
204 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
|
205 | | rpne0 11848 |
. . . . . . . . . . . . . . . . . . . . 21
|
206 | 205 | necon2bi 2824 |
. . . . . . . . . . . . . . . . . . . 20
|
207 | 206 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 207, 84, 132 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
|
209 | 204, 208 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
210 | 203, 209 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
211 | 199, 210 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
212 | | 0m0e0 11130 |
. . . . . . . . . . . . . . 15
|
213 | 211, 212 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
214 | 213 | eqcoms 2630 |
. . . . . . . . . . . . 13
|
215 | 214 | adantl 482 |
. . . . . . . . . . . 12
|
216 | | 0red 10041 |
. . . . . . . . . . . . . 14
|
217 | 28 | nnge1d 11063 |
. . . . . . . . . . . . . . 15
|
218 | 87, 217 | logge0d 24376 |
. . . . . . . . . . . . . 14
|
219 | 35 | lep1d 10955 |
. . . . . . . . . . . . . 14
|
220 | 216, 35, 37, 218, 219 | letrd 10194 |
. . . . . . . . . . . . 13
|
221 | 220 | adantr 481 |
. . . . . . . . . . . 12
|
222 | 215, 221 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
223 | | elfzle1 12344 |
. . . . . . . . . . . . 13
|
224 | 223 | adantl 482 |
. . . . . . . . . . . 12
|
225 | 36, 87 | leloed 10180 |
. . . . . . . . . . . 12
|
226 | 224, 225 | mpbid 222 |
. . . . . . . . . . 11
|
227 | 184, 222,
226 | mpjaodan 827 |
. . . . . . . . . 10
|
228 | 100, 37, 34, 110, 227 | lemul2ad 10964 |
. . . . . . . . 9
|
229 | 25, 101, 38, 228 | fsumle 14531 |
. . . . . . . 8
|
230 | 102, 75, 74, 109, 229 | lemul2ad 10964 |
. . . . . . 7
|
231 | 103, 76, 49, 230 | lesub2dd 10644 |
. . . . . 6
|
232 | 77, 104, 10, 231 | lediv1dd 11930 |
. . . . 5
|
233 | 232 | adantrr 753 |
. . . 4
|
234 | 82, 86, 105, 78, 233 | lo1le 14382 |
. . 3
|
235 | 106 | a1i 11 |
. . . . . . . 8
|
236 | | pntrlog2bndlem5.1 |
. . . . . . . 8
|
237 | 235, 236 | rpmulcld 11888 |
. . . . . . 7
|
238 | 237 | rpred 11872 |
. . . . . 6
|
239 | 238 | adantr 481 |
. . . . 5
|
240 | 5, 22 | rerpdivcld 11903 |
. . . . . 6
|
241 | 5, 240 | readdcld 10069 |
. . . . 5
|
242 | | ioossre 12235 |
. . . . . 6
|
243 | | lo1const 14351 |
. . . . . 6
|
244 | 242, 238,
243 | sylancr 695 |
. . . . 5
|
245 | | lo1const 14351 |
. . . . . . 7
|
246 | 242, 82, 245 | sylancr 695 |
. . . . . 6
|
247 | | divlogrlim 24381 |
. . . . . . . 8
|
248 | | rlimo1 14347 |
. . . . . . . 8
|
249 | 247, 248 | mp1i 13 |
. . . . . . 7
|
250 | 240, 249 | o1lo1d 14270 |
. . . . . 6
|
251 | 5, 240, 246, 250 | lo1add 14357 |
. . . . 5
|
252 | 237 | adantr 481 |
. . . . . 6
|
253 | 252 | rpge0d 11876 |
. . . . 5
|
254 | 239, 241,
244, 251, 253 | lo1mul 14358 |
. . . 4
|
255 | 239, 241 | remulcld 10070 |
. . . 4
|
256 | 79, 10 | rerpdivcld 11903 |
. . . . . . 7
|
257 | 18, 5 | readdcld 10069 |
. . . . . . . 8
|
258 | 236 | adantr 481 |
. . . . . . . . 9
|
259 | 258 | rpred 11872 |
. . . . . . . 8
|
260 | 257, 259 | remulcld 10070 |
. . . . . . 7
|
261 | 28 | nnrecred 11066 |
. . . . . . . . . 10
|
262 | 25, 261 | fsumrecl 14465 |
. . . . . . . . 9
|
263 | 262, 259 | remulcld 10070 |
. . . . . . . 8
|
264 | 34, 26 | rerpdivcld 11903 |
. . . . . . . . . 10
|
265 | 259 | adantr 481 |
. . . . . . . . . . 11
|
266 | 261, 265 | remulcld 10070 |
. . . . . . . . . 10
|
267 | 30 | rpcnd 11874 |
. . . . . . . . . . . . . . . 16
|
268 | 30 | rpne0d 11877 |
. . . . . . . . . . . . . . . 16
|
269 | 33, 267, 268 | absdivd 14194 |
. . . . . . . . . . . . . . 15
|
270 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
271 | 270, 28 | nndivred 11069 |
. . . . . . . . . . . . . . . . 17
|
272 | 30 | rpge0d 11876 |
. . . . . . . . . . . . . . . . 17
|
273 | 271, 272 | absidd 14161 |
. . . . . . . . . . . . . . . 16
|
274 | 273 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
275 | 269, 274 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
276 | 46 | adantr 481 |
. . . . . . . . . . . . . . 15
|
277 | 87 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
278 | 47 | adantr 481 |
. . . . . . . . . . . . . . 15
|
279 | 28 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
|
280 | 43, 276, 277, 278, 279 | divdiv2d 10833 |
. . . . . . . . . . . . . 14
|
281 | 43, 277, 276, 278 | div23d 10838 |
. . . . . . . . . . . . . 14
|
282 | 275, 280,
281 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
283 | | pntrlog2bndlem5.2 |
. . . . . . . . . . . . . . 15
|
284 | 283 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
285 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
286 | | id 22 |
. . . . . . . . . . . . . . . . . 18
|
287 | 285, 286 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
288 | 287 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
289 | 288 | breq1d 4663 |
. . . . . . . . . . . . . . 15
|
290 | 289 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
291 | 30, 284, 290 | sylc 65 |
. . . . . . . . . . . . 13
|
292 | 282, 291 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
|
293 | 264, 265,
29 | lemuldivd 11921 |
. . . . . . . . . . . 12
|
294 | 292, 293 | mpbid 222 |
. . . . . . . . . . 11
|
295 | 265 | recnd 10068 |
. . . . . . . . . . . 12
|
296 | 295, 277,
279 | divrec2d 10805 |
. . . . . . . . . . 11
|
297 | 294, 296 | breqtrd 4679 |
. . . . . . . . . 10
|
298 | 25, 264, 266, 297 | fsumle 14531 |
. . . . . . . . 9
|
299 | 25, 46, 43, 47 | fsumdivc 14518 |
. . . . . . . . 9
|
300 | 258 | rpcnd 11874 |
. . . . . . . . . 10
|
301 | 261 | recnd 10068 |
. . . . . . . . . 10
|
302 | 25, 300, 301 | fsummulc1 14517 |
. . . . . . . . 9
|
303 | 298, 299,
302 | 3brtr4d 4685 |
. . . . . . . 8
|
304 | 258 | rpge0d 11876 |
. . . . . . . . 9
|
305 | | harmonicubnd 24736 |
. . . . . . . . . 10
|
306 | 2, 9, 305 | syl2anc 693 |
. . . . . . . . 9
|
307 | 262, 257,
259, 304, 306 | lemul1ad 10963 |
. . . . . . . 8
|
308 | 256, 263,
260, 303, 307 | letrd 10194 |
. . . . . . 7
|
309 | 256, 260,
74, 109, 308 | lemul2ad 10964 |
. . . . . 6
|
310 | 24, 44, 46, 47 | divassd 10836 |
. . . . . 6
|
311 | 241 | recnd 10068 |
. . . . . . . 8
|
312 | 21, 300, 311 | mul32d 10246 |
. . . . . . 7
|
313 | | 1cnd 10056 |
. . . . . . . . . . . 12
|
314 | 19, 313, 19, 23 | divdird 10839 |
. . . . . . . . . . 11
|
315 | 19, 23 | dividd 10799 |
. . . . . . . . . . . 12
|
316 | 315 | oveq1d 6665 |
. . . . . . . . . . 11
|
317 | 314, 316 | eqtr2d 2657 |
. . . . . . . . . 10
|
318 | 317 | oveq2d 6666 |
. . . . . . . . 9
|
319 | 19, 313 | addcld 10059 |
. . . . . . . . . 10
|
320 | 21, 19, 319, 23 | div32d 10824 |
. . . . . . . . 9
|
321 | 318, 320 | eqtr4d 2659 |
. . . . . . . 8
|
322 | 321 | oveq1d 6665 |
. . . . . . 7
|
323 | 24, 319, 300 | mulassd 10063 |
. . . . . . 7
|
324 | 312, 322,
323 | 3eqtrd 2660 |
. . . . . 6
|
325 | 309, 310,
324 | 3brtr4d 4685 |
. . . . 5
|
326 | 325 | adantrr 753 |
. . . 4
|
327 | 82, 254, 255, 81, 326 | lo1le 14382 |
. . 3
|
328 | 78, 81, 234, 327 | lo1add 14357 |
. 2
|
329 | 71, 328 | eqeltrrd 2702 |
1
|