Step | Hyp | Ref
| Expression |
1 | | itgmulc2.1 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
2 | 1 | recld 15085 |
. . . . . . . 8
โข (๐ โ (โโ๐ถ) โ
โ) |
3 | 2 | recnd 11188 |
. . . . . . 7
โข (๐ โ (โโ๐ถ) โ
โ) |
4 | 3 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ถ) โ โ) |
5 | | itgmulc2.3 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
6 | | iblmbf 25148 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
8 | | itgmulc2.2 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
9 | 7, 8 | mbfmptcl 25016 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
10 | 9 | recld 15085 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
11 | 10 | recnd 11188 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
12 | 4, 11 | mulcld 11180 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ ((โโ๐ถ) ยท (โโ๐ต)) โ โ) |
13 | 9 | iblcn 25179 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
14 | 5, 13 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
15 | 14 | simpld 496 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
16 | 3, 10, 15 | iblmulc2 25211 |
. . . . 5
โข (๐ โ (๐ฅ โ ๐ด โฆ ((โโ๐ถ) ยท (โโ๐ต))) โ
๐ฟ1) |
17 | 12, 16 | itgcl 25164 |
. . . 4
โข (๐ โ โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ โ โ) |
18 | | ax-icn 11115 |
. . . . 5
โข i โ
โ |
19 | 9 | imcld 15086 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
20 | 19 | recnd 11188 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
21 | 4, 20 | mulcld 11180 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ ((โโ๐ถ) ยท (โโ๐ต)) โ โ) |
22 | 14 | simprd 497 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
23 | 3, 19, 22 | iblmulc2 25211 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ ((โโ๐ถ) ยท (โโ๐ต))) โ
๐ฟ1) |
24 | 21, 23 | itgcl 25164 |
. . . . 5
โข (๐ โ โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ โ โ) |
25 | | mulcl 11140 |
. . . . 5
โข ((i
โ โ โง โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ โ โ) โ (i ยท
โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) โ โ) |
26 | 18, 24, 25 | sylancr 588 |
. . . 4
โข (๐ โ (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) โ โ) |
27 | 1 | imcld 15086 |
. . . . . . . . 9
โข (๐ โ (โโ๐ถ) โ
โ) |
28 | 27 | renegcld 11587 |
. . . . . . . 8
โข (๐ โ -(โโ๐ถ) โ
โ) |
29 | 28 | recnd 11188 |
. . . . . . 7
โข (๐ โ -(โโ๐ถ) โ
โ) |
30 | 29 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ถ) โ โ) |
31 | 30, 20 | mulcld 11180 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ (-(โโ๐ถ) ยท (โโ๐ต)) โ โ) |
32 | 29, 19, 22 | iblmulc2 25211 |
. . . . 5
โข (๐ โ (๐ฅ โ ๐ด โฆ (-(โโ๐ถ) ยท (โโ๐ต))) โ
๐ฟ1) |
33 | 31, 32 | itgcl 25164 |
. . . 4
โข (๐ โ โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ โ โ) |
34 | 27 | recnd 11188 |
. . . . . . . 8
โข (๐ โ (โโ๐ถ) โ
โ) |
35 | 34 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ถ) โ โ) |
36 | 35, 11 | mulcld 11180 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ ((โโ๐ถ) ยท (โโ๐ต)) โ โ) |
37 | 34, 10, 15 | iblmulc2 25211 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ ((โโ๐ถ) ยท (โโ๐ต))) โ
๐ฟ1) |
38 | 36, 37 | itgcl 25164 |
. . . . 5
โข (๐ โ โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ โ โ) |
39 | | mulcl 11140 |
. . . . 5
โข ((i
โ โ โง โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ โ โ) โ (i ยท
โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) โ โ) |
40 | 18, 38, 39 | sylancr 588 |
. . . 4
โข (๐ โ (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) โ โ) |
41 | 17, 26, 33, 40 | add4d 11388 |
. . 3
โข (๐ โ ((โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) + (โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) = ((โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + ((i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)))) |
42 | 8, 5 | itgcl 25164 |
. . . 4
โข (๐ โ โซ๐ด๐ต d๐ฅ โ โ) |
43 | | mulcl 11140 |
. . . . 5
โข ((i
โ โ โง (โโ๐ถ) โ โ) โ (i ยท
(โโ๐ถ)) โ
โ) |
44 | 18, 34, 43 | sylancr 588 |
. . . 4
โข (๐ โ (i ยท
(โโ๐ถ)) โ
โ) |
45 | 8, 5 | itgcnval 25180 |
. . . . . . 7
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
46 | 45 | oveq2d 7374 |
. . . . . 6
โข (๐ โ ((โโ๐ถ) ยท โซ๐ด๐ต d๐ฅ) = ((โโ๐ถ) ยท (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)))) |
47 | 10, 15 | itgcl 25164 |
. . . . . . 7
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
48 | 19, 22 | itgcl 25164 |
. . . . . . . 8
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
49 | | mulcl 11140 |
. . . . . . . 8
โข ((i
โ โ โง โซ๐ด(โโ๐ต) d๐ฅ โ โ) โ (i ยท
โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
50 | 18, 48, 49 | sylancr 588 |
. . . . . . 7
โข (๐ โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
51 | 3, 47, 50 | adddid 11184 |
. . . . . 6
โข (๐ โ ((โโ๐ถ) ยท (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) = (((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) + ((โโ๐ถ) ยท (i ยท โซ๐ด(โโ๐ต) d๐ฅ)))) |
52 | 3, 10, 15, 2, 10 | itgmulc2lem2 25213 |
. . . . . . 7
โข (๐ โ ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) = โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) |
53 | 18 | a1i 11 |
. . . . . . . . 9
โข (๐ โ i โ
โ) |
54 | 3, 53, 48 | mul12d 11369 |
. . . . . . . 8
โข (๐ โ ((โโ๐ถ) ยท (i ยท
โซ๐ด(โโ๐ต) d๐ฅ)) = (i ยท ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
55 | 3, 19, 22, 2, 19 | itgmulc2lem2 25213 |
. . . . . . . . 9
โข (๐ โ ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) = โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) |
56 | 55 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ (i ยท
((โโ๐ถ) ยท
โซ๐ด(โโ๐ต) d๐ฅ)) = (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
57 | 54, 56 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((โโ๐ถ) ยท (i ยท
โซ๐ด(โโ๐ต) d๐ฅ)) = (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
58 | 52, 57 | oveq12d 7376 |
. . . . . 6
โข (๐ โ (((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) + ((โโ๐ถ) ยท (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) = (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
59 | 46, 51, 58 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ ((โโ๐ถ) ยท โซ๐ด๐ต d๐ฅ) = (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
60 | 45 | oveq2d 7374 |
. . . . . 6
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
โซ๐ด๐ต d๐ฅ) = ((i ยท (โโ๐ถ)) ยท (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)))) |
61 | 44, 47, 50 | adddid 11184 |
. . . . . 6
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
(โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) = (((i ยท (โโ๐ถ)) ยท โซ๐ด(โโ๐ต) d๐ฅ) + ((i ยท (โโ๐ถ)) ยท (i ยท
โซ๐ด(โโ๐ต) d๐ฅ)))) |
62 | 53, 34, 47 | mulassd 11183 |
. . . . . . . . 9
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
โซ๐ด(โโ๐ต) d๐ฅ) = (i ยท ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
63 | 34, 10, 15, 27, 10 | itgmulc2lem2 25213 |
. . . . . . . . . 10
โข (๐ โ ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) = โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) |
64 | 63 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ (i ยท
((โโ๐ถ) ยท
โซ๐ด(โโ๐ต) d๐ฅ)) = (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
65 | 62, 64 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
โซ๐ด(โโ๐ต) d๐ฅ) = (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
66 | 53, 34, 53, 48 | mul4d 11372 |
. . . . . . . . 9
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
(i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = ((i ยท i) ยท
((โโ๐ถ) ยท
โซ๐ด(โโ๐ต) d๐ฅ))) |
67 | | ixi 11789 |
. . . . . . . . . . 11
โข (i
ยท i) = -1 |
68 | 67 | oveq1i 7368 |
. . . . . . . . . 10
โข ((i
ยท i) ยท ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (-1 ยท ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ)) |
69 | 34, 48 | mulcld 11180 |
. . . . . . . . . . 11
โข (๐ โ ((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
70 | 69 | mulm1d 11612 |
. . . . . . . . . 10
โข (๐ โ (-1 ยท
((โโ๐ถ) ยท
โซ๐ด(โโ๐ต) d๐ฅ)) = -((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ)) |
71 | 68, 70 | eqtrid 2785 |
. . . . . . . . 9
โข (๐ โ ((i ยท i) ยท
((โโ๐ถ) ยท
โซ๐ด(โโ๐ต) d๐ฅ)) = -((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ)) |
72 | 34, 48 | mulneg1d 11613 |
. . . . . . . . . 10
โข (๐ โ (-(โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) = -((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ)) |
73 | 29, 19, 22, 28, 19 | itgmulc2lem2 25213 |
. . . . . . . . . 10
โข (๐ โ (-(โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) = โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) |
74 | 72, 73 | eqtr3d 2775 |
. . . . . . . . 9
โข (๐ โ -((โโ๐ถ) ยท โซ๐ด(โโ๐ต) d๐ฅ) = โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) |
75 | 66, 71, 74 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
(i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) |
76 | 65, 75 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ (((i ยท
(โโ๐ถ)) ยท
โซ๐ด(โโ๐ต) d๐ฅ) + ((i ยท (โโ๐ถ)) ยท (i ยท
โซ๐ด(โโ๐ต) d๐ฅ))) = ((i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
77 | 40, 33, 76 | comraddd 11374 |
. . . . . 6
โข (๐ โ (((i ยท
(โโ๐ถ)) ยท
โซ๐ด(โโ๐ต) d๐ฅ) + ((i ยท (โโ๐ถ)) ยท (i ยท
โซ๐ด(โโ๐ต) d๐ฅ))) = (โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
78 | 60, 61, 77 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ ((i ยท
(โโ๐ถ)) ยท
โซ๐ด๐ต d๐ฅ) = (โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
79 | 59, 78 | oveq12d 7376 |
. . . 4
โข (๐ โ (((โโ๐ถ) ยท โซ๐ด๐ต d๐ฅ) + ((i ยท (โโ๐ถ)) ยท โซ๐ด๐ต d๐ฅ)) = ((โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) + (โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)))) |
80 | 3, 42, 44, 79 | joinlmuladdmuld 11187 |
. . 3
โข (๐ โ (((โโ๐ถ) + (i ยท
(โโ๐ถ)))
ยท โซ๐ด๐ต d๐ฅ) = ((โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) + (โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)))) |
81 | 35, 20 | mulcld 11180 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ((โโ๐ถ) ยท (โโ๐ต)) โ โ) |
82 | 12, 81 | negsubd 11523 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (((โโ๐ถ) ยท (โโ๐ต)) + -((โโ๐ถ) ยท (โโ๐ต))) = (((โโ๐ถ) ยท (โโ๐ต)) โ ((โโ๐ถ) ยท (โโ๐ต)))) |
83 | 35, 20 | mulneg1d 11613 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (-(โโ๐ถ) ยท (โโ๐ต)) = -((โโ๐ถ) ยท (โโ๐ต))) |
84 | 83 | oveq2d 7374 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (((โโ๐ถ) ยท (โโ๐ต)) + (-(โโ๐ถ) ยท (โโ๐ต))) = (((โโ๐ถ) ยท (โโ๐ต)) + -((โโ๐ถ) ยท (โโ๐ต)))) |
85 | 1 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
86 | 85, 9 | remuld 15109 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ถ ยท ๐ต)) = (((โโ๐ถ) ยท (โโ๐ต)) โ ((โโ๐ถ) ยท (โโ๐ต)))) |
87 | 82, 84, 86 | 3eqtr4d 2783 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (((โโ๐ถ) ยท (โโ๐ต)) + (-(โโ๐ถ) ยท (โโ๐ต))) = (โโ(๐ถ ยท ๐ต))) |
88 | 87 | itgeq2dv 25162 |
. . . . 5
โข (๐ โ โซ๐ด(((โโ๐ถ) ยท (โโ๐ต)) + (-(โโ๐ถ) ยท (โโ๐ต))) d๐ฅ = โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ) |
89 | 12, 16, 31, 32 | itgadd 25205 |
. . . . 5
โข (๐ โ โซ๐ด(((โโ๐ถ) ยท (โโ๐ต)) + (-(โโ๐ถ) ยท (โโ๐ต))) d๐ฅ = (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
90 | 88, 89 | eqtr3d 2775 |
. . . 4
โข (๐ โ โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ = (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
91 | 85, 9 | immuld 15110 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ถ ยท ๐ต)) = (((โโ๐ถ) ยท (โโ๐ต)) + ((โโ๐ถ) ยท (โโ๐ต)))) |
92 | 91 | itgeq2dv 25162 |
. . . . . . 7
โข (๐ โ โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ = โซ๐ด(((โโ๐ถ) ยท (โโ๐ต)) + ((โโ๐ถ) ยท (โโ๐ต))) d๐ฅ) |
93 | 21, 23, 36, 37 | itgadd 25205 |
. . . . . . 7
โข (๐ โ โซ๐ด(((โโ๐ถ) ยท (โโ๐ต)) + ((โโ๐ถ) ยท (โโ๐ต))) d๐ฅ = (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
94 | 92, 93 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ = (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) |
95 | 94 | oveq2d 7374 |
. . . . 5
โข (๐ โ (i ยท โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ) = (i ยท (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
96 | 53, 24, 38 | adddid 11184 |
. . . . 5
โข (๐ โ (i ยท (โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)) = ((i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
97 | 95, 96 | eqtrd 2773 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ) = ((i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ))) |
98 | 90, 97 | oveq12d 7376 |
. . 3
โข (๐ โ (โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ)) = ((โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ + โซ๐ด(-(โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + ((i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ) + (i ยท โซ๐ด((โโ๐ถ) ยท (โโ๐ต)) d๐ฅ)))) |
99 | 41, 80, 98 | 3eqtr4d 2783 |
. 2
โข (๐ โ (((โโ๐ถ) + (i ยท
(โโ๐ถ)))
ยท โซ๐ด๐ต d๐ฅ) = (โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ))) |
100 | 1 | replimd 15088 |
. . 3
โข (๐ โ ๐ถ = ((โโ๐ถ) + (i ยท (โโ๐ถ)))) |
101 | 100 | oveq1d 7373 |
. 2
โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = (((โโ๐ถ) + (i ยท (โโ๐ถ))) ยท โซ๐ด๐ต d๐ฅ)) |
102 | 85, 9 | mulcld 11180 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) โ โ) |
103 | 1, 8, 5 | iblmulc2 25211 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ
๐ฟ1) |
104 | 102, 103 | itgcnval 25180 |
. 2
โข (๐ โ โซ๐ด(๐ถ ยท ๐ต) d๐ฅ = (โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ถ ยท ๐ต)) d๐ฅ))) |
105 | 99, 101, 104 | 3eqtr4d 2783 |
1
โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด(๐ถ ยท ๐ต) d๐ฅ) |