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 | | iblrelem.1 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
6 | | itgreval.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 | 5 | rered 15118 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) = ๐ต) |
9 | 8 | ibllem 25152 |
. . . . . 6
โข (๐ โ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0) = if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0)) |
10 | 9 | mpteq2dv 5211 |
. . . . 5
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) |
11 | 10 | fveq2d 6850 |
. . . 4
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0)))) |
12 | 8 | negeqd 11403 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) = -๐ต) |
13 | 12 | ibllem 25152 |
. . . . . 6
โข (๐ โ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0) = if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0)) |
14 | 13 | mpteq2dv 5211 |
. . . . 5
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))) |
15 | 14 | fveq2d 6850 |
. . . 4
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0)))) |
16 | 11, 15 | oveq12d 7379 |
. . 3
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))) =
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))))) |
17 | 5 | reim0d 15119 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) = 0) |
18 | 17 | itgvallem3 25173 |
. . . . . . 7
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) = 0) |
19 | 17 | negeqd 11403 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) = -0) |
20 | | neg0 11455 |
. . . . . . . . 9
โข -0 =
0 |
21 | 19, 20 | eqtrdi 2789 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) = 0) |
22 | 21 | itgvallem3 25173 |
. . . . . . 7
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) = 0) |
23 | 18, 22 | oveq12d 7379 |
. . . . . 6
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))) = (0 โ
0)) |
24 | | 0m0e0 12281 |
. . . . . 6
โข (0
โ 0) = 0 |
25 | 23, 24 | eqtrdi 2789 |
. . . . 5
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))) = 0) |
26 | 25 | oveq2d 7377 |
. . . 4
โข (๐ โ (i ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))))) = (i ยท
0)) |
27 | | it0e0 12383 |
. . . 4
โข (i
ยท 0) = 0 |
28 | 26, 27 | eqtrdi 2789 |
. . 3
โข (๐ โ (i ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))))) = 0) |
29 | 16, 28 | oveq12d 7379 |
. 2
โข (๐ โ
(((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))) + (i ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)))))) =
(((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0)))) + 0)) |
30 | 5 | iblrelem 25178 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ โ โง
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))) โ โ))) |
31 | 6, 30 | mpbid 231 |
. . . . . 6
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ โ โง
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))) โ โ)) |
32 | 31 | simp2d 1144 |
. . . . 5
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ โ) |
33 | 31 | simp3d 1145 |
. . . . 5
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))) โ โ) |
34 | 32, 33 | resubcld 11591 |
. . . 4
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0)))) โ โ) |
35 | 34 | recnd 11191 |
. . 3
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0)))) โ โ) |
36 | 35 | addid1d 11363 |
. 2
โข (๐ โ
(((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0)))) + 0) =
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))))) |
37 | 7, 29, 36 | 3eqtrd 2777 |
1
โข (๐ โ โซ๐ด๐ต d๐ฅ = ((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))))) |