Step | Hyp | Ref
| Expression |
1 | | ftc2nc.a |
. . . . . . 7
|
2 | 1 | rexrd 10089 |
. . . . . 6
|
3 | | ftc2nc.b |
. . . . . . 7
|
4 | 3 | rexrd 10089 |
. . . . . 6
|
5 | | ftc2nc.le |
. . . . . 6
|
6 | | ubicc2 12289 |
. . . . . 6
|
7 | 2, 4, 5, 6 | syl3anc 1326 |
. . . . 5
|
8 | | fvex 6201 |
. . . . . 6
|
9 | 8 | fvconst2 6469 |
. . . . 5
|
10 | 7, 9 | syl 17 |
. . . 4
|
11 | | eqid 2622 |
. . . . . . . 8
ℂfld ℂfld |
12 | 11 | subcn 22669 |
. . . . . . . . 9
ℂfld ℂfld ℂfld |
13 | 12 | a1i 11 |
. . . . . . . 8
ℂfld
ℂfld ℂfld |
14 | | eqid 2622 |
. . . . . . . . 9
|
15 | | ssid 3624 |
. . . . . . . . . 10
|
16 | 15 | a1i 11 |
. . . . . . . . 9
|
17 | | ioossre 12235 |
. . . . . . . . . 10
|
18 | 17 | a1i 11 |
. . . . . . . . 9
|
19 | | ftc2nc.i |
. . . . . . . . 9
|
20 | | ftc2nc.c |
. . . . . . . . . 10
|
21 | | cncff 22696 |
. . . . . . . . . 10
|
22 | 20, 21 | syl 17 |
. . . . . . . . 9
|
23 | | ioof 12271 |
. . . . . . . . . . . . 13
|
24 | | ffun 6048 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . 12
|
26 | | fvelima 6248 |
. . . . . . . . . . . 12
|
27 | 25, 26 | mpan 706 |
. . . . . . . . . . 11
|
28 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . 17
|
29 | 28 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
30 | | df-ov 6653 |
. . . . . . . . . . . . . . . 16
|
31 | 29, 30 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
32 | 31 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
33 | 32 | adantl 482 |
. . . . . . . . . . . . 13
|
34 | 2, 4 | jca 554 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | elicc1 12219 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | 2, 4, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 38 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 39 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 36, 40 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
|
42 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | | iccleub 12229 |
. . . . . . . . . . . . . . . . . . . . 21
|
44 | 43 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | 34, 42, 44 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | ioossioo 12265 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 35, 41, 45, 46 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
|
49 | 22 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
50 | 49 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
51 | 48, 50 | syldan 487 |
. . . . . . . . . . . . . . . 16
|
52 | | ioombl 23333 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
54 | | fvexd 6203 |
. . . . . . . . . . . . . . . . 17
|
55 | 22 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55, 19 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
58 | 47, 53, 54, 57 | iblss 23571 |
. . . . . . . . . . . . . . . 16
|
59 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | | cncfss 22702 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 59, 60, 61 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | | abscncf 22704 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | 62, 63 | sselii 3600 |
. . . . . . . . . . . . . . . . . . 19
|
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
66 | 55 | reseq1d 5395 |
. . . . . . . . . . . . . . . . . . . . 21
|
67 | 66 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | 47 | resmptd 5452 |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 67, 68 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | | rescncf 22700 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 47, 70, 71 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 69, 72 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
|
74 | 65, 73 | cncfmpt1f 22716 |
. . . . . . . . . . . . . . . . 17
|
75 | | cnmbf 23426 |
. . . . . . . . . . . . . . . . 17
MblFn |
76 | 52, 74, 75 | sylancr 695 |
. . . . . . . . . . . . . . . 16
MblFn |
77 | 51, 58 | itgcl 23550 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 77 | cjcld 13936 |
. . . . . . . . . . . . . . . . . . 19
|
79 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 79, 59 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | | cncfmptc 22714 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 80, 60, 81 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 78, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
84 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | 84, 85, 86 | cbvmpt 4749 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 87, 73 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . . . 18
|
89 | 83, 88 | mulcncf 23215 |
. . . . . . . . . . . . . . . . 17
|
90 | | cnmbf 23426 |
. . . . . . . . . . . . . . . . 17
MblFn |
91 | 52, 89, 90 | sylancr 695 |
. . . . . . . . . . . . . . . 16
MblFn |
92 | 51, 58, 76, 91 | itgabsnc 33479 |
. . . . . . . . . . . . . . 15
|
93 | 51 | abscld 14175 |
. . . . . . . . . . . . . . . 16
|
94 | | fvexd 6203 |
. . . . . . . . . . . . . . . . 17
|
95 | 94, 58, 76 | iblabsnc 33474 |
. . . . . . . . . . . . . . . 16
|
96 | 51 | absge0d 14183 |
. . . . . . . . . . . . . . . 16
|
97 | 93, 95, 96 | itgposval 23562 |
. . . . . . . . . . . . . . 15
|
98 | 92, 97 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
99 | | itgeq1 23539 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
101 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . 18
|
102 | 101 | ifbid 4108 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
|
104 | 103 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
105 | 100, 104 | breq12d 4666 |
. . . . . . . . . . . . . 14
|
106 | 98, 105 | syl5ibcom 235 |
. . . . . . . . . . . . 13
|
107 | 33, 106 | sylbid 230 |
. . . . . . . . . . . 12
|
108 | 107 | rexlimdva 3031 |
. . . . . . . . . . 11
|
109 | 27, 108 | syl5 34 |
. . . . . . . . . 10
|
110 | 109 | ralrimiv 2965 |
. . . . . . . . 9
|
111 | 14, 1, 3, 5, 16, 18, 19, 22, 110 | ftc1anc 33493 |
. . . . . . . 8
|
112 | | ftc2nc.f |
. . . . . . . . . . 11
|
113 | | cncff 22696 |
. . . . . . . . . . 11
|
114 | 112, 113 | syl 17 |
. . . . . . . . . 10
|
115 | 114 | feqmptd 6249 |
. . . . . . . . 9
|
116 | 115, 112 | eqeltrrd 2702 |
. . . . . . . 8
|
117 | 11, 13, 111, 116 | cncfmpt2f 22717 |
. . . . . . 7
|
118 | 59 | a1i 11 |
. . . . . . . . . 10
|
119 | | iccssre 12255 |
. . . . . . . . . . 11
|
120 | 1, 3, 119 | syl2anc 693 |
. . . . . . . . . 10
|
121 | | fvexd 6203 |
. . . . . . . . . . . 12
|
122 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
|
123 | 122 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
124 | | elicc2 12238 |
. . . . . . . . . . . . . . . . 17
|
125 | 1, 3, 124 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
126 | 125 | biimpa 501 |
. . . . . . . . . . . . . . 15
|
127 | 126 | simp3d 1075 |
. . . . . . . . . . . . . 14
|
128 | | iooss2 12211 |
. . . . . . . . . . . . . 14
|
129 | 123, 127,
128 | syl2anc 693 |
. . . . . . . . . . . . 13
|
130 | | ioombl 23333 |
. . . . . . . . . . . . . 14
|
131 | 130 | a1i 11 |
. . . . . . . . . . . . 13
|
132 | | fvexd 6203 |
. . . . . . . . . . . . 13
|
133 | 56 | adantr 481 |
. . . . . . . . . . . . 13
|
134 | 129, 131,
132, 133 | iblss 23571 |
. . . . . . . . . . . 12
|
135 | 121, 134 | itgcl 23550 |
. . . . . . . . . . 11
|
136 | 114 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
137 | 135, 136 | subcld 10392 |
. . . . . . . . . 10
|
138 | 11 | tgioo2 22606 |
. . . . . . . . . 10
ℂfld
↾t |
139 | | iccntr 22624 |
. . . . . . . . . . 11
|
140 | 1, 3, 139 | syl2anc 693 |
. . . . . . . . . 10
|
141 | 118, 120,
137, 138, 11, 140 | dvmptntr 23734 |
. . . . . . . . 9
|
142 | | reelprrecn 10028 |
. . . . . . . . . . 11
|
143 | 142 | a1i 11 |
. . . . . . . . . 10
|
144 | | ioossicc 12259 |
. . . . . . . . . . . 12
|
145 | 144 | sseli 3599 |
. . . . . . . . . . 11
|
146 | 145, 135 | sylan2 491 |
. . . . . . . . . 10
|
147 | 22 | ffvelrnda 6359 |
. . . . . . . . . 10
|
148 | 14, 1, 3, 5, 20, 19 | ftc1cnnc 33484 |
. . . . . . . . . . 11
|
149 | 118, 120,
135, 138, 11, 140 | dvmptntr 23734 |
. . . . . . . . . . 11
|
150 | 22 | feqmptd 6249 |
. . . . . . . . . . 11
|
151 | 148, 149,
150 | 3eqtr3d 2664 |
. . . . . . . . . 10
|
152 | 145, 136 | sylan2 491 |
. . . . . . . . . 10
|
153 | 115 | oveq2d 6666 |
. . . . . . . . . . 11
|
154 | 118, 120,
136, 138, 11, 140 | dvmptntr 23734 |
. . . . . . . . . . 11
|
155 | 153, 150,
154 | 3eqtr3rd 2665 |
. . . . . . . . . 10
|
156 | 143, 146,
147, 151, 152, 147, 155 | dvmptsub 23730 |
. . . . . . . . 9
|
157 | 147 | subidd 10380 |
. . . . . . . . . 10
|
158 | 157 | mpteq2dva 4744 |
. . . . . . . . 9
|
159 | 141, 156,
158 | 3eqtrd 2660 |
. . . . . . . 8
|
160 | | fconstmpt 5163 |
. . . . . . . 8
|
161 | 159, 160 | syl6eqr 2674 |
. . . . . . 7
|
162 | 1, 3, 117, 161 | dveq0 23763 |
. . . . . 6
|
163 | 162 | fveq1d 6193 |
. . . . 5
|
164 | | oveq2 6658 |
. . . . . . . . 9
|
165 | | itgeq1 23539 |
. . . . . . . . 9
|
166 | 164, 165 | syl 17 |
. . . . . . . 8
|
167 | | fveq2 6191 |
. . . . . . . 8
|
168 | 166, 167 | oveq12d 6668 |
. . . . . . 7
|
169 | | eqid 2622 |
. . . . . . 7
|
170 | | ovex 6678 |
. . . . . . 7
|
171 | 168, 169,
170 | fvmpt 6282 |
. . . . . 6
|
172 | 7, 171 | syl 17 |
. . . . 5
|
173 | 163, 172 | eqtr3d 2658 |
. . . 4
|
174 | | lbicc2 12288 |
. . . . . 6
|
175 | 2, 4, 5, 174 | syl3anc 1326 |
. . . . 5
|
176 | | oveq2 6658 |
. . . . . . . . . . 11
|
177 | | iooid 12203 |
. . . . . . . . . . 11
|
178 | 176, 177 | syl6eq 2672 |
. . . . . . . . . 10
|
179 | | itgeq1 23539 |
. . . . . . . . . 10
|
180 | 178, 179 | syl 17 |
. . . . . . . . 9
|
181 | | itg0 23546 |
. . . . . . . . 9
|
182 | 180, 181 | syl6eq 2672 |
. . . . . . . 8
|
183 | | fveq2 6191 |
. . . . . . . 8
|
184 | 182, 183 | oveq12d 6668 |
. . . . . . 7
|
185 | | df-neg 10269 |
. . . . . . 7
|
186 | 184, 185 | syl6eqr 2674 |
. . . . . 6
|
187 | | negex 10279 |
. . . . . 6
|
188 | 186, 169,
187 | fvmpt 6282 |
. . . . 5
|
189 | 175, 188 | syl 17 |
. . . 4
|
190 | 10, 173, 189 | 3eqtr3d 2664 |
. . 3
|
191 | 190 | oveq2d 6666 |
. 2
|
192 | 114, 7 | ffvelrnd 6360 |
. . 3
|
193 | | fvexd 6203 |
. . . 4
|
194 | 193, 56 | itgcl 23550 |
. . 3
|
195 | 192, 194 | pncan3d 10395 |
. 2
|
196 | 114, 175 | ffvelrnd 6360 |
. . 3
|
197 | 192, 196 | negsubd 10398 |
. 2
|
198 | 191, 195,
197 | 3eqtr3d 2664 |
1
|