Proof of Theorem itgsinexplem1
Step | Hyp | Ref
| Expression |
1 | | 0m0e0 11130 |
. . . . 5
|
2 | 1 | oveq1i 6660 |
. . . 4
|
3 | | 0re 10040 |
. . . . . 6
|
4 | 3 | a1i 11 |
. . . . 5
|
5 | | pire 24210 |
. . . . . 6
|
6 | 5 | a1i 11 |
. . . . 5
|
7 | | pipos 24212 |
. . . . . . 7
|
8 | 3, 5, 7 | ltleii 10160 |
. . . . . 6
|
9 | 8 | a1i 11 |
. . . . 5
|
10 | 3, 5 | pm3.2i 471 |
. . . . . . . . . . . . 13
|
11 | | iccssre 12255 |
. . . . . . . . . . . . 13
|
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . 12
|
13 | | ax-resscn 9993 |
. . . . . . . . . . . 12
|
14 | 12, 13 | sstri 3612 |
. . . . . . . . . . 11
|
15 | 14 | sseli 3599 |
. . . . . . . . . 10
|
16 | 15 | adantl 482 |
. . . . . . . . 9
|
17 | 15 | sincld 14860 |
. . . . . . . . . . 11
|
18 | 17 | adantl 482 |
. . . . . . . . . 10
|
19 | | itgsinexplem1.7 |
. . . . . . . . . . . 12
|
20 | 19 | nnnn0d 11351 |
. . . . . . . . . . 11
|
21 | 20 | adantr 481 |
. . . . . . . . . 10
|
22 | 18, 21 | expcld 13008 |
. . . . . . . . 9
|
23 | | itgsinexplem1.1 |
. . . . . . . . . 10
|
24 | 23 | fvmpt2 6291 |
. . . . . . . . 9
|
25 | 16, 22, 24 | syl2anc 693 |
. . . . . . . 8
|
26 | 25 | eqcomd 2628 |
. . . . . . 7
|
27 | 26 | mpteq2dva 4744 |
. . . . . 6
|
28 | | nfmpt1 4747 |
. . . . . . . 8
|
29 | 23, 28 | nfcxfr 2762 |
. . . . . . 7
|
30 | | nfcv 2764 |
. . . . . . . . 9
|
31 | | sincn 24198 |
. . . . . . . . . 10
|
32 | 31 | a1i 11 |
. . . . . . . . 9
|
33 | 30, 32, 20 | expcnfg 39823 |
. . . . . . . 8
|
34 | 23, 33 | syl5eqel 2705 |
. . . . . . 7
|
35 | 14 | a1i 11 |
. . . . . . 7
|
36 | 29, 34, 35 | cncfmptss 39819 |
. . . . . 6
|
37 | 27, 36 | eqeltrd 2701 |
. . . . 5
|
38 | 15 | coscld 14861 |
. . . . . . . . . . 11
|
39 | 38 | negcld 10379 |
. . . . . . . . . 10
|
40 | | itgsinexplem1.2 |
. . . . . . . . . . 11
|
41 | 40 | fvmpt2 6291 |
. . . . . . . . . 10
|
42 | 15, 39, 41 | syl2anc 693 |
. . . . . . . . 9
|
43 | 42 | eqcomd 2628 |
. . . . . . . 8
|
44 | 43 | adantl 482 |
. . . . . . 7
|
45 | 44 | mpteq2dva 4744 |
. . . . . 6
|
46 | | nfmpt1 4747 |
. . . . . . . 8
|
47 | 40, 46 | nfcxfr 2762 |
. . . . . . 7
|
48 | | coscn 24199 |
. . . . . . . . 9
|
49 | 48 | a1i 11 |
. . . . . . . 8
|
50 | 40 | negfcncf 22722 |
. . . . . . . 8
|
51 | 49, 50 | syl 17 |
. . . . . . 7
|
52 | 47, 51, 35 | cncfmptss 39819 |
. . . . . 6
|
53 | 45, 52 | eqeltrd 2701 |
. . . . 5
|
54 | | itgsinexplem1.3 |
. . . . . 6
|
55 | | ssid 3624 |
. . . . . . . . . . 11
|
56 | 55 | a1i 11 |
. . . . . . . . . 10
|
57 | 19 | nncnd 11036 |
. . . . . . . . . 10
|
58 | 56, 57, 56 | constcncfg 40084 |
. . . . . . . . 9
|
59 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
60 | 19, 59 | syl 17 |
. . . . . . . . . 10
|
61 | 30, 32, 60 | expcnfg 39823 |
. . . . . . . . 9
|
62 | 58, 61 | mulcncf 23215 |
. . . . . . . 8
|
63 | | cosf 14855 |
. . . . . . . . . . 11
|
64 | 63 | a1i 11 |
. . . . . . . . . 10
|
65 | 64 | feqmptd 6249 |
. . . . . . . . 9
|
66 | 65, 48 | syl6eqelr 2710 |
. . . . . . . 8
|
67 | 62, 66 | mulcncf 23215 |
. . . . . . 7
|
68 | 54, 67 | syl5eqel 2705 |
. . . . . 6
|
69 | | ioosscn 39716 |
. . . . . . 7
|
70 | 69 | a1i 11 |
. . . . . 6
|
71 | 57 | adantr 481 |
. . . . . . . 8
|
72 | 69 | sseli 3599 |
. . . . . . . . . . 11
|
73 | 72 | sincld 14860 |
. . . . . . . . . 10
|
74 | 73 | adantl 482 |
. . . . . . . . 9
|
75 | 60 | adantr 481 |
. . . . . . . . 9
|
76 | 74, 75 | expcld 13008 |
. . . . . . . 8
|
77 | 71, 76 | mulcld 10060 |
. . . . . . 7
|
78 | 72 | coscld 14861 |
. . . . . . . 8
|
79 | 78 | adantl 482 |
. . . . . . 7
|
80 | 77, 79 | mulcld 10060 |
. . . . . 6
|
81 | 54, 68, 70, 56, 80 | cncfmptssg 40083 |
. . . . 5
|
82 | 30, 32, 70 | cncfmptss 39819 |
. . . . 5
|
83 | | ioossicc 12259 |
. . . . . . 7
|
84 | 83 | a1i 11 |
. . . . . 6
|
85 | | ioombl 23333 |
. . . . . . 7
|
86 | 85 | a1i 11 |
. . . . . 6
|
87 | 22, 18 | mulcld 10060 |
. . . . . 6
|
88 | | itgsinexplem1.4 |
. . . . . . . . . . . 12
|
89 | 88 | fvmpt2 6291 |
. . . . . . . . . . 11
|
90 | 16, 87, 89 | syl2anc 693 |
. . . . . . . . . 10
|
91 | 90 | eqcomd 2628 |
. . . . . . . . 9
|
92 | 91 | mpteq2dva 4744 |
. . . . . . . 8
|
93 | | nfmpt1 4747 |
. . . . . . . . . 10
|
94 | 88, 93 | nfcxfr 2762 |
. . . . . . . . 9
|
95 | | sinf 14854 |
. . . . . . . . . . . . . 14
|
96 | 95 | a1i 11 |
. . . . . . . . . . . . 13
|
97 | 96 | feqmptd 6249 |
. . . . . . . . . . . 12
|
98 | 97, 31 | syl6eqelr 2710 |
. . . . . . . . . . 11
|
99 | 33, 98 | mulcncf 23215 |
. . . . . . . . . 10
|
100 | 88, 99 | syl5eqel 2705 |
. . . . . . . . 9
|
101 | 94, 100, 35 | cncfmptss 39819 |
. . . . . . . 8
|
102 | 92, 101 | eqeltrd 2701 |
. . . . . . 7
|
103 | | cniccibl 23607 |
. . . . . . 7
|
104 | 4, 6, 102, 103 | syl3anc 1326 |
. . . . . 6
|
105 | 84, 86, 87, 104 | iblss 23571 |
. . . . 5
|
106 | 57 | adantr 481 |
. . . . . . . . 9
|
107 | 60 | adantr 481 |
. . . . . . . . . 10
|
108 | 18, 107 | expcld 13008 |
. . . . . . . . 9
|
109 | 106, 108 | mulcld 10060 |
. . . . . . . 8
|
110 | 38 | adantl 482 |
. . . . . . . 8
|
111 | 109, 110 | mulcld 10060 |
. . . . . . 7
|
112 | 39 | adantl 482 |
. . . . . . 7
|
113 | 111, 112 | mulcld 10060 |
. . . . . 6
|
114 | | itgsinexplem1.5 |
. . . . . . . 8
|
115 | | eqid 2622 |
. . . . . . . . . . . 12
|
116 | 115 | negfcncf 22722 |
. . . . . . . . . . 11
|
117 | 49, 116 | syl 17 |
. . . . . . . . . 10
|
118 | 67, 117 | mulcncf 23215 |
. . . . . . . . 9
|
119 | 114, 118 | syl5eqel 2705 |
. . . . . . . 8
|
120 | 114, 119,
35, 56, 113 | cncfmptssg 40083 |
. . . . . . 7
|
121 | | cniccibl 23607 |
. . . . . . 7
|
122 | 4, 6, 120, 121 | syl3anc 1326 |
. . . . . 6
|
123 | 84, 86, 113, 122 | iblss 23571 |
. . . . 5
|
124 | | reelprrecn 10028 |
. . . . . . 7
|
125 | 124 | a1i 11 |
. . . . . 6
|
126 | | recn 10026 |
. . . . . . . . 9
|
127 | 126 | sincld 14860 |
. . . . . . . 8
|
128 | 127 | adantl 482 |
. . . . . . 7
|
129 | 20 | adantr 481 |
. . . . . . 7
|
130 | 128, 129 | expcld 13008 |
. . . . . 6
|
131 | 57 | adantr 481 |
. . . . . . . 8
|
132 | 60 | adantr 481 |
. . . . . . . . 9
|
133 | 128, 132 | expcld 13008 |
. . . . . . . 8
|
134 | 131, 133 | mulcld 10060 |
. . . . . . 7
|
135 | 126 | coscld 14861 |
. . . . . . . 8
|
136 | 135 | adantl 482 |
. . . . . . 7
|
137 | 134, 136 | mulcld 10060 |
. . . . . 6
|
138 | | sincl 14856 |
. . . . . . . . . . 11
|
139 | 138 | adantl 482 |
. . . . . . . . . 10
|
140 | 20 | adantr 481 |
. . . . . . . . . 10
|
141 | 139, 140 | expcld 13008 |
. . . . . . . . 9
|
142 | 141, 23 | fmptd 6385 |
. . . . . . . 8
|
143 | 126 | adantl 482 |
. . . . . . . . . . . . . 14
|
144 | | elex 3212 |
. . . . . . . . . . . . . . 15
|
145 | 137, 144 | syl 17 |
. . . . . . . . . . . . . 14
|
146 | | rabid 3116 |
. . . . . . . . . . . . . 14
|
147 | 143, 145,
146 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
148 | 54 | dmmpt 5630 |
. . . . . . . . . . . . 13
|
149 | 147, 148 | syl6eleqr 2712 |
. . . . . . . . . . . 12
|
150 | 149 | ex 450 |
. . . . . . . . . . 11
|
151 | 150 | alrimiv 1855 |
. . . . . . . . . 10
|
152 | | nfcv 2764 |
. . . . . . . . . . 11
|
153 | | nfmpt1 4747 |
. . . . . . . . . . . . 13
|
154 | 54, 153 | nfcxfr 2762 |
. . . . . . . . . . . 12
|
155 | 154 | nfdm 5367 |
. . . . . . . . . . 11
|
156 | 152, 155 | dfss2f 3594 |
. . . . . . . . . 10
|
157 | 151, 156 | sylibr 224 |
. . . . . . . . 9
|
158 | 19 | dvsinexp 40125 |
. . . . . . . . . . 11
|
159 | 23 | oveq2i 6661 |
. . . . . . . . . . 11
|
160 | 158, 159,
54 | 3eqtr4g 2681 |
. . . . . . . . . 10
|
161 | 160 | dmeqd 5326 |
. . . . . . . . 9
|
162 | 157, 161 | sseqtr4d 3642 |
. . . . . . . 8
|
163 | | dvres3 23677 |
. . . . . . . 8
|
164 | 125, 142,
56, 162, 163 | syl22anc 1327 |
. . . . . . 7
|
165 | 23 | reseq1i 5392 |
. . . . . . . . . 10
|
166 | | resmpt 5449 |
. . . . . . . . . . 11
|
167 | 13, 166 | ax-mp 5 |
. . . . . . . . . 10
|
168 | 165, 167 | eqtri 2644 |
. . . . . . . . 9
|
169 | 168 | oveq2i 6661 |
. . . . . . . 8
|
170 | 169 | a1i 11 |
. . . . . . 7
|
171 | 160 | reseq1d 5395 |
. . . . . . . 8
|
172 | 54 | reseq1i 5392 |
. . . . . . . . 9
|
173 | | resmpt 5449 |
. . . . . . . . . 10
|
174 | 13, 173 | ax-mp 5 |
. . . . . . . . 9
|
175 | 172, 174 | eqtri 2644 |
. . . . . . . 8
|
176 | 171, 175 | syl6eq 2672 |
. . . . . . 7
|
177 | 164, 170,
176 | 3eqtr3d 2664 |
. . . . . 6
|
178 | 12 | a1i 11 |
. . . . . 6
|
179 | | eqid 2622 |
. . . . . . 7
ℂfld ℂfld |
180 | 179 | tgioo2 22606 |
. . . . . 6
ℂfld
↾t |
181 | 10 | a1i 11 |
. . . . . . 7
|
182 | | iccntr 22624 |
. . . . . . 7
|
183 | 181, 182 | syl 17 |
. . . . . 6
|
184 | 125, 130,
137, 177, 178, 180, 179, 183 | dvmptres2 23725 |
. . . . 5
|
185 | 135 | negcld 10379 |
. . . . . . 7
|
186 | 185 | adantl 482 |
. . . . . 6
|
187 | 127 | negcld 10379 |
. . . . . . . . 9
|
188 | 187 | adantl 482 |
. . . . . . . 8
|
189 | | dvcosre 40126 |
. . . . . . . . 9
|
190 | 189 | a1i 11 |
. . . . . . . 8
|
191 | 125, 136,
188, 190 | dvmptneg 23729 |
. . . . . . 7
|
192 | 127 | negnegd 10383 |
. . . . . . . . 9
|
193 | 192 | adantl 482 |
. . . . . . . 8
|
194 | 193 | mpteq2dva 4744 |
. . . . . . 7
|
195 | 191, 194 | eqtrd 2656 |
. . . . . 6
|
196 | 125, 186,
128, 195, 178, 180, 179, 183 | dvmptres2 23725 |
. . . . 5
|
197 | | fveq2 6191 |
. . . . . . . . . . 11
|
198 | | sin0 14879 |
. . . . . . . . . . 11
|
199 | 197, 198 | syl6eq 2672 |
. . . . . . . . . 10
|
200 | 199 | oveq1d 6665 |
. . . . . . . . 9
|
201 | 200 | adantl 482 |
. . . . . . . 8
|
202 | 19 | adantr 481 |
. . . . . . . . 9
|
203 | 202 | 0expd 13024 |
. . . . . . . 8
|
204 | 201, 203 | eqtrd 2656 |
. . . . . . 7
|
205 | 204 | oveq1d 6665 |
. . . . . 6
|
206 | | id 22 |
. . . . . . . . . 10
|
207 | | 0cn 10032 |
. . . . . . . . . 10
|
208 | 206, 207 | syl6eqel 2709 |
. . . . . . . . 9
|
209 | | coscl 14857 |
. . . . . . . . . 10
|
210 | 209 | negcld 10379 |
. . . . . . . . 9
|
211 | 208, 210 | syl 17 |
. . . . . . . 8
|
212 | 211 | adantl 482 |
. . . . . . 7
|
213 | 212 | mul02d 10234 |
. . . . . 6
|
214 | 205, 213 | eqtrd 2656 |
. . . . 5
|
215 | | fveq2 6191 |
. . . . . . . . . . 11
|
216 | | sinpi 24209 |
. . . . . . . . . . 11
|
217 | 215, 216 | syl6eq 2672 |
. . . . . . . . . 10
|
218 | 217 | oveq1d 6665 |
. . . . . . . . 9
|
219 | 218 | adantl 482 |
. . . . . . . 8
|
220 | 19 | adantr 481 |
. . . . . . . . 9
|
221 | 220 | 0expd 13024 |
. . . . . . . 8
|
222 | 219, 221 | eqtrd 2656 |
. . . . . . 7
|
223 | 222 | oveq1d 6665 |
. . . . . 6
|
224 | | id 22 |
. . . . . . . . . . 11
|
225 | | picn 24211 |
. . . . . . . . . . 11
|
226 | 224, 225 | syl6eqel 2709 |
. . . . . . . . . 10
|
227 | 226 | coscld 14861 |
. . . . . . . . 9
|
228 | 227 | negcld 10379 |
. . . . . . . 8
|
229 | 228 | adantl 482 |
. . . . . . 7
|
230 | 229 | mul02d 10234 |
. . . . . 6
|
231 | 223, 230 | eqtrd 2656 |
. . . . 5
|
232 | 4, 6, 9, 37, 53, 81, 82, 105, 123, 184, 196, 214, 231 | itgparts 23810 |
. . . 4
|
233 | | df-neg 10269 |
. . . . 5
|
234 | 233 | a1i 11 |
. . . 4
|
235 | 2, 232, 234 | 3eqtr4a 2682 |
. . 3
|
236 | 77, 79, 79 | mulassd 10063 |
. . . . . . . . 9
|
237 | | sqval 12922 |
. . . . . . . . . . . . . 14
|
238 | 237 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
239 | 78, 238 | syl 17 |
. . . . . . . . . . . 12
|
240 | 239 | adantl 482 |
. . . . . . . . . . 11
|
241 | 240 | oveq2d 6666 |
. . . . . . . . . 10
|
242 | 78 | sqcld 13006 |
. . . . . . . . . . . 12
|
243 | 242 | adantl 482 |
. . . . . . . . . . 11
|
244 | 71, 76, 243 | mulassd 10063 |
. . . . . . . . . 10
|
245 | 241, 244 | eqtrd 2656 |
. . . . . . . . 9
|
246 | 76, 243 | mulcomd 10061 |
. . . . . . . . . 10
|
247 | 246 | oveq2d 6666 |
. . . . . . . . 9
|
248 | 236, 245,
247 | 3eqtrd 2660 |
. . . . . . . 8
|
249 | 248 | negeqd 10275 |
. . . . . . 7
|
250 | 80, 79 | mulneg2d 10484 |
. . . . . . 7
|
251 | 243, 76 | mulcld 10060 |
. . . . . . . 8
|
252 | 71, 251 | mulneg1d 10483 |
. . . . . . 7
|
253 | 249, 250,
252 | 3eqtr4d 2666 |
. . . . . 6
|
254 | 253 | itgeq2dv 23548 |
. . . . 5
|
255 | 57 | negcld 10379 |
. . . . . 6
|
256 | 38 | sqcld 13006 |
. . . . . . . . 9
|
257 | 256 | adantl 482 |
. . . . . . . 8
|
258 | 257, 108 | mulcld 10060 |
. . . . . . 7
|
259 | | itgsinexplem1.6 |
. . . . . . . . . . . . 13
|
260 | 259 | fvmpt2 6291 |
. . . . . . . . . . . 12
|
261 | 16, 258, 260 | syl2anc 693 |
. . . . . . . . . . 11
|
262 | 261 | eqcomd 2628 |
. . . . . . . . . 10
|
263 | 262 | mpteq2dva 4744 |
. . . . . . . . 9
|
264 | | nfmpt1 4747 |
. . . . . . . . . . 11
|
265 | 259, 264 | nfcxfr 2762 |
. . . . . . . . . 10
|
266 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
267 | | 2nn0 11309 |
. . . . . . . . . . . . . 14
|
268 | 267 | a1i 11 |
. . . . . . . . . . . . 13
|
269 | 266, 49, 268 | expcnfg 39823 |
. . . . . . . . . . . 12
|
270 | 269, 61 | mulcncf 23215 |
. . . . . . . . . . 11
|
271 | 259, 270 | syl5eqel 2705 |
. . . . . . . . . 10
|
272 | 265, 271,
35 | cncfmptss 39819 |
. . . . . . . . 9
|
273 | 263, 272 | eqeltrd 2701 |
. . . . . . . 8
|
274 | | cniccibl 23607 |
. . . . . . . 8
|
275 | 4, 6, 273, 274 | syl3anc 1326 |
. . . . . . 7
|
276 | 84, 86, 258, 275 | iblss 23571 |
. . . . . 6
|
277 | 255, 251,
276 | itgmulc2 23600 |
. . . . 5
|
278 | 254, 277 | eqtr4d 2659 |
. . . 4
|
279 | 278 | negeqd 10275 |
. . 3
|
280 | 235, 279 | eqtrd 2656 |
. 2
|
281 | 251, 276 | itgcl 23550 |
. . . 4
|
282 | 57, 281 | mulneg1d 10483 |
. . 3
|
283 | 282 | negeqd 10275 |
. 2
|
284 | 57, 281 | mulcld 10060 |
. . 3
|
285 | 284 | negnegd 10383 |
. 2
|
286 | 280, 283,
285 | 3eqtrd 2660 |
1
|