Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข
(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) |
2 | | eqid 2733 |
. . 3
โข
(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) |
3 | | eqid 2733 |
. . 3
โข
(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) |
4 | | eqid 2733 |
. . 3
โข
(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) |
5 | | itgcnval.1 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
6 | | itgcnval.2 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
7 | 1, 2, 3, 4, 5, 6 | itgcnlem 25177 |
. 2
โข (๐ โ โซ๐ด๐ต d๐ฅ = (((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ๐ต)),
(โโ๐ต), 0)))
โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))) + (i ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))))))) |
8 | | iblmbf 25155 |
. . . . . . 7
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
9 | 6, 8 | syl 17 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
10 | 9, 5 | mbfmptcl 25023 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
11 | 10 | recld 15088 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
12 | 10 | iblcn 25186 |
. . . . . 6
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
13 | 6, 12 | mpbid 231 |
. . . . 5
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
14 | 13 | simpld 496 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
15 | 11, 14 | itgrevallem1 25182 |
. . 3
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ = ((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ๐ต)),
(โโ๐ต), 0)))
โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))))) |
16 | 10 | imcld 15089 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
17 | 13 | simprd 497 |
. . . . 5
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
18 | 16, 17 | itgrevallem1 25182 |
. . . 4
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ = ((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ๐ต)),
(โโ๐ต), 0)))
โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))))) |
19 | 18 | oveq2d 7377 |
. . 3
โข (๐ โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) = (i ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))))) |
20 | 15, 19 | oveq12d 7379 |
. 2
โข (๐ โ (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ๐ต)),
(โโ๐ต), 0)))
โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))) + (i ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))))))) |
21 | 7, 20 | eqtr4d 2776 |
1
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |