Step | Hyp | Ref
| Expression |
1 | | hgt750leme.n |
. . . . . 6
|
2 | 1 | nnnn0d 11351 |
. . . . 5
|
3 | | 3nn0 11310 |
. . . . . 6
|
4 | 3 | a1i 11 |
. . . . 5
|
5 | | ssid 3624 |
. . . . . 6
|
6 | 5 | a1i 11 |
. . . . 5
|
7 | 2, 4, 6 | reprfi2 30701 |
. . . 4
repr |
8 | | hgt750lemb.a |
. . . . 5
repr |
9 | 8 | ssrab3 3688 |
. . . 4
repr |
10 | | ssfi 8180 |
. . . 4
repr repr
|
11 | 7, 9, 10 | sylancl 694 |
. . 3
|
12 | | vmaf 24845 |
. . . . . 6
Λ |
13 | 12 | a1i 11 |
. . . . 5
Λ |
14 | 5 | a1i 11 |
. . . . . . 7
|
15 | 1 | nnzd 11481 |
. . . . . . . 8
|
16 | 15 | adantr 481 |
. . . . . . 7
|
17 | 3 | a1i 11 |
. . . . . . 7
|
18 | | simpr 477 |
. . . . . . . 8
|
19 | 9, 18 | sseldi 3601 |
. . . . . . 7
repr |
20 | 14, 16, 17, 19 | reprf 30690 |
. . . . . 6
..^ |
21 | | c0ex 10034 |
. . . . . . . . 9
|
22 | 21 | tpid1 4303 |
. . . . . . . 8
|
23 | | fzo0to3tp 12554 |
. . . . . . . 8
..^ |
24 | 22, 23 | eleqtrri 2700 |
. . . . . . 7
..^ |
25 | 24 | a1i 11 |
. . . . . 6
..^ |
26 | 20, 25 | ffvelrnd 6360 |
. . . . 5
|
27 | 13, 26 | ffvelrnd 6360 |
. . . 4
Λ |
28 | | 1ex 10035 |
. . . . . . . . . 10
|
29 | 28 | tpid2 4304 |
. . . . . . . . 9
|
30 | 29, 23 | eleqtrri 2700 |
. . . . . . . 8
..^ |
31 | 30 | a1i 11 |
. . . . . . 7
..^ |
32 | 20, 31 | ffvelrnd 6360 |
. . . . . 6
|
33 | 13, 32 | ffvelrnd 6360 |
. . . . 5
Λ |
34 | | 2ex 11092 |
. . . . . . . . . 10
|
35 | 34 | tpid3 4307 |
. . . . . . . . 9
|
36 | 35, 23 | eleqtrri 2700 |
. . . . . . . 8
..^ |
37 | 36 | a1i 11 |
. . . . . . 7
..^ |
38 | 20, 37 | ffvelrnd 6360 |
. . . . . 6
|
39 | 13, 38 | ffvelrnd 6360 |
. . . . 5
Λ |
40 | 33, 39 | remulcld 10070 |
. . . 4
Λ Λ |
41 | 27, 40 | remulcld 10070 |
. . 3
Λ Λ Λ |
42 | 11, 41 | fsumrecl 14465 |
. 2
Λ Λ Λ |
43 | 1 | nnrpd 11870 |
. . . 4
|
44 | 43 | relogcld 24369 |
. . 3
|
45 | 27, 33 | remulcld 10070 |
. . . 4
Λ Λ |
46 | 11, 45 | fsumrecl 14465 |
. . 3
Λ Λ |
47 | 44, 46 | remulcld 10070 |
. 2
Λ Λ |
48 | | fzfi 12771 |
. . . . . . . 8
|
49 | | diffi 8192 |
. . . . . . . 8
|
50 | 48, 49 | ax-mp 5 |
. . . . . . 7
|
51 | | snfi 8038 |
. . . . . . 7
|
52 | | unfi 8227 |
. . . . . . 7
|
53 | 50, 51, 52 | mp2an 708 |
. . . . . 6
|
54 | 53 | a1i 11 |
. . . . 5
|
55 | 12 | a1i 11 |
. . . . . 6
Λ |
56 | | difss 3737 |
. . . . . . . . . 10
|
57 | 56 | a1i 11 |
. . . . . . . . 9
|
58 | | 2nn 11185 |
. . . . . . . . . . . 12
|
59 | 58 | a1i 11 |
. . . . . . . . . . 11
|
60 | | hgt750lemb.2 |
. . . . . . . . . . 11
|
61 | | elfz1b 12409 |
. . . . . . . . . . . 12
|
62 | 61 | biimpri 218 |
. . . . . . . . . . 11
|
63 | 59, 1, 60, 62 | syl3anc 1326 |
. . . . . . . . . 10
|
64 | 63 | snssd 4340 |
. . . . . . . . 9
|
65 | 57, 64 | unssd 3789 |
. . . . . . . 8
|
66 | | fz1ssnn 12372 |
. . . . . . . . 9
|
67 | 66 | a1i 11 |
. . . . . . . 8
|
68 | 65, 67 | sstrd 3613 |
. . . . . . 7
|
69 | 68 | sselda 3603 |
. . . . . 6
|
70 | 55, 69 | ffvelrnd 6360 |
. . . . 5
Λ |
71 | 54, 70 | fsumrecl 14465 |
. . . 4
Λ |
72 | | fzfid 12772 |
. . . . 5
|
73 | 12 | a1i 11 |
. . . . . 6
Λ |
74 | 67 | sselda 3603 |
. . . . . 6
|
75 | 73, 74 | ffvelrnd 6360 |
. . . . 5
Λ |
76 | 72, 75 | fsumrecl 14465 |
. . . 4
Λ |
77 | 71, 76 | remulcld 10070 |
. . 3
Λ Λ |
78 | 44, 77 | remulcld 10070 |
. 2
Λ Λ |
79 | 1 | adantr 481 |
. . . . . . . 8
|
80 | 79 | nnrpd 11870 |
. . . . . . 7
|
81 | | relogcl 24322 |
. . . . . . 7
|
82 | 80, 81 | syl 17 |
. . . . . 6
|
83 | 33, 82 | remulcld 10070 |
. . . . 5
Λ |
84 | 27, 83 | remulcld 10070 |
. . . 4
Λ Λ |
85 | | vmage0 24847 |
. . . . . 6
Λ |
86 | 26, 85 | syl 17 |
. . . . 5
Λ |
87 | | vmage0 24847 |
. . . . . . 7
Λ |
88 | 32, 87 | syl 17 |
. . . . . 6
Λ |
89 | 38 | nnrpd 11870 |
. . . . . . . 8
|
90 | 89 | relogcld 24369 |
. . . . . . 7
|
91 | | vmalelog 24930 |
. . . . . . . 8
Λ |
92 | 38, 91 | syl 17 |
. . . . . . 7
Λ |
93 | 14, 16, 17, 19, 37 | reprle 30692 |
. . . . . . . 8
|
94 | | logleb 24349 |
. . . . . . . . 9
|
95 | 94 | biimpa 501 |
. . . . . . . 8
|
96 | 89, 80, 93, 95 | syl21anc 1325 |
. . . . . . 7
|
97 | 39, 90, 82, 92, 96 | letrd 10194 |
. . . . . 6
Λ |
98 | 39, 82, 33, 88, 97 | lemul2ad 10964 |
. . . . 5
Λ Λ
Λ |
99 | 40, 83, 27, 86, 98 | lemul2ad 10964 |
. . . 4
Λ Λ Λ Λ Λ |
100 | 11, 41, 84, 99 | fsumle 14531 |
. . 3
Λ Λ Λ Λ Λ |
101 | 1 | nncnd 11036 |
. . . . . 6
|
102 | 1 | nnne0d 11065 |
. . . . . 6
|
103 | 101, 102 | logcld 24317 |
. . . . 5
|
104 | 45 | recnd 10068 |
. . . . 5
Λ Λ |
105 | 11, 103, 104 | fsummulc2 14516 |
. . . 4
Λ Λ Λ Λ |
106 | 103 | adantr 481 |
. . . . . . 7
|
107 | 106, 104 | mulcomd 10061 |
. . . . . 6
Λ Λ Λ Λ |
108 | 27 | recnd 10068 |
. . . . . . 7
Λ |
109 | 33 | recnd 10068 |
. . . . . . 7
Λ |
110 | 108, 109,
106 | mulassd 10063 |
. . . . . 6
Λ Λ Λ Λ |
111 | 107, 110 | eqtrd 2656 |
. . . . 5
Λ Λ Λ Λ |
112 | 111 | sumeq2dv 14433 |
. . . 4
Λ Λ Λ Λ |
113 | 105, 112 | eqtr2d 2657 |
. . 3
Λ Λ Λ Λ |
114 | 100, 113 | breqtrd 4679 |
. 2
Λ Λ Λ
Λ Λ |
115 | 1 | nnred 11035 |
. . . 4
|
116 | 1 | nnge1d 11063 |
. . . 4
|
117 | 115, 116 | logge0d 24376 |
. . 3
|
118 | | xpfi 8231 |
. . . . . 6
|
119 | 54, 72, 118 | syl2anc 693 |
. . . . 5
|
120 | 12 | a1i 11 |
. . . . . . 7
Λ |
121 | 68 | adantr 481 |
. . . . . . . 8
|
122 | | xp1st 7198 |
. . . . . . . . 9
|
123 | 122 | adantl 482 |
. . . . . . . 8
|
124 | 121, 123 | sseldd 3604 |
. . . . . . 7
|
125 | 120, 124 | ffvelrnd 6360 |
. . . . . 6
Λ |
126 | | xp2nd 7199 |
. . . . . . . . 9
|
127 | 126 | adantl 482 |
. . . . . . . 8
|
128 | 66, 127 | sseldi 3601 |
. . . . . . 7
|
129 | 120, 128 | ffvelrnd 6360 |
. . . . . 6
Λ |
130 | 125, 129 | remulcld 10070 |
. . . . 5
Λ Λ |
131 | | vmage0 24847 |
. . . . . . 7
Λ |
132 | 124, 131 | syl 17 |
. . . . . 6
Λ |
133 | | vmage0 24847 |
. . . . . . 7
Λ |
134 | 128, 133 | syl 17 |
. . . . . 6
Λ |
135 | 125, 129,
132, 134 | mulge0d 10604 |
. . . . 5
Λ Λ |
136 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
|
137 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
|
138 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
|
139 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
140 | 9, 139 | sseldi 3601 |
. . . . . . . . . . . . . 14
repr |
141 | 136, 137,
138, 140 | reprf 30690 |
. . . . . . . . . . . . 13
..^ |
142 | 24 | a1i 11 |
. . . . . . . . . . . . 13
..^ |
143 | 141, 142 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
144 | 1 | adantr 481 |
. . . . . . . . . . . 12
|
145 | 136, 137,
138, 140, 142 | reprle 30692 |
. . . . . . . . . . . 12
|
146 | | elfz1b 12409 |
. . . . . . . . . . . . 13
|
147 | 146 | biimpri 218 |
. . . . . . . . . . . 12
|
148 | 143, 144,
145, 147 | syl3anc 1326 |
. . . . . . . . . . 11
|
149 | 8 | rabeq2i 3197 |
. . . . . . . . . . . . . 14
repr |
150 | 149 | simprbi 480 |
. . . . . . . . . . . . 13
|
151 | | hgt750leme.o |
. . . . . . . . . . . . . . 15
|
152 | 151 | oddprm2 30733 |
. . . . . . . . . . . . . 14
|
153 | 152 | eleq2i 2693 |
. . . . . . . . . . . . 13
|
154 | 150, 153 | sylnibr 319 |
. . . . . . . . . . . 12
|
155 | 139, 154 | syl 17 |
. . . . . . . . . . 11
|
156 | 148, 155 | jca 554 |
. . . . . . . . . 10
|
157 | | eldif 3584 |
. . . . . . . . . 10
|
158 | 156, 157 | sylibr 224 |
. . . . . . . . 9
|
159 | | uncom 3757 |
. . . . . . . . . . . . 13
|
160 | | undif3 3888 |
. . . . . . . . . . . . 13
|
161 | 159, 160 | eqtri 2644 |
. . . . . . . . . . . 12
|
162 | | ssequn1 3783 |
. . . . . . . . . . . . . 14
|
163 | 64, 162 | sylib 208 |
. . . . . . . . . . . . 13
|
164 | 163 | difeq1d 3727 |
. . . . . . . . . . . 12
|
165 | 161, 164 | syl5eq 2668 |
. . . . . . . . . . 11
|
166 | 165 | eleq2d 2687 |
. . . . . . . . . 10
|
167 | 166 | adantr 481 |
. . . . . . . . 9
|
168 | 158, 167 | mpbird 247 |
. . . . . . . 8
|
169 | 30 | a1i 11 |
. . . . . . . . . 10
..^ |
170 | 141, 169 | ffvelrnd 6360 |
. . . . . . . . 9
|
171 | 136, 137,
138, 140, 169 | reprle 30692 |
. . . . . . . . 9
|
172 | | elfz1b 12409 |
. . . . . . . . . 10
|
173 | 172 | biimpri 218 |
. . . . . . . . 9
|
174 | 170, 144,
171, 173 | syl3anc 1326 |
. . . . . . . 8
|
175 | 168, 174 | opelxpd 5149 |
. . . . . . 7
|
176 | 175 | ralrimiva 2966 |
. . . . . 6
|
177 | | fveq1 6190 |
. . . . . . . . 9
|
178 | | fveq1 6190 |
. . . . . . . . 9
|
179 | 177, 178 | opeq12d 4410 |
. . . . . . . 8
|
180 | 179 | cbvmptv 4750 |
. . . . . . 7
|
181 | 180 | rnmptss 6392 |
. . . . . 6
|
182 | 176, 181 | syl 17 |
. . . . 5
|
183 | 119, 130,
135, 182 | fsumless 14528 |
. . . 4
Λ Λ
Λ Λ |
184 | | fvex 6201 |
. . . . . . . 8
|
185 | | fvex 6201 |
. . . . . . . 8
|
186 | 184, 185 | op1std 7178 |
. . . . . . 7
|
187 | 186 | fveq2d 6195 |
. . . . . 6
Λ Λ |
188 | 184, 185 | op2ndd 7179 |
. . . . . . 7
|
189 | 188 | fveq2d 6195 |
. . . . . 6
Λ Λ |
190 | 187, 189 | oveq12d 6668 |
. . . . 5
Λ Λ Λ Λ |
191 | | opex 4932 |
. . . . . . . 8
|
192 | 191 | rgenw 2924 |
. . . . . . 7
|
193 | 180 | fnmpt 6020 |
. . . . . . 7
|
194 | 192, 193 | mp1i 13 |
. . . . . 6
|
195 | | eqidd 2623 |
. . . . . 6
|
196 | 141 | ad2antrr 762 |
. . . . . . . . . . 11
..^ |
197 | 196 | ffnd 6046 |
. . . . . . . . . 10
..^ |
198 | 20 | ad4ant13 1292 |
. . . . . . . . . . 11
..^ |
199 | 198 | ffnd 6046 |
. . . . . . . . . 10
..^ |
200 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
201 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
202 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
203 | 201, 202 | fvmpt2d 6293 |
. . . . . . . . . . . . . . . . . 18
|
204 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
205 | 204 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
206 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
207 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
|
208 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
|
209 | 207, 208 | opeq12d 4410 |
. . . . . . . . . . . . . . . . . . . 20
|
210 | 209 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
211 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . 20
|
212 | 211 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
213 | 206, 210,
18, 212 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . 18
|
214 | 213 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
215 | 214 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
216 | 200, 205,
215 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . 15
|
217 | 184, 185 | opth2 4949 |
. . . . . . . . . . . . . . 15
|
218 | 216, 217 | sylib 208 |
. . . . . . . . . . . . . 14
|
219 | 218 | simpld 475 |
. . . . . . . . . . . . 13
|
220 | 219 | ad2antrr 762 |
. . . . . . . . . . . 12
..^
|
221 | | simpr 477 |
. . . . . . . . . . . . 13
..^
|
222 | 221 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
|
223 | 221 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
|
224 | 220, 222,
223 | 3eqtr4d 2666 |
. . . . . . . . . . 11
..^
|
225 | 218 | simprd 479 |
. . . . . . . . . . . . 13
|
226 | 225 | ad2antrr 762 |
. . . . . . . . . . . 12
..^
|
227 | | simpr 477 |
. . . . . . . . . . . . 13
..^
|
228 | 227 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
|
229 | 227 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
|
230 | 226, 228,
229 | 3eqtr4d 2666 |
. . . . . . . . . . 11
..^
|
231 | 219 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
..^
|
232 | 225 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
..^
|
233 | 231, 232 | oveq12d 6668 |
. . . . . . . . . . . . . 14
..^
|
234 | 233 | oveq2d 6666 |
. . . . . . . . . . . . 13
..^
|
235 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
..^ |
236 | 235 | sumeq1d 14431 |
. . . . . . . . . . . . . . 15
..^
..^ |
237 | 5 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
|
238 | 137 | ad4antr 768 |
. . . . . . . . . . . . . . . 16
..^
|
239 | 3 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
|
240 | 140 | ad4antr 768 |
. . . . . . . . . . . . . . . 16
..^
repr |
241 | 237, 238,
239, 240 | reprsum 30691 |
. . . . . . . . . . . . . . 15
..^
..^ |
242 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
243 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
244 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
245 | 143 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
246 | 245 | ad4antr 768 |
. . . . . . . . . . . . . . . . 17
..^
|
247 | 170 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
248 | 247 | ad4antr 768 |
. . . . . . . . . . . . . . . . 17
..^
|
249 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
250 | 141, 249 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
|
251 | 250 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
252 | 251 | ad4antr 768 |
. . . . . . . . . . . . . . . . 17
..^
|
253 | 246, 248,
252 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
..^
|
254 | 21, 28, 34 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . 17
|
255 | 254 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
|
256 | | 0ne1 11088 |
. . . . . . . . . . . . . . . . 17
|
257 | 256 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
|
258 | | 0ne2 11239 |
. . . . . . . . . . . . . . . . 17
|
259 | 258 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
|
260 | | 1ne2 11240 |
. . . . . . . . . . . . . . . . 17
|
261 | 260 | a1i 11 |
. . . . . . . . . . . . . . . 16
..^
|
262 | 242, 243,
244, 253, 255, 257, 259, 261 | sumtp 14478 |
. . . . . . . . . . . . . . 15
..^
|
263 | 236, 241,
262 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . 14
..^
|
264 | 246, 248 | addcld 10059 |
. . . . . . . . . . . . . . 15
..^
|
265 | 101 | ad5antr 770 |
. . . . . . . . . . . . . . 15
..^
|
266 | 264, 252,
265 | addrsub 10448 |
. . . . . . . . . . . . . 14
..^
|
267 | 263, 266 | mpbid 222 |
. . . . . . . . . . . . 13
..^
|
268 | 235 | sumeq1d 14431 |
. . . . . . . . . . . . . . 15
..^
..^ |
269 | 19 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . 17
repr |
270 | 269 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
..^
repr |
271 | 237, 238,
239, 270 | reprsum 30691 |
. . . . . . . . . . . . . . 15
..^
..^ |
272 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
273 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
274 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
275 | 26 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
276 | 275 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
277 | 276 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
..^
|
278 | 32 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
279 | 278 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
280 | 279 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
..^
|
281 | 38 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
282 | 281 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
283 | 282 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
..^
|
284 | 277, 280,
283 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
..^
|
285 | 272, 273,
274, 284, 255, 257, 259, 261 | sumtp 14478 |
. . . . . . . . . . . . . . 15
..^
|
286 | 268, 271,
285 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . 14
..^
|
287 | 277, 280 | addcld 10059 |
. . . . . . . . . . . . . . 15
..^
|
288 | 287, 283,
265 | addrsub 10448 |
. . . . . . . . . . . . . 14
..^
|
289 | 286, 288 | mpbid 222 |
. . . . . . . . . . . . 13
..^
|
290 | 234, 267,
289 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
..^
|
291 | | simpr 477 |
. . . . . . . . . . . . 13
..^
|
292 | 291 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
|
293 | 291 | fveq2d 6195 |
. . . . . . . . . . . 12
..^
|
294 | 290, 292,
293 | 3eqtr4d 2666 |
. . . . . . . . . . 11
..^
|
295 | | simpr 477 |
. . . . . . . . . . . . 13
..^ ..^ |
296 | 295, 23 | syl6eleq 2711 |
. . . . . . . . . . . 12
..^ |
297 | | vex 3203 |
. . . . . . . . . . . . 13
|
298 | 297 | eltp 4230 |
. . . . . . . . . . . 12
|
299 | 296, 298 | sylib 208 |
. . . . . . . . . . 11
..^ |
300 | 224, 230,
294, 299 | mpjao3dan 1395 |
. . . . . . . . . 10
..^ |
301 | 197, 199,
300 | eqfnfvd 6314 |
. . . . . . . . 9
|
302 | 301 | ex 450 |
. . . . . . . 8
|
303 | 302 | anasss 679 |
. . . . . . 7
|
304 | 303 | ralrimivva 2971 |
. . . . . 6
|
305 | | dff1o6 6531 |
. . . . . . 7
|
306 | 305 | biimpri 218 |
. . . . . 6
|
307 | 194, 195,
304, 306 | syl3anc 1326 |
. . . . 5
|
308 | 182 | sselda 3603 |
. . . . . . . 8
|
309 | 308, 125 | syldan 487 |
. . . . . . 7
Λ |
310 | 308, 129 | syldan 487 |
. . . . . . 7
Λ |
311 | 309, 310 | remulcld 10070 |
. . . . . 6
Λ Λ |
312 | 311 | recnd 10068 |
. . . . 5
Λ Λ |
313 | 190, 11, 307, 213, 312 | fsumf1o 14454 |
. . . 4
Λ Λ
Λ Λ |
314 | 76 | recnd 10068 |
. . . . . 6
Λ |
315 | 70 | recnd 10068 |
. . . . . 6
Λ |
316 | 54, 314, 315 | fsummulc1 14517 |
. . . . 5
Λ Λ Λ
Λ |
317 | 48 | a1i 11 |
. . . . . . 7
|
318 | 75 | adantrl 752 |
. . . . . . . . 9
Λ |
319 | 318 | anassrs 680 |
. . . . . . . 8
Λ |
320 | 319 | recnd 10068 |
. . . . . . 7
Λ |
321 | 317, 315,
320 | fsummulc2 14516 |
. . . . . 6
Λ Λ Λ Λ |
322 | 321 | sumeq2dv 14433 |
. . . . 5
Λ Λ Λ Λ |
323 | | vex 3203 |
. . . . . . . . 9
|
324 | 297, 323 | op1std 7178 |
. . . . . . . 8
|
325 | 324 | fveq2d 6195 |
. . . . . . 7
Λ Λ |
326 | 297, 323 | op2ndd 7179 |
. . . . . . . 8
|
327 | 326 | fveq2d 6195 |
. . . . . . 7
Λ Λ |
328 | 325, 327 | oveq12d 6668 |
. . . . . 6
Λ Λ Λ Λ |
329 | 70 | adantrr 753 |
. . . . . . . 8
Λ |
330 | 329, 318 | remulcld 10070 |
. . . . . . 7
Λ Λ |
331 | 330 | recnd 10068 |
. . . . . 6
Λ Λ |
332 | 328, 54, 72, 331 | fsumxp 14503 |
. . . . 5
Λ Λ
Λ Λ |
333 | 316, 322,
332 | 3eqtrrd 2661 |
. . . 4
Λ Λ
Λ Λ |
334 | 183, 313,
333 | 3brtr3d 4684 |
. . 3
Λ Λ
Λ Λ |
335 | 46, 77, 44, 117, 334 | lemul2ad 10964 |
. 2
Λ Λ
Λ Λ |
336 | 42, 47, 78, 114, 335 | letrd 10194 |
1
Λ Λ Λ
Λ Λ |