Step | Hyp | Ref
| Expression |
1 | | itgmulc2.4 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
2 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
3 | | max0sub 13121 |
. . . . . 6
โข (๐ถ โ โ โ (if(0
โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) = ๐ถ) |
4 | 2, 3 | syl 17 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) = ๐ถ) |
5 | 4 | oveq1d 7373 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ ((if(0 โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) ยท ๐ต) = (๐ถ ยท ๐ต)) |
6 | | 0re 11162 |
. . . . . . . 8
โข 0 โ
โ |
7 | | ifcl 4532 |
. . . . . . . 8
โข ((๐ถ โ โ โง 0 โ
โ) โ if(0 โค ๐ถ, ๐ถ, 0) โ โ) |
8 | 1, 6, 7 | sylancl 587 |
. . . . . . 7
โข (๐ โ if(0 โค ๐ถ, ๐ถ, 0) โ โ) |
9 | 8 | recnd 11188 |
. . . . . 6
โข (๐ โ if(0 โค ๐ถ, ๐ถ, 0) โ โ) |
10 | 9 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค ๐ถ, ๐ถ, 0) โ โ) |
11 | 1 | renegcld 11587 |
. . . . . . . 8
โข (๐ โ -๐ถ โ โ) |
12 | | ifcl 4532 |
. . . . . . . 8
โข ((-๐ถ โ โ โง 0 โ
โ) โ if(0 โค -๐ถ, -๐ถ, 0) โ โ) |
13 | 11, 6, 12 | sylancl 587 |
. . . . . . 7
โข (๐ โ if(0 โค -๐ถ, -๐ถ, 0) โ โ) |
14 | 13 | recnd 11188 |
. . . . . 6
โข (๐ โ if(0 โค -๐ถ, -๐ถ, 0) โ โ) |
15 | 14 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -๐ถ, -๐ถ, 0) โ โ) |
16 | | itgmulc2.5 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
17 | 16 | recnd 11188 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
18 | 10, 15, 17 | subdird 11617 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ ((if(0 โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) ยท ๐ต) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต))) |
19 | 5, 18 | eqtr3d 2775 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต))) |
20 | 19 | itgeq2dv 25162 |
. 2
โข (๐ โ โซ๐ด(๐ถ ยท ๐ต) d๐ฅ = โซ๐ด((if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต)) d๐ฅ) |
21 | 8 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค ๐ถ, ๐ถ, 0) โ โ) |
22 | 21, 16 | remulcld 11190 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) โ โ) |
23 | | itgmulc2.2 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
24 | | itgmulc2.3 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
25 | 9, 23, 24 | iblmulc2 25211 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ (if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต)) โ
๐ฟ1) |
26 | 13 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -๐ถ, -๐ถ, 0) โ โ) |
27 | 26, 16 | remulcld 11190 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) โ โ) |
28 | 14, 23, 24 | iblmulc2 25211 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต)) โ
๐ฟ1) |
29 | 22, 25, 27, 28 | itgsub 25206 |
. 2
โข (๐ โ โซ๐ด((if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต)) d๐ฅ = (โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) d๐ฅ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) d๐ฅ)) |
30 | | ifcl 4532 |
. . . . . . . 8
โข ((๐ต โ โ โง 0 โ
โ) โ if(0 โค ๐ต, ๐ต, 0) โ โ) |
31 | 16, 6, 30 | sylancl 587 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค ๐ต, ๐ต, 0) โ โ) |
32 | 21, 31 | remulcld 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ โ) |
33 | 16 | iblre 25174 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ if(0 โค ๐ต, ๐ต, 0)) โ ๐ฟ1 โง
(๐ฅ โ ๐ด โฆ if(0 โค -๐ต, -๐ต, 0)) โ
๐ฟ1))) |
34 | 24, 33 | mpbid 231 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ if(0 โค ๐ต, ๐ต, 0)) โ ๐ฟ1 โง
(๐ฅ โ ๐ด โฆ if(0 โค -๐ต, -๐ต, 0)) โ
๐ฟ1)) |
35 | 34 | simpld 496 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ if(0 โค ๐ต, ๐ต, 0)) โ
๐ฟ1) |
36 | 9, 31, 35 | iblmulc2 25211 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0))) โ
๐ฟ1) |
37 | 16 | renegcld 11587 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ -๐ต โ โ) |
38 | | ifcl 4532 |
. . . . . . . 8
โข ((-๐ต โ โ โง 0 โ
โ) โ if(0 โค -๐ต, -๐ต, 0) โ โ) |
39 | 37, 6, 38 | sylancl 587 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -๐ต, -๐ต, 0) โ โ) |
40 | 21, 39 | remulcld 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) โ โ) |
41 | 34 | simprd 497 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ if(0 โค -๐ต, -๐ต, 0)) โ
๐ฟ1) |
42 | 9, 39, 41 | iblmulc2 25211 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0))) โ
๐ฟ1) |
43 | 32, 36, 40, 42 | itgsub 25206 |
. . . . 5
โข (๐ โ โซ๐ด((if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0))) d๐ฅ = (โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ โ โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ)) |
44 | | max0sub 13121 |
. . . . . . . . 9
โข (๐ต โ โ โ (if(0
โค ๐ต, ๐ต, 0) โ if(0 โค -๐ต, -๐ต, 0)) = ๐ต) |
45 | 16, 44 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ต, ๐ต, 0) โ if(0 โค -๐ต, -๐ต, 0)) = ๐ต) |
46 | 45 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท (if(0 โค ๐ต, ๐ต, 0) โ if(0 โค -๐ต, -๐ต, 0))) = (if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต)) |
47 | 31 | recnd 11188 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค ๐ต, ๐ต, 0) โ โ) |
48 | 39 | recnd 11188 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -๐ต, -๐ต, 0) โ โ) |
49 | 10, 47, 48 | subdid 11616 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท (if(0 โค ๐ต, ๐ต, 0) โ if(0 โค -๐ต, -๐ต, 0))) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)))) |
50 | 46, 49 | eqtr3d 2775 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)))) |
51 | 50 | itgeq2dv 25162 |
. . . . 5
โข (๐ โ โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) d๐ฅ = โซ๐ด((if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0))) d๐ฅ) |
52 | 16, 24 | itgreval 25177 |
. . . . . . 7
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ)) |
53 | 52 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ) = (if(0 โค ๐ถ, ๐ถ, 0) ยท (โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ))) |
54 | 31, 35 | itgcl 25164 |
. . . . . . 7
โข (๐ โ โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โ) |
55 | 39, 41 | itgcl 25164 |
. . . . . . 7
โข (๐ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ โ โ) |
56 | 9, 54, 55 | subdid 11616 |
. . . . . 6
โข (๐ โ (if(0 โค ๐ถ, ๐ถ, 0) ยท (โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ)) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ))) |
57 | | max1 13110 |
. . . . . . . . 9
โข ((0
โ โ โง ๐ถ
โ โ) โ 0 โค if(0 โค ๐ถ, ๐ถ, 0)) |
58 | 6, 1, 57 | sylancr 588 |
. . . . . . . 8
โข (๐ โ 0 โค if(0 โค ๐ถ, ๐ถ, 0)) |
59 | | max1 13110 |
. . . . . . . . 9
โข ((0
โ โ โง ๐ต
โ โ) โ 0 โค if(0 โค ๐ต, ๐ต, 0)) |
60 | 6, 16, 59 | sylancr 588 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค if(0 โค ๐ต, ๐ต, 0)) |
61 | 9, 31, 35, 8, 31, 58, 60 | itgmulc2lem1 25212 |
. . . . . . 7
โข (๐ โ (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ) = โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ) |
62 | | max1 13110 |
. . . . . . . . 9
โข ((0
โ โ โง -๐ต
โ โ) โ 0 โค if(0 โค -๐ต, -๐ต, 0)) |
63 | 6, 37, 62 | sylancr 588 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค if(0 โค -๐ต, -๐ต, 0)) |
64 | 9, 39, 41, 8, 39, 58, 63 | itgmulc2lem1 25212 |
. . . . . . 7
โข (๐ โ (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ) = โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ) |
65 | 61, 64 | oveq12d 7376 |
. . . . . 6
โข (๐ โ ((if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ) โ (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ)) = (โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ โ โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ)) |
66 | 53, 56, 65 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ) = (โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ โ โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ)) |
67 | 43, 51, 66 | 3eqtr4d 2783 |
. . . 4
โข (๐ โ โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) d๐ฅ = (if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ)) |
68 | 26, 31 | remulcld 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ โ) |
69 | 14, 31, 35 | iblmulc2 25211 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0))) โ
๐ฟ1) |
70 | 26, 39 | remulcld 11190 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) โ โ) |
71 | 14, 39, 41 | iblmulc2 25211 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0))) โ
๐ฟ1) |
72 | 68, 69, 70, 71 | itgsub 25206 |
. . . . 5
โข (๐ โ โซ๐ด((if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0))) d๐ฅ = (โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ)) |
73 | 45 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท (if(0 โค ๐ต, ๐ต, 0) โ if(0 โค -๐ต, -๐ต, 0))) = (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต)) |
74 | 15, 47, 48 | subdid 11616 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท (if(0 โค ๐ต, ๐ต, 0) โ if(0 โค -๐ต, -๐ต, 0))) = ((if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)))) |
75 | 73, 74 | eqtr3d 2775 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) = ((if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)))) |
76 | 75 | itgeq2dv 25162 |
. . . . 5
โข (๐ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) d๐ฅ = โซ๐ด((if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0))) d๐ฅ) |
77 | 52 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ) = (if(0 โค -๐ถ, -๐ถ, 0) ยท (โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ))) |
78 | 14, 54, 55 | subdid 11616 |
. . . . . 6
โข (๐ โ (if(0 โค -๐ถ, -๐ถ, 0) ยท (โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ)) = ((if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ))) |
79 | | max1 13110 |
. . . . . . . . 9
โข ((0
โ โ โง -๐ถ
โ โ) โ 0 โค if(0 โค -๐ถ, -๐ถ, 0)) |
80 | 6, 11, 79 | sylancr 588 |
. . . . . . . 8
โข (๐ โ 0 โค if(0 โค -๐ถ, -๐ถ, 0)) |
81 | 14, 31, 35, 13, 31, 80, 60 | itgmulc2lem1 25212 |
. . . . . . 7
โข (๐ โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ) = โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ) |
82 | 14, 39, 41, 13, 39, 80, 63 | itgmulc2lem1 25212 |
. . . . . . 7
โข (๐ โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ) = โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ) |
83 | 81, 82 | oveq12d 7376 |
. . . . . 6
โข (๐ โ ((if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ)) = (โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ)) |
84 | 77, 78, 83 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ) = (โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค ๐ต, ๐ต, 0)) d๐ฅ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท if(0 โค -๐ต, -๐ต, 0)) d๐ฅ)) |
85 | 72, 76, 84 | 3eqtr4d 2783 |
. . . 4
โข (๐ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) d๐ฅ = (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ)) |
86 | 67, 85 | oveq12d 7376 |
. . 3
โข (๐ โ (โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) d๐ฅ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) d๐ฅ) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ))) |
87 | 23, 24 | itgcl 25164 |
. . . 4
โข (๐ โ โซ๐ด๐ต d๐ฅ โ โ) |
88 | 9, 14, 87 | subdird 11617 |
. . 3
โข (๐ โ ((if(0 โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) ยท โซ๐ด๐ต d๐ฅ) = ((if(0 โค ๐ถ, ๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ) โ (if(0 โค -๐ถ, -๐ถ, 0) ยท โซ๐ด๐ต d๐ฅ))) |
89 | 1, 3 | syl 17 |
. . . 4
โข (๐ โ (if(0 โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) = ๐ถ) |
90 | 89 | oveq1d 7373 |
. . 3
โข (๐ โ ((if(0 โค ๐ถ, ๐ถ, 0) โ if(0 โค -๐ถ, -๐ถ, 0)) ยท โซ๐ด๐ต d๐ฅ) = (๐ถ ยท โซ๐ด๐ต d๐ฅ)) |
91 | 86, 88, 90 | 3eqtr2d 2779 |
. 2
โข (๐ โ (โซ๐ด(if(0 โค ๐ถ, ๐ถ, 0) ยท ๐ต) d๐ฅ โ โซ๐ด(if(0 โค -๐ถ, -๐ถ, 0) ยท ๐ต) d๐ฅ) = (๐ถ ยท โซ๐ด๐ต d๐ฅ)) |
92 | 20, 29, 91 | 3eqtrrd 2778 |
1
โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด(๐ถ ยท ๐ต) d๐ฅ) |