Proof of Theorem sqwvfoura
Step | Hyp | Ref
| Expression |
1 | | pire 24210 |
. . . . . 6
|
2 | 1 | renegcli 10342 |
. . . . 5
|
3 | 2 | a1i 11 |
. . . 4
|
4 | 1 | a1i 11 |
. . . 4
|
5 | | 0re 10040 |
. . . . . 6
|
6 | | negpilt0 39492 |
. . . . . . 7
|
7 | 2, 5, 6 | ltleii 10160 |
. . . . . 6
|
8 | | pipos 24212 |
. . . . . . 7
|
9 | 5, 1, 8 | ltleii 10160 |
. . . . . 6
|
10 | 2, 1 | elicc2i 12239 |
. . . . . 6
|
11 | 5, 7, 9, 10 | mpbir3an 1244 |
. . . . 5
|
12 | 11 | a1i 11 |
. . . 4
|
13 | | 1red 10055 |
. . . . . . . . . . 11
|
14 | 13 | renegcld 10457 |
. . . . . . . . . . 11
|
15 | 13, 14 | ifcld 4131 |
. . . . . . . . . 10
|
16 | 15 | adantl 482 |
. . . . . . . . 9
|
17 | | sqwvfoura.f |
. . . . . . . . 9
|
18 | 16, 17 | fmptd 6385 |
. . . . . . . 8
|
19 | 18 | adantr 481 |
. . . . . . 7
|
20 | | elioore 12205 |
. . . . . . . 8
|
21 | 20 | adantl 482 |
. . . . . . 7
|
22 | 19, 21 | ffvelrnd 6360 |
. . . . . 6
|
23 | | sqwvfoura.n |
. . . . . . . . . 10
|
24 | 23 | nn0red 11352 |
. . . . . . . . 9
|
25 | 24 | adantr 481 |
. . . . . . . 8
|
26 | 25, 21 | remulcld 10070 |
. . . . . . 7
|
27 | 26 | recoscld 14874 |
. . . . . 6
|
28 | 22, 27 | remulcld 10070 |
. . . . 5
|
29 | 28 | recnd 10068 |
. . . 4
|
30 | | elioore 12205 |
. . . . . . . . . 10
|
31 | 30, 15 | syl 17 |
. . . . . . . . . 10
|
32 | 17 | fvmpt2 6291 |
. . . . . . . . . 10
|
33 | 30, 31, 32 | syl2anc 693 |
. . . . . . . . 9
|
34 | 1 | a1i 11 |
. . . . . . . . . . 11
|
35 | | sqwvfoura.t |
. . . . . . . . . . . . . 14
|
36 | | 2rp 11837 |
. . . . . . . . . . . . . . 15
|
37 | | pirp 24213 |
. . . . . . . . . . . . . . 15
|
38 | | rpmulcl 11855 |
. . . . . . . . . . . . . . 15
|
39 | 36, 37, 38 | mp2an 708 |
. . . . . . . . . . . . . 14
|
40 | 35, 39 | eqeltri 2697 |
. . . . . . . . . . . . 13
|
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
|
42 | 30, 41 | modcld 12674 |
. . . . . . . . . . 11
|
43 | | picn 24211 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | 2timesi 11147 |
. . . . . . . . . . . . . . . 16
|
45 | 35, 44 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
46 | 45 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
47 | 2 | recni 10052 |
. . . . . . . . . . . . . . 15
|
48 | 47, 43, 43 | addassi 10048 |
. . . . . . . . . . . . . 14
|
49 | 43 | negidi 10350 |
. . . . . . . . . . . . . . . . 17
|
50 | 43, 47, 49 | addcomli 10228 |
. . . . . . . . . . . . . . . 16
|
51 | 50 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
|
52 | 43 | addid2i 10224 |
. . . . . . . . . . . . . . 15
|
53 | 51, 52 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
54 | 46, 48, 53 | 3eqtr2ri 2651 |
. . . . . . . . . . . . 13
|
55 | 2 | a1i 11 |
. . . . . . . . . . . . . 14
|
56 | | 2re 11090 |
. . . . . . . . . . . . . . . . 17
|
57 | 56, 1 | remulcli 10054 |
. . . . . . . . . . . . . . . 16
|
58 | 35, 57 | eqeltri 2697 |
. . . . . . . . . . . . . . 15
|
59 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
|
60 | 2 | rexri 10097 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . 15
|
62 | | 0red 10041 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
64 | | id 22 |
. . . . . . . . . . . . . . 15
|
65 | | ioogtlb 39717 |
. . . . . . . . . . . . . . 15
|
66 | 61, 63, 64, 65 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
67 | 55, 30, 59, 66 | ltadd1dd 10638 |
. . . . . . . . . . . . 13
|
68 | 54, 67 | syl5eqbr 4688 |
. . . . . . . . . . . 12
|
69 | 58 | recni 10052 |
. . . . . . . . . . . . . . . . 17
|
70 | 69 | mulid2i 10043 |
. . . . . . . . . . . . . . . 16
|
71 | 70 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
|
72 | 71 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
73 | 72 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
74 | 30, 59 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
75 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
76 | 62, 34, 74, 75, 68 | lttrd 10198 |
. . . . . . . . . . . . . . 15
|
77 | 62, 74, 76 | ltled 10185 |
. . . . . . . . . . . . . 14
|
78 | | iooltub 39735 |
. . . . . . . . . . . . . . . . 17
|
79 | 61, 63, 64, 78 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
80 | 30, 62, 59, 79 | ltadd1dd 10638 |
. . . . . . . . . . . . . . 15
|
81 | 69 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | addid2d 10237 |
. . . . . . . . . . . . . . 15
|
83 | 80, 82 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
84 | | modid 12695 |
. . . . . . . . . . . . . 14
|
85 | 74, 41, 77, 83, 84 | syl22anc 1327 |
. . . . . . . . . . . . 13
|
86 | | 1zzd 11408 |
. . . . . . . . . . . . . 14
|
87 | | modcyc 12705 |
. . . . . . . . . . . . . 14
|
88 | 30, 41, 86, 87 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
89 | 73, 85, 88 | 3eqtr3a 2680 |
. . . . . . . . . . . 12
|
90 | 68, 89 | breqtrd 4679 |
. . . . . . . . . . 11
|
91 | 34, 42, 90 | ltnsymd 10186 |
. . . . . . . . . 10
|
92 | 91 | iffalsed 4097 |
. . . . . . . . 9
|
93 | 33, 92 | eqtrd 2656 |
. . . . . . . 8
|
94 | 93 | oveq1d 6665 |
. . . . . . 7
|
95 | 94 | adantl 482 |
. . . . . 6
|
96 | 95 | mpteq2dva 4744 |
. . . . 5
|
97 | | 1cnd 10056 |
. . . . . . 7
|
98 | 97 | negcld 10379 |
. . . . . 6
|
99 | 24 | adantr 481 |
. . . . . . . 8
|
100 | 30 | adantl 482 |
. . . . . . . 8
|
101 | 99, 100 | remulcld 10070 |
. . . . . . 7
|
102 | 101 | recoscld 14874 |
. . . . . 6
|
103 | | ioossicc 12259 |
. . . . . . . 8
|
104 | 103 | a1i 11 |
. . . . . . 7
|
105 | | ioombl 23333 |
. . . . . . . 8
|
106 | 105 | a1i 11 |
. . . . . . 7
|
107 | 24 | adantr 481 |
. . . . . . . . 9
|
108 | | iccssre 12255 |
. . . . . . . . . . . 12
|
109 | 2, 5, 108 | mp2an 708 |
. . . . . . . . . . 11
|
110 | 109 | sseli 3599 |
. . . . . . . . . 10
|
111 | 110 | adantl 482 |
. . . . . . . . 9
|
112 | 107, 111 | remulcld 10070 |
. . . . . . . 8
|
113 | 112 | recoscld 14874 |
. . . . . . 7
|
114 | | 0red 10041 |
. . . . . . . 8
|
115 | | coscn 24199 |
. . . . . . . . . 10
|
116 | 115 | a1i 11 |
. . . . . . . . 9
|
117 | | ax-resscn 9993 |
. . . . . . . . . . . . 13
|
118 | 109, 117 | sstri 3612 |
. . . . . . . . . . . 12
|
119 | 118 | a1i 11 |
. . . . . . . . . . 11
|
120 | 24 | recnd 10068 |
. . . . . . . . . . 11
|
121 | | ssid 3624 |
. . . . . . . . . . . 12
|
122 | 121 | a1i 11 |
. . . . . . . . . . 11
|
123 | 119, 120,
122 | constcncfg 40084 |
. . . . . . . . . 10
|
124 | 119, 122 | idcncfg 40085 |
. . . . . . . . . 10
|
125 | 123, 124 | mulcncf 23215 |
. . . . . . . . 9
|
126 | 116, 125 | cncfmpt1f 22716 |
. . . . . . . 8
|
127 | | cniccibl 23607 |
. . . . . . . 8
|
128 | 3, 114, 126, 127 | syl3anc 1326 |
. . . . . . 7
|
129 | 104, 106,
113, 128 | iblss 23571 |
. . . . . 6
|
130 | 98, 102, 129 | iblmulc2 23597 |
. . . . 5
|
131 | 96, 130 | eqeltrd 2701 |
. . . 4
|
132 | | elioore 12205 |
. . . . . . . . . 10
|
133 | 132, 15 | syl 17 |
. . . . . . . . . 10
|
134 | 132, 133,
32 | syl2anc 693 |
. . . . . . . . 9
|
135 | 40 | a1i 11 |
. . . . . . . . . . . 12
|
136 | | 0red 10041 |
. . . . . . . . . . . . 13
|
137 | 136 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
138 | 1 | rexri 10097 |
. . . . . . . . . . . . . . 15
|
139 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
|
140 | | id 22 |
. . . . . . . . . . . . . 14
|
141 | | ioogtlb 39717 |
. . . . . . . . . . . . . 14
|
142 | 137, 139,
140, 141 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
143 | 136, 132,
142 | ltled 10185 |
. . . . . . . . . . . 12
|
144 | 1 | a1i 11 |
. . . . . . . . . . . . 13
|
145 | 58 | a1i 11 |
. . . . . . . . . . . . 13
|
146 | | iooltub 39735 |
. . . . . . . . . . . . . 14
|
147 | 137, 139,
140, 146 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
148 | | 2timesgt 39500 |
. . . . . . . . . . . . . . . 16
|
149 | 37, 148 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
150 | 149, 35 | breqtrri 4680 |
. . . . . . . . . . . . . 14
|
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
|
152 | 132, 144,
145, 147, 151 | lttrd 10198 |
. . . . . . . . . . . 12
|
153 | | modid 12695 |
. . . . . . . . . . . 12
|
154 | 132, 135,
143, 152, 153 | syl22anc 1327 |
. . . . . . . . . . 11
|
155 | 154, 147 | eqbrtrd 4675 |
. . . . . . . . . 10
|
156 | 155 | iftrued 4094 |
. . . . . . . . 9
|
157 | 134, 156 | eqtrd 2656 |
. . . . . . . 8
|
158 | 157 | oveq1d 6665 |
. . . . . . 7
|
159 | 158 | adantl 482 |
. . . . . 6
|
160 | 159 | mpteq2dva 4744 |
. . . . 5
|
161 | 24 | adantr 481 |
. . . . . . . 8
|
162 | 132 | adantl 482 |
. . . . . . . 8
|
163 | 161, 162 | remulcld 10070 |
. . . . . . 7
|
164 | 163 | recoscld 14874 |
. . . . . 6
|
165 | | ioossicc 12259 |
. . . . . . . 8
|
166 | 165 | a1i 11 |
. . . . . . 7
|
167 | | ioombl 23333 |
. . . . . . . 8
|
168 | 167 | a1i 11 |
. . . . . . 7
|
169 | 24 | adantr 481 |
. . . . . . . . 9
|
170 | | iccssre 12255 |
. . . . . . . . . . . 12
|
171 | 5, 1, 170 | mp2an 708 |
. . . . . . . . . . 11
|
172 | 171 | sseli 3599 |
. . . . . . . . . 10
|
173 | 172 | adantl 482 |
. . . . . . . . 9
|
174 | 169, 173 | remulcld 10070 |
. . . . . . . 8
|
175 | 174 | recoscld 14874 |
. . . . . . 7
|
176 | 171, 117 | sstri 3612 |
. . . . . . . . . . . 12
|
177 | 176 | a1i 11 |
. . . . . . . . . . 11
|
178 | 177, 120,
122 | constcncfg 40084 |
. . . . . . . . . 10
|
179 | 177, 122 | idcncfg 40085 |
. . . . . . . . . 10
|
180 | 178, 179 | mulcncf 23215 |
. . . . . . . . 9
|
181 | 116, 180 | cncfmpt1f 22716 |
. . . . . . . 8
|
182 | | cniccibl 23607 |
. . . . . . . 8
|
183 | 114, 4, 181, 182 | syl3anc 1326 |
. . . . . . 7
|
184 | 166, 168,
175, 183 | iblss 23571 |
. . . . . 6
|
185 | 97, 164, 184 | iblmulc2 23597 |
. . . . 5
|
186 | 160, 185 | eqeltrd 2701 |
. . . 4
|
187 | 3, 4, 12, 29, 131, 186 | itgsplitioo 23604 |
. . 3
|
188 | 187 | oveq1d 6665 |
. 2
|
189 | 95 | itgeq2dv 23548 |
. . . . 5
|
190 | 98, 102, 129 | itgmulc2 23600 |
. . . . 5
|
191 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
192 | | ioosscn 39716 |
. . . . . . . . . . . . . . . 16
|
193 | 192 | sseli 3599 |
. . . . . . . . . . . . . . 15
|
194 | 193 | mul02d 10234 |
. . . . . . . . . . . . . 14
|
195 | 191, 194 | sylan9eq 2676 |
. . . . . . . . . . . . 13
|
196 | 195 | fveq2d 6195 |
. . . . . . . . . . . 12
|
197 | | cos0 14880 |
. . . . . . . . . . . 12
|
198 | 196, 197 | syl6eq 2672 |
. . . . . . . . . . 11
|
199 | 198 | adantll 750 |
. . . . . . . . . 10
|
200 | 199 | itgeq2dv 23548 |
. . . . . . . . 9
|
201 | | ioovolcl 23338 |
. . . . . . . . . . . . 13
|
202 | 2, 5, 201 | mp2an 708 |
. . . . . . . . . . . 12
|
203 | 202 | a1i 11 |
. . . . . . . . . . 11
|
204 | | itgconst 23585 |
. . . . . . . . . . 11
|
205 | 106, 203,
97, 204 | syl3anc 1326 |
. . . . . . . . . 10
|
206 | 205 | adantr 481 |
. . . . . . . . 9
|
207 | | volioo 23337 |
. . . . . . . . . . . . . . 15
|
208 | 2, 5, 7, 207 | mp3an 1424 |
. . . . . . . . . . . . . 14
|
209 | | 0cn 10032 |
. . . . . . . . . . . . . . 15
|
210 | 209, 43 | subnegi 10360 |
. . . . . . . . . . . . . 14
|
211 | 208, 210,
52 | 3eqtri 2648 |
. . . . . . . . . . . . 13
|
212 | 211 | a1i 11 |
. . . . . . . . . . . 12
|
213 | 212 | oveq2d 6666 |
. . . . . . . . . . 11
|
214 | 43 | a1i 11 |
. . . . . . . . . . . 12
|
215 | 214 | mulid2d 10058 |
. . . . . . . . . . 11
|
216 | 213, 215 | eqtrd 2656 |
. . . . . . . . . 10
|
217 | 216 | adantr 481 |
. . . . . . . . 9
|
218 | 200, 206,
217 | 3eqtrd 2660 |
. . . . . . . 8
|
219 | 218 | oveq2d 6666 |
. . . . . . 7
|
220 | 43 | mulm1i 10475 |
. . . . . . . 8
|
221 | 220 | a1i 11 |
. . . . . . 7
|
222 | | iftrue 4092 |
. . . . . . . . 9
|
223 | 222 | eqcomd 2628 |
. . . . . . . 8
|
224 | 223 | adantl 482 |
. . . . . . 7
|
225 | 219, 221,
224 | 3eqtrd 2660 |
. . . . . 6
|
226 | 24 | adantr 481 |
. . . . . . . 8
|
227 | 23 | nn0ge0d 11354 |
. . . . . . . . 9
|
228 | 227 | adantr 481 |
. . . . . . . 8
|
229 | | neqne 2802 |
. . . . . . . . 9
|
230 | 229 | adantl 482 |
. . . . . . . 8
|
231 | 226, 228,
230 | ne0gt0d 10174 |
. . . . . . 7
|
232 | | 1cnd 10056 |
. . . . . . . . . 10
|
233 | 232 | negcld 10379 |
. . . . . . . . 9
|
234 | 233 | mul01d 10235 |
. . . . . . . 8
|
235 | 120 | adantr 481 |
. . . . . . . . . . 11
|
236 | 2 | a1i 11 |
. . . . . . . . . . 11
|
237 | | 0red 10041 |
. . . . . . . . . . 11
|
238 | 7 | a1i 11 |
. . . . . . . . . . 11
|
239 | | simpr 477 |
. . . . . . . . . . . 12
|
240 | 239 | gt0ne0d 10592 |
. . . . . . . . . . 11
|
241 | 235, 236,
237, 238, 240 | itgcoscmulx 40185 |
. . . . . . . . . 10
|
242 | 120 | mul01d 10235 |
. . . . . . . . . . . . . . . 16
|
243 | 242 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
244 | | sin0 14879 |
. . . . . . . . . . . . . . 15
|
245 | 243, 244 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
246 | 120, 214 | mulneg2d 10484 |
. . . . . . . . . . . . . . . 16
|
247 | 246 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
248 | 120, 214 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
249 | | sinneg 14876 |
. . . . . . . . . . . . . . . 16
|
250 | 248, 249 | syl 17 |
. . . . . . . . . . . . . . 15
|
251 | 247, 250 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
252 | 245, 251 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
253 | | 0cnd 10033 |
. . . . . . . . . . . . . 14
|
254 | 248 | sincld 14860 |
. . . . . . . . . . . . . 14
|
255 | 253, 254 | subnegd 10399 |
. . . . . . . . . . . . 13
|
256 | 254 | addid2d 10237 |
. . . . . . . . . . . . 13
|
257 | 252, 255,
256 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
258 | 257 | adantr 481 |
. . . . . . . . . . 11
|
259 | 258 | oveq1d 6665 |
. . . . . . . . . 10
|
260 | 23 | nn0zd 11480 |
. . . . . . . . . . . . . 14
|
261 | | sinkpi 24271 |
. . . . . . . . . . . . . 14
|
262 | 260, 261 | syl 17 |
. . . . . . . . . . . . 13
|
263 | 262 | oveq1d 6665 |
. . . . . . . . . . . 12
|
264 | 263 | adantr 481 |
. . . . . . . . . . 11
|
265 | 235, 240 | div0d 10800 |
. . . . . . . . . . 11
|
266 | 264, 265 | eqtrd 2656 |
. . . . . . . . . 10
|
267 | 241, 259,
266 | 3eqtrd 2660 |
. . . . . . . . 9
|
268 | 267 | oveq2d 6666 |
. . . . . . . 8
|
269 | 240 | neneqd 2799 |
. . . . . . . . 9
|
270 | 269 | iffalsed 4097 |
. . . . . . . 8
|
271 | 234, 268,
270 | 3eqtr4d 2666 |
. . . . . . 7
|
272 | 231, 271 | syldan 487 |
. . . . . 6
|
273 | 225, 272 | pm2.61dan 832 |
. . . . 5
|
274 | 189, 190,
273 | 3eqtr2d 2662 |
. . . 4
|
275 | 159 | itgeq2dv 23548 |
. . . . 5
|
276 | 97, 164, 184 | itgmulc2 23600 |
. . . . 5
|
277 | 164, 184 | itgcl 23550 |
. . . . . . 7
|
278 | 277 | mulid2d 10058 |
. . . . . 6
|
279 | | simpl 473 |
. . . . . . . . . . . . . 14
|
280 | 279 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
281 | 132 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
282 | 281 | adantl 482 |
. . . . . . . . . . . . . 14
|
283 | 282 | mul02d 10234 |
. . . . . . . . . . . . 13
|
284 | 280, 283 | eqtrd 2656 |
. . . . . . . . . . . 12
|
285 | 284 | fveq2d 6195 |
. . . . . . . . . . 11
|
286 | 285, 197 | syl6eq 2672 |
. . . . . . . . . 10
|
287 | 286 | adantll 750 |
. . . . . . . . 9
|
288 | 287 | itgeq2dv 23548 |
. . . . . . . 8
|
289 | | ioovolcl 23338 |
. . . . . . . . . . 11
|
290 | 5, 1, 289 | mp2an 708 |
. . . . . . . . . 10
|
291 | | ax-1cn 9994 |
. . . . . . . . . 10
|
292 | | itgconst 23585 |
. . . . . . . . . 10
|
293 | 167, 290,
291, 292 | mp3an 1424 |
. . . . . . . . 9
|
294 | 293 | a1i 11 |
. . . . . . . 8
|
295 | 43 | mulid2i 10043 |
. . . . . . . . . 10
|
296 | | volioo 23337 |
. . . . . . . . . . . . . 14
|
297 | 5, 1, 9, 296 | mp3an 1424 |
. . . . . . . . . . . . 13
|
298 | 43 | subid1i 10353 |
. . . . . . . . . . . . 13
|
299 | 297, 298 | eqtri 2644 |
. . . . . . . . . . . 12
|
300 | 299 | oveq2i 6661 |
. . . . . . . . . . 11
|
301 | 300 | a1i 11 |
. . . . . . . . . 10
|
302 | | iftrue 4092 |
. . . . . . . . . 10
|
303 | 295, 301,
302 | 3eqtr4a 2682 |
. . . . . . . . 9
|
304 | 303 | adantl 482 |
. . . . . . . 8
|
305 | 288, 294,
304 | 3eqtrd 2660 |
. . . . . . 7
|
306 | 262, 245 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
307 | 253 | subidd 10380 |
. . . . . . . . . . . . 13
|
308 | 306, 307 | eqtrd 2656 |
. . . . . . . . . . . 12
|
309 | 308 | oveq1d 6665 |
. . . . . . . . . . 11
|
310 | 309 | adantr 481 |
. . . . . . . . . 10
|
311 | 310, 265 | eqtrd 2656 |
. . . . . . . . 9
|
312 | 1 | a1i 11 |
. . . . . . . . . 10
|
313 | 9 | a1i 11 |
. . . . . . . . . 10
|
314 | 235, 237,
312, 313, 240 | itgcoscmulx 40185 |
. . . . . . . . 9
|
315 | 269 | iffalsed 4097 |
. . . . . . . . 9
|
316 | 311, 314,
315 | 3eqtr4d 2666 |
. . . . . . . 8
|
317 | 231, 316 | syldan 487 |
. . . . . . 7
|
318 | 305, 317 | pm2.61dan 832 |
. . . . . 6
|
319 | 278, 318 | eqtrd 2656 |
. . . . 5
|
320 | 275, 276,
319 | 3eqtr2d 2662 |
. . . 4
|
321 | 274, 320 | oveq12d 6668 |
. . 3
|
322 | 321 | oveq1d 6665 |
. 2
|
323 | 222, 302 | oveq12d 6668 |
. . . . . . 7
|
324 | 323, 50 | syl6eq 2672 |
. . . . . 6
|
325 | | iffalse 4095 |
. . . . . . . 8
|
326 | | iffalse 4095 |
. . . . . . . 8
|
327 | 325, 326 | oveq12d 6668 |
. . . . . . 7
|
328 | | 00id 10211 |
. . . . . . 7
|
329 | 327, 328 | syl6eq 2672 |
. . . . . 6
|
330 | 324, 329 | pm2.61i 176 |
. . . . 5
|
331 | 330 | oveq1i 6660 |
. . . 4
|
332 | 5, 8 | gtneii 10149 |
. . . . 5
|
333 | 43, 332 | div0i 10759 |
. . . 4
|
334 | 331, 333 | eqtri 2644 |
. . 3
|
335 | 334 | a1i 11 |
. 2
|
336 | 188, 322,
335 | 3eqtrd 2660 |
1
|