Proof of Theorem dirkertrigeqlem3
Step | Hyp | Ref
| Expression |
1 | | dirkertrigeqlem3.a |
. . . . . . . . . . . . 13
|
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
|
3 | 2 | oveq2d 6666 |
. . . . . . . . . . 11
|
4 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
5 | 4 | zcnd 11483 |
. . . . . . . . . . . . 13
|
6 | 5 | adantl 482 |
. . . . . . . . . . . 12
|
7 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
8 | | dirkertrigeqlem3.k |
. . . . . . . . . . . . . . . . 17
|
9 | 8 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
10 | 9 | adantr 481 |
. . . . . . . . . . . . . . 15
|
11 | 7, 10 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
12 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
13 | 11, 12 | addcld 10059 |
. . . . . . . . . . . . 13
|
14 | | picn 24211 |
. . . . . . . . . . . . . 14
|
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
|
16 | 13, 15 | mulcld 10060 |
. . . . . . . . . . . 12
|
17 | 6, 16 | mulcomd 10061 |
. . . . . . . . . . 11
|
18 | 13, 15, 6 | mulassd 10063 |
. . . . . . . . . . . 12
|
19 | 15, 6 | mulcld 10060 |
. . . . . . . . . . . . 13
|
20 | 11, 12, 19 | adddird 10065 |
. . . . . . . . . . . 12
|
21 | 11, 19 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
22 | 12, 19 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
23 | 21, 22 | addcomd 10238 |
. . . . . . . . . . . . 13
|
24 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
25 | 24, 5 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . . 14
|
28 | 7, 10, 15, 6 | mul4d 10248 |
. . . . . . . . . . . . . . 15
|
29 | 7, 15 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
30 | 10, 6 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
31 | 29, 30 | mulcomd 10061 |
. . . . . . . . . . . . . . 15
|
32 | 28, 31 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
33 | 27, 32 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
34 | 23, 33 | eqtrd 2656 |
. . . . . . . . . . . 12
|
35 | 18, 20, 34 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
36 | 3, 17, 35 | 3eqtrd 2660 |
. . . . . . . . . 10
|
37 | 36 | fveq2d 6195 |
. . . . . . . . 9
|
38 | 8 | adantr 481 |
. . . . . . . . . . 11
|
39 | 4 | adantl 482 |
. . . . . . . . . . 11
|
40 | 38, 39 | zmulcld 11488 |
. . . . . . . . . 10
|
41 | | cosper 24234 |
. . . . . . . . . 10
|
42 | 19, 40, 41 | syl2anc 693 |
. . . . . . . . 9
|
43 | 37, 42 | eqtrd 2656 |
. . . . . . . 8
|
44 | 43 | sumeq2dv 14433 |
. . . . . . 7
|
45 | 44 | oveq2d 6666 |
. . . . . 6
|
46 | 45 | oveq1d 6665 |
. . . . 5
|
47 | 46 | adantr 481 |
. . . 4
|
48 | | dirkertrigeqlem3.n |
. . . . . . . . . . . . . 14
|
49 | 48 | nncnd 11036 |
. . . . . . . . . . . . 13
|
50 | | 2cnd 11093 |
. . . . . . . . . . . . 13
|
51 | | 2ne0 11113 |
. . . . . . . . . . . . . 14
|
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
|
53 | 49, 50, 52 | divcan2d 10803 |
. . . . . . . . . . . 12
|
54 | 53 | eqcomd 2628 |
. . . . . . . . . . 11
|
55 | 54 | oveq2d 6666 |
. . . . . . . . . 10
|
56 | 55 | sumeq1d 14431 |
. . . . . . . . 9
|
57 | 56 | adantr 481 |
. . . . . . . 8
|
58 | 14 | a1i 11 |
. . . . . . . . . . . . 13
|
59 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
60 | 59 | zcnd 11483 |
. . . . . . . . . . . . 13
|
61 | 58, 60 | mulcomd 10061 |
. . . . . . . . . . . 12
|
62 | 61 | fveq2d 6195 |
. . . . . . . . . . 11
|
63 | 62 | rgen 2922 |
. . . . . . . . . 10
|
64 | 63 | a1i 11 |
. . . . . . . . 9
|
65 | 64 | sumeq2d 14432 |
. . . . . . . 8
|
66 | | simpr 477 |
. . . . . . . . . . 11
|
67 | 48 | nnred 11035 |
. . . . . . . . . . . . 13
|
68 | 67 | adantr 481 |
. . . . . . . . . . . 12
|
69 | | 2rp 11837 |
. . . . . . . . . . . 12
|
70 | | mod0 12675 |
. . . . . . . . . . . 12
|
71 | 68, 69, 70 | sylancl 694 |
. . . . . . . . . . 11
|
72 | 66, 71 | mpbid 222 |
. . . . . . . . . 10
|
73 | | 2re 11090 |
. . . . . . . . . . . . 13
|
74 | 73 | a1i 11 |
. . . . . . . . . . . 12
|
75 | 48 | nngt0d 11064 |
. . . . . . . . . . . 12
|
76 | | 2pos 11112 |
. . . . . . . . . . . . 13
|
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
|
78 | 67, 74, 75, 77 | divgt0d 10959 |
. . . . . . . . . . 11
|
79 | 78 | adantr 481 |
. . . . . . . . . 10
|
80 | | elnnz 11387 |
. . . . . . . . . 10
|
81 | 72, 79, 80 | sylanbrc 698 |
. . . . . . . . 9
|
82 | | dirkertrigeqlem1 40315 |
. . . . . . . . 9
|
83 | 81, 82 | syl 17 |
. . . . . . . 8
|
84 | 57, 65, 83 | 3eqtrd 2660 |
. . . . . . 7
|
85 | 84 | oveq2d 6666 |
. . . . . 6
|
86 | | halfcn 11247 |
. . . . . . 7
|
87 | 86 | addid1i 10223 |
. . . . . 6
|
88 | 85, 87 | syl6eq 2672 |
. . . . 5
|
89 | 88 | oveq1d 6665 |
. . . 4
|
90 | | ax-1cn 9994 |
. . . . . 6
|
91 | | 2cnne0 11242 |
. . . . . 6
|
92 | | pire 24210 |
. . . . . . . 8
|
93 | | pipos 24212 |
. . . . . . . 8
|
94 | 92, 93 | gt0ne0ii 10564 |
. . . . . . 7
|
95 | 14, 94 | pm3.2i 471 |
. . . . . 6
|
96 | | divdiv1 10736 |
. . . . . 6
|
97 | 90, 91, 95, 96 | mp3an 1424 |
. . . . 5
|
98 | 97 | a1i 11 |
. . . 4
|
99 | 47, 89, 98 | 3eqtrd 2660 |
. . 3
|
100 | 1 | oveq2i 6661 |
. . . . . . . . . 10
|
101 | 100 | a1i 11 |
. . . . . . . . 9
|
102 | 86 | a1i 11 |
. . . . . . . . . . 11
|
103 | 49, 102 | addcld 10059 |
. . . . . . . . . 10
|
104 | 50, 9 | mulcld 10060 |
. . . . . . . . . . 11
|
105 | | peano2cn 10208 |
. . . . . . . . . . 11
|
106 | 104, 105 | syl 17 |
. . . . . . . . . 10
|
107 | 14 | a1i 11 |
. . . . . . . . . 10
|
108 | 103, 106,
107 | mulassd 10063 |
. . . . . . . . 9
|
109 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
110 | 49, 102, 104, 109 | muladdd 10489 |
. . . . . . . . . . . . 13
|
111 | 49, 50, 9 | mul12d 10245 |
. . . . . . . . . . . . . . 15
|
112 | 102 | mulid2d 10058 |
. . . . . . . . . . . . . . 15
|
113 | 111, 112 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
114 | 49 | mulid1d 10057 |
. . . . . . . . . . . . . . 15
|
115 | 50, 9 | mulcomd 10061 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
117 | 9, 50, 102 | mulassd 10063 |
. . . . . . . . . . . . . . . 16
|
118 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . 19
|
119 | 118, 51 | recidi 10756 |
. . . . . . . . . . . . . . . . . 18
|
120 | 119 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
|
121 | 9 | mulid1d 10057 |
. . . . . . . . . . . . . . . . 17
|
122 | 120, 121 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
|
123 | 116, 117,
122 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
|
124 | 114, 123 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
125 | 113, 124 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
126 | 49, 9 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
127 | 50, 126 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
128 | 49, 9 | addcld 10059 |
. . . . . . . . . . . . . 14
|
129 | 127, 102,
128 | addassd 10062 |
. . . . . . . . . . . . 13
|
130 | 110, 125,
129 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
131 | 102, 128 | addcld 10059 |
. . . . . . . . . . . . 13
|
132 | 127, 131 | addcomd 10238 |
. . . . . . . . . . . 12
|
133 | 50, 126 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
134 | 133 | oveq2d 6666 |
. . . . . . . . . . . 12
|
135 | 130, 132,
134 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
136 | 135 | oveq1d 6665 |
. . . . . . . . . 10
|
137 | 126, 50 | mulcld 10060 |
. . . . . . . . . . 11
|
138 | 131, 137,
107 | adddird 10065 |
. . . . . . . . . 10
|
139 | 126, 50, 107 | mulassd 10063 |
. . . . . . . . . . 11
|
140 | 139 | oveq2d 6666 |
. . . . . . . . . 10
|
141 | 136, 138,
140 | 3eqtrd 2660 |
. . . . . . . . 9
|
142 | 101, 108,
141 | 3eqtr2d 2662 |
. . . . . . . 8
|
143 | 142 | fveq2d 6195 |
. . . . . . 7
|
144 | 131, 107 | mulcld 10060 |
. . . . . . . 8
|
145 | 48 | nnzd 11481 |
. . . . . . . . 9
|
146 | 145, 8 | zmulcld 11488 |
. . . . . . . 8
|
147 | | sinper 24233 |
. . . . . . . 8
|
148 | 144, 146,
147 | syl2anc 693 |
. . . . . . 7
|
149 | 102, 128 | addcomd 10238 |
. . . . . . . . . 10
|
150 | 49, 9, 102 | addassd 10062 |
. . . . . . . . . 10
|
151 | 9, 102 | addcld 10059 |
. . . . . . . . . . 11
|
152 | 49, 151 | addcomd 10238 |
. . . . . . . . . 10
|
153 | 149, 150,
152 | 3eqtrd 2660 |
. . . . . . . . 9
|
154 | 153 | oveq1d 6665 |
. . . . . . . 8
|
155 | 154 | fveq2d 6195 |
. . . . . . 7
|
156 | 143, 148,
155 | 3eqtrd 2660 |
. . . . . 6
|
157 | 1 | a1i 11 |
. . . . . . . . . 10
|
158 | 157 | oveq1d 6665 |
. . . . . . . . 9
|
159 | 106, 107,
50, 52 | div23d 10838 |
. . . . . . . . 9
|
160 | 104, 109,
50, 52 | divdird 10839 |
. . . . . . . . . . 11
|
161 | 9, 50, 52 | divcan3d 10806 |
. . . . . . . . . . . 12
|
162 | 161 | oveq1d 6665 |
. . . . . . . . . . 11
|
163 | 160, 162 | eqtrd 2656 |
. . . . . . . . . 10
|
164 | 163 | oveq1d 6665 |
. . . . . . . . 9
|
165 | 158, 159,
164 | 3eqtrd 2660 |
. . . . . . . 8
|
166 | 165 | fveq2d 6195 |
. . . . . . 7
|
167 | 166 | oveq2d 6666 |
. . . . . 6
|
168 | 156, 167 | oveq12d 6668 |
. . . . 5
|
169 | 168 | adantr 481 |
. . . 4
|
170 | 151, 49, 107 | adddird 10065 |
. . . . . . 7
|
171 | 170 | fveq2d 6195 |
. . . . . 6
|
172 | 171 | oveq1d 6665 |
. . . . 5
|
173 | 172 | adantr 481 |
. . . 4
|
174 | 49 | halfcld 11277 |
. . . . . . . . . . . . . 14
|
175 | 50, 174 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
176 | 53, 175 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
177 | 176 | oveq1d 6665 |
. . . . . . . . . . 11
|
178 | 174, 50, 107 | mulassd 10063 |
. . . . . . . . . . 11
|
179 | 177, 178 | eqtrd 2656 |
. . . . . . . . . 10
|
180 | 179 | oveq2d 6666 |
. . . . . . . . 9
|
181 | 180 | fveq2d 6195 |
. . . . . . . 8
|
182 | 181 | adantr 481 |
. . . . . . 7
|
183 | 9 | adantr 481 |
. . . . . . . . . 10
|
184 | | 1cnd 10056 |
. . . . . . . . . . 11
|
185 | 184 | halfcld 11277 |
. . . . . . . . . 10
|
186 | 183, 185 | addcld 10059 |
. . . . . . . . 9
|
187 | 14 | a1i 11 |
. . . . . . . . 9
|
188 | 186, 187 | mulcld 10060 |
. . . . . . . 8
|
189 | | sinper 24233 |
. . . . . . . 8
|
190 | 188, 72, 189 | syl2anc 693 |
. . . . . . 7
|
191 | 182, 190 | eqtrd 2656 |
. . . . . 6
|
192 | 50, 107 | mulcld 10060 |
. . . . . . . 8
|
193 | 151, 107 | mulcld 10060 |
. . . . . . . . 9
|
194 | 193 | sincld 14860 |
. . . . . . . 8
|
195 | 192, 194 | mulcomd 10061 |
. . . . . . 7
|
196 | 195 | adantr 481 |
. . . . . 6
|
197 | 191, 196 | oveq12d 6668 |
. . . . 5
|
198 | 94 | a1i 11 |
. . . . . . . . . . . 12
|
199 | 151, 107,
198 | divcan4d 10807 |
. . . . . . . . . . 11
|
200 | 8 | zred 11482 |
. . . . . . . . . . . . 13
|
201 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
|
202 | 201 | rpreccld 11882 |
. . . . . . . . . . . . 13
|
203 | 200, 202 | ltaddrpd 11905 |
. . . . . . . . . . . 12
|
204 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
205 | 204 | rehalfcld 11279 |
. . . . . . . . . . . . 13
|
206 | | halflt1 11250 |
. . . . . . . . . . . . . 14
|
207 | 206 | a1i 11 |
. . . . . . . . . . . . 13
|
208 | 205, 204,
200, 207 | ltadd2dd 10196 |
. . . . . . . . . . . 12
|
209 | | btwnnz 11453 |
. . . . . . . . . . . 12
|
210 | 8, 203, 208, 209 | syl3anc 1326 |
. . . . . . . . . . 11
|
211 | 199, 210 | eqneltrd 2720 |
. . . . . . . . . 10
|
212 | | sineq0 24273 |
. . . . . . . . . . 11
|
213 | 193, 212 | syl 17 |
. . . . . . . . . 10
|
214 | 211, 213 | mtbird 315 |
. . . . . . . . 9
|
215 | 214 | neqned 2801 |
. . . . . . . 8
|
216 | 50, 107, 52, 198 | mulne0d 10679 |
. . . . . . . 8
|
217 | 194, 194,
192, 215, 216 | divdiv1d 10832 |
. . . . . . 7
|
218 | 194, 215 | dividd 10799 |
. . . . . . . 8
|
219 | 218 | oveq1d 6665 |
. . . . . . 7
|
220 | 217, 219 | eqtr3d 2658 |
. . . . . 6
|
221 | 220 | adantr 481 |
. . . . 5
|
222 | 197, 221 | eqtrd 2656 |
. . . 4
|
223 | 169, 173,
222 | 3eqtrrd 2661 |
. . 3
|
224 | 99, 223 | eqtrd 2656 |
. 2
|
225 | 46 | adantr 481 |
. . 3
|
226 | 145 | adantr 481 |
. . . . . . . . 9
|
227 | | simpr 477 |
. . . . . . . . . 10
|
228 | 227 | neqned 2801 |
. . . . . . . . 9
|
229 | | oddfl 39489 |
. . . . . . . . 9
|
230 | 226, 228,
229 | syl2anc 693 |
. . . . . . . 8
|
231 | 230 | oveq2d 6666 |
. . . . . . 7
|
232 | 231 | sumeq1d 14431 |
. . . . . 6
|
233 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
234 | 233 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
235 | | halffl 39510 |
. . . . . . . . . . . . . . . . 17
|
236 | 234, 235 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
237 | 236 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
238 | | 2t0e0 11183 |
. . . . . . . . . . . . . . 15
|
239 | 237, 238 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
240 | 239 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
241 | 90 | addid2i 10224 |
. . . . . . . . . . . . 13
|
242 | 240, 241 | syl6eq 2672 |
. . . . . . . . . . . 12
|
243 | 242 | oveq2d 6666 |
. . . . . . . . . . 11
|
244 | 243 | sumeq1d 14431 |
. . . . . . . . . 10
|
245 | | 1z 11407 |
. . . . . . . . . . . 12
|
246 | | coscl 14857 |
. . . . . . . . . . . . 13
|
247 | 14, 246 | ax-mp 5 |
. . . . . . . . . . . 12
|
248 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
249 | 14 | mulid1i 10042 |
. . . . . . . . . . . . . . 15
|
250 | 248, 249 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
251 | 250 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
252 | 251 | fsum1 14476 |
. . . . . . . . . . . 12
|
253 | 245, 247,
252 | mp2an 708 |
. . . . . . . . . . 11
|
254 | 253 | a1i 11 |
. . . . . . . . . 10
|
255 | | cospi 24224 |
. . . . . . . . . . 11
|
256 | 255 | a1i 11 |
. . . . . . . . . 10
|
257 | 244, 254,
256 | 3eqtrd 2660 |
. . . . . . . . 9
|
258 | 257 | adantl 482 |
. . . . . . . 8
|
259 | | 2nn 11185 |
. . . . . . . . . . . . 13
|
260 | 259 | a1i 11 |
. . . . . . . . . . . 12
|
261 | 67 | rehalfcld 11279 |
. . . . . . . . . . . . . . 15
|
262 | 261 | flcld 12599 |
. . . . . . . . . . . . . 14
|
263 | 262 | adantr 481 |
. . . . . . . . . . . . 13
|
264 | | 2div2e1 11150 |
. . . . . . . . . . . . . . 15
|
265 | 73 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
266 | 67 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
267 | 69 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
268 | | neqne 2802 |
. . . . . . . . . . . . . . . . 17
|
269 | | nnne1ge2 39504 |
. . . . . . . . . . . . . . . . 17
|
270 | 48, 268, 269 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
271 | 265, 266,
267, 270 | lediv1dd 11930 |
. . . . . . . . . . . . . . 15
|
272 | 264, 271 | syl5eqbrr 4689 |
. . . . . . . . . . . . . 14
|
273 | 261 | adantr 481 |
. . . . . . . . . . . . . . 15
|
274 | | flge 12606 |
. . . . . . . . . . . . . . 15
|
275 | 273, 245,
274 | sylancl 694 |
. . . . . . . . . . . . . 14
|
276 | 272, 275 | mpbid 222 |
. . . . . . . . . . . . 13
|
277 | | elnnz1 11403 |
. . . . . . . . . . . . 13
|
278 | 263, 276,
277 | sylanbrc 698 |
. . . . . . . . . . . 12
|
279 | 260, 278 | nnmulcld 11068 |
. . . . . . . . . . 11
|
280 | | nnuz 11723 |
. . . . . . . . . . 11
|
281 | 279, 280 | syl6eleq 2711 |
. . . . . . . . . 10
|
282 | 14 | a1i 11 |
. . . . . . . . . . . 12
|
283 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
284 | 283 | zcnd 11483 |
. . . . . . . . . . . . 13
|
285 | 284 | adantl 482 |
. . . . . . . . . . . 12
|
286 | 282, 285 | mulcld 10060 |
. . . . . . . . . . 11
|
287 | 286 | coscld 14861 |
. . . . . . . . . 10
|
288 | | oveq2 6658 |
. . . . . . . . . . 11
|
289 | 288 | fveq2d 6195 |
. . . . . . . . . 10
|
290 | 281, 287,
289 | fsump1 14487 |
. . . . . . . . 9
|
291 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
|
292 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
|
293 | 292 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
294 | 291, 293 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
295 | 294 | fveq2d 6195 |
. . . . . . . . . . . 12
|
296 | 295 | sumeq2i 14429 |
. . . . . . . . . . 11
|
297 | | dirkertrigeqlem1 40315 |
. . . . . . . . . . . 12
|
298 | 278, 297 | syl 17 |
. . . . . . . . . . 11
|
299 | 296, 298 | syl5eq 2668 |
. . . . . . . . . 10
|
300 | 262 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
|
301 | 50, 300 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
302 | 107, 301,
109 | adddid 10064 |
. . . . . . . . . . . . . 14
|
303 | 107, 50, 300 | mul13d 39491 |
. . . . . . . . . . . . . . 15
|
304 | 249 | a1i 11 |
. . . . . . . . . . . . . . 15
|
305 | 303, 304 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
306 | 300, 192 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
307 | 306, 107 | addcomd 10238 |
. . . . . . . . . . . . . 14
|
308 | 302, 305,
307 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
309 | 308 | fveq2d 6195 |
. . . . . . . . . . . 12
|
310 | | cosper 24234 |
. . . . . . . . . . . . 13
|
311 | 107, 262,
310 | syl2anc 693 |
. . . . . . . . . . . 12
|
312 | 255 | a1i 11 |
. . . . . . . . . . . 12
|
313 | 309, 311,
312 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
314 | 313 | adantr 481 |
. . . . . . . . . 10
|
315 | 299, 314 | oveq12d 6668 |
. . . . . . . . 9
|
316 | | neg1cn 11124 |
. . . . . . . . . . 11
|
317 | 316 | addid2i 10224 |
. . . . . . . . . 10
|
318 | 317 | a1i 11 |
. . . . . . . . 9
|
319 | 290, 315,
318 | 3eqtrd 2660 |
. . . . . . . 8
|
320 | 258, 319 | pm2.61dan 832 |
. . . . . . 7
|
321 | 320 | adantr 481 |
. . . . . 6
|
322 | 232, 321 | eqtrd 2656 |
. . . . 5
|
323 | 322 | oveq2d 6666 |
. . . 4
|
324 | 323 | oveq1d 6665 |
. . 3
|
325 | 168, 172 | eqtrd 2656 |
. . . . 5
|
326 | 325 | adantr 481 |
. . . 4
|
327 | 230 | oveq1d 6665 |
. . . . . . . . 9
|
328 | 301, 109,
107 | adddird 10065 |
. . . . . . . . . . 11
|
329 | 107 | mulid2d 10058 |
. . . . . . . . . . . 12
|
330 | 329 | oveq2d 6666 |
. . . . . . . . . . 11
|
331 | 301, 107 | mulcld 10060 |
. . . . . . . . . . . 12
|
332 | 331, 107 | addcomd 10238 |
. . . . . . . . . . 11
|
333 | 328, 330,
332 | 3eqtrd 2660 |
. . . . . . . . . 10
|
334 | 333 | adantr 481 |
. . . . . . . . 9
|
335 | 50, 300 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
336 | 335 | oveq1d 6665 |
. . . . . . . . . . . 12
|
337 | 300, 50, 107 | mulassd 10063 |
. . . . . . . . . . . 12
|
338 | 336, 337 | eqtrd 2656 |
. . . . . . . . . . 11
|
339 | 338 | oveq2d 6666 |
. . . . . . . . . 10
|
340 | 339 | adantr 481 |
. . . . . . . . 9
|
341 | 327, 334,
340 | 3eqtrd 2660 |
. . . . . . . 8
|
342 | 341 | oveq2d 6666 |
. . . . . . 7
|
343 | 193 | adantr 481 |
. . . . . . . 8
|
344 | 14 | a1i 11 |
. . . . . . . 8
|
345 | 306 | adantr 481 |
. . . . . . . 8
|
346 | 343, 344,
345 | addassd 10062 |
. . . . . . 7
|
347 | 342, 346 | eqtr4d 2659 |
. . . . . 6
|
348 | 347 | fveq2d 6195 |
. . . . 5
|
349 | 348 | oveq1d 6665 |
. . . 4
|
350 | 193, 107 | addcld 10059 |
. . . . . . . . 9
|
351 | | sinper 24233 |
. . . . . . . . 9
|
352 | 350, 262,
351 | syl2anc 693 |
. . . . . . . 8
|
353 | | sinppi 24241 |
. . . . . . . . 9
|
354 | 193, 353 | syl 17 |
. . . . . . . 8
|
355 | 352, 354 | eqtrd 2656 |
. . . . . . 7
|
356 | 355 | oveq1d 6665 |
. . . . . 6
|
357 | 195 | oveq2d 6666 |
. . . . . 6
|
358 | 194, 194,
215 | divnegd 10814 |
. . . . . . . . 9
|
359 | 218 | negeqd 10275 |
. . . . . . . . 9
|
360 | 358, 359 | eqtr3d 2658 |
. . . . . . . 8
|
361 | 360 | oveq1d 6665 |
. . . . . . 7
|
362 | 194 | negcld 10379 |
. . . . . . . 8
|
363 | 362, 194,
192, 215, 216 | divdiv1d 10832 |
. . . . . . 7
|
364 | 86, 90 | negsubi 10359 |
. . . . . . . . . . 11
|
365 | 90, 86 | negsubdi2i 10367 |
. . . . . . . . . . 11
|
366 | | 1mhlfehlf 11251 |
. . . . . . . . . . . . 13
|
367 | 366 | negeqi 10274 |
. . . . . . . . . . . 12
|
368 | | divneg 10719 |
. . . . . . . . . . . . 13
|
369 | 90, 118, 51, 368 | mp3an 1424 |
. . . . . . . . . . . 12
|
370 | 367, 369 | eqtri 2644 |
. . . . . . . . . . 11
|
371 | 364, 365,
370 | 3eqtr2i 2650 |
. . . . . . . . . 10
|
372 | 371 | oveq1i 6660 |
. . . . . . . . 9
|
373 | | divdiv1 10736 |
. . . . . . . . . 10
|
374 | 316, 91, 95, 373 | mp3an 1424 |
. . . . . . . . 9
|
375 | 372, 374 | eqtr2i 2645 |
. . . . . . . 8
|
376 | 375 | a1i 11 |
. . . . . . 7
|
377 | 361, 363,
376 | 3eqtr3d 2664 |
. . . . . 6
|
378 | 356, 357,
377 | 3eqtrd 2660 |
. . . . 5
|
379 | 378 | adantr 481 |
. . . 4
|
380 | 326, 349,
379 | 3eqtrrd 2661 |
. . 3
|
381 | 225, 324,
380 | 3eqtrd 2660 |
. 2
|
382 | 224, 381 | pm2.61dan 832 |
1
|