Step |
Hyp |
Ref |
Expression |
1 |
|
itgcnval.1 |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ๐ต โ ๐ ) |
2 |
|
itgcnval.2 |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ ๐ต ) โ ๐ฟ1 ) |
3 |
|
iblmbf |
โข ( ( ๐ฅ โ ๐ด โฆ ๐ต ) โ ๐ฟ1 โ ( ๐ฅ โ ๐ด โฆ ๐ต ) โ MblFn ) |
4 |
2 3
|
syl |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ ๐ต ) โ MblFn ) |
5 |
4 1
|
mbfmptcl |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ๐ต โ โ ) |
6 |
5
|
recld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ ๐ต ) โ โ ) |
7 |
5
|
iblcn |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ ๐ต ) โ ๐ฟ1 โ ( ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 ) ) ) |
8 |
2 7
|
mpbid |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 ) ) |
9 |
8
|
simpld |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 ) |
10 |
6 9
|
itgcl |
โข ( ๐ โ โซ ๐ด ( โ โ ๐ต ) d ๐ฅ โ โ ) |
11 |
|
ax-icn |
โข i โ โ |
12 |
5
|
imcld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ ๐ต ) โ โ ) |
13 |
8
|
simprd |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 ) |
14 |
12 13
|
itgcl |
โข ( ๐ โ โซ ๐ด ( โ โ ๐ต ) d ๐ฅ โ โ ) |
15 |
|
mulcl |
โข ( ( i โ โ โง โซ ๐ด ( โ โ ๐ต ) d ๐ฅ โ โ ) โ ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) โ โ ) |
16 |
11 14 15
|
sylancr |
โข ( ๐ โ ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) โ โ ) |
17 |
10 16
|
negdid |
โข ( ๐ โ - ( โซ ๐ด ( โ โ ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) = ( - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ + - ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) ) |
18 |
|
0re |
โข 0 โ โ |
19 |
|
ifcl |
โข ( ( ( โ โ ๐ต ) โ โ โง 0 โ โ ) โ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) โ โ ) |
20 |
6 18 19
|
sylancl |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) โ โ ) |
21 |
6
|
iblre |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 โ ( ( ๐ฅ โ ๐ด โฆ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) ) ) |
22 |
9 21
|
mpbid |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) ) |
23 |
22
|
simpld |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) |
24 |
20 23
|
itgcl |
โข ( ๐ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โ ) |
25 |
6
|
renegcld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ( โ โ ๐ต ) โ โ ) |
26 |
|
ifcl |
โข ( ( - ( โ โ ๐ต ) โ โ โง 0 โ โ ) โ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) โ โ ) |
27 |
25 18 26
|
sylancl |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) โ โ ) |
28 |
22
|
simprd |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) |
29 |
27 28
|
itgcl |
โข ( ๐ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โ ) |
30 |
24 29
|
negsubdi2d |
โข ( ๐ โ - ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) = ( โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
31 |
6 9
|
itgreval |
โข ( ๐ โ โซ ๐ด ( โ โ ๐ต ) d ๐ฅ = ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
32 |
31
|
negeqd |
โข ( ๐ โ - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ = - ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
33 |
5
|
negcld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ๐ต โ โ ) |
34 |
33
|
recld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ - ๐ต ) โ โ ) |
35 |
1 2
|
iblneg |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ - ๐ต ) โ ๐ฟ1 ) |
36 |
33
|
iblcn |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ - ๐ต ) โ ๐ฟ1 โ ( ( ๐ฅ โ ๐ด โฆ ( โ โ - ๐ต ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ ( โ โ - ๐ต ) ) โ ๐ฟ1 ) ) ) |
37 |
35 36
|
mpbid |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ ( โ โ - ๐ต ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ ( โ โ - ๐ต ) ) โ ๐ฟ1 ) ) |
38 |
37
|
simpld |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ ( โ โ - ๐ต ) ) โ ๐ฟ1 ) |
39 |
34 38
|
itgreval |
โข ( ๐ โ โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ = ( โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ ) ) |
40 |
5
|
renegd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ - ๐ต ) = - ( โ โ ๐ต ) ) |
41 |
40
|
breq2d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( 0 โค ( โ โ - ๐ต ) โ 0 โค - ( โ โ ๐ต ) ) ) |
42 |
41 40
|
ifbieq1d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) = if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) |
43 |
42
|
itgeq2dv |
โข ( ๐ โ โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ = โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) |
44 |
40
|
negeqd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ( โ โ - ๐ต ) = - - ( โ โ ๐ต ) ) |
45 |
6
|
recnd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ ๐ต ) โ โ ) |
46 |
45
|
negnegd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - - ( โ โ ๐ต ) = ( โ โ ๐ต ) ) |
47 |
44 46
|
eqtrd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ( โ โ - ๐ต ) = ( โ โ ๐ต ) ) |
48 |
47
|
breq2d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( 0 โค - ( โ โ - ๐ต ) โ 0 โค ( โ โ ๐ต ) ) ) |
49 |
48 47
|
ifbieq1d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) = if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) |
50 |
49
|
itgeq2dv |
โข ( ๐ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ = โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) |
51 |
43 50
|
oveq12d |
โข ( ๐ โ ( โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ ) = ( โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
52 |
39 51
|
eqtrd |
โข ( ๐ โ โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ = ( โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
53 |
30 32 52
|
3eqtr4d |
โข ( ๐ โ - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ = โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) |
54 |
|
mulneg2 |
โข ( ( i โ โ โง โซ ๐ด ( โ โ ๐ต ) d ๐ฅ โ โ ) โ ( i ยท - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) = - ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) |
55 |
11 14 54
|
sylancr |
โข ( ๐ โ ( i ยท - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) = - ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) |
56 |
|
ifcl |
โข ( ( ( โ โ ๐ต ) โ โ โง 0 โ โ ) โ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) โ โ ) |
57 |
12 18 56
|
sylancl |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) โ โ ) |
58 |
12
|
iblre |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ ( โ โ ๐ต ) ) โ ๐ฟ1 โ ( ( ๐ฅ โ ๐ด โฆ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) ) ) |
59 |
13 58
|
mpbid |
โข ( ๐ โ ( ( ๐ฅ โ ๐ด โฆ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 โง ( ๐ฅ โ ๐ด โฆ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) ) |
60 |
59
|
simpld |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) |
61 |
57 60
|
itgcl |
โข ( ๐ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โ ) |
62 |
12
|
renegcld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ( โ โ ๐ต ) โ โ ) |
63 |
|
ifcl |
โข ( ( - ( โ โ ๐ต ) โ โ โง 0 โ โ ) โ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) โ โ ) |
64 |
62 18 63
|
sylancl |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) โ โ ) |
65 |
59
|
simprd |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) โ ๐ฟ1 ) |
66 |
64 65
|
itgcl |
โข ( ๐ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โ ) |
67 |
61 66
|
negsubdi2d |
โข ( ๐ โ - ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) = ( โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
68 |
5
|
imnegd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ - ๐ต ) = - ( โ โ ๐ต ) ) |
69 |
68
|
breq2d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( 0 โค ( โ โ - ๐ต ) โ 0 โค - ( โ โ ๐ต ) ) ) |
70 |
69 68
|
ifbieq1d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) = if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) ) |
71 |
70
|
itgeq2dv |
โข ( ๐ โ โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ = โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) |
72 |
68
|
negeqd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ( โ โ - ๐ต ) = - - ( โ โ ๐ต ) ) |
73 |
12
|
recnd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ ๐ต ) โ โ ) |
74 |
73
|
negnegd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - - ( โ โ ๐ต ) = ( โ โ ๐ต ) ) |
75 |
72 74
|
eqtrd |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ - ( โ โ - ๐ต ) = ( โ โ ๐ต ) ) |
76 |
75
|
breq2d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( 0 โค - ( โ โ - ๐ต ) โ 0 โค ( โ โ ๐ต ) ) ) |
77 |
76 75
|
ifbieq1d |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) = if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) ) |
78 |
77
|
itgeq2dv |
โข ( ๐ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ = โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) |
79 |
71 78
|
oveq12d |
โข ( ๐ โ ( โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ ) = ( โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
80 |
67 79
|
eqtr4d |
โข ( ๐ โ - ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) = ( โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ ) ) |
81 |
12 13
|
itgreval |
โข ( ๐ โ โซ ๐ด ( โ โ ๐ต ) d ๐ฅ = ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
82 |
81
|
negeqd |
โข ( ๐ โ - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ = - ( โซ ๐ด if ( 0 โค ( โ โ ๐ต ) , ( โ โ ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ ๐ต ) , - ( โ โ ๐ต ) , 0 ) d ๐ฅ ) ) |
83 |
33
|
imcld |
โข ( ( ๐ โง ๐ฅ โ ๐ด ) โ ( โ โ - ๐ต ) โ โ ) |
84 |
37
|
simprd |
โข ( ๐ โ ( ๐ฅ โ ๐ด โฆ ( โ โ - ๐ต ) ) โ ๐ฟ1 ) |
85 |
83 84
|
itgreval |
โข ( ๐ โ โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ = ( โซ ๐ด if ( 0 โค ( โ โ - ๐ต ) , ( โ โ - ๐ต ) , 0 ) d ๐ฅ โ โซ ๐ด if ( 0 โค - ( โ โ - ๐ต ) , - ( โ โ - ๐ต ) , 0 ) d ๐ฅ ) ) |
86 |
80 82 85
|
3eqtr4d |
โข ( ๐ โ - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ = โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) |
87 |
86
|
oveq2d |
โข ( ๐ โ ( i ยท - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) = ( i ยท โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) ) |
88 |
55 87
|
eqtr3d |
โข ( ๐ โ - ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) = ( i ยท โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) ) |
89 |
53 88
|
oveq12d |
โข ( ๐ โ ( - โซ ๐ด ( โ โ ๐ต ) d ๐ฅ + - ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) = ( โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) ) ) |
90 |
17 89
|
eqtrd |
โข ( ๐ โ - ( โซ ๐ด ( โ โ ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) = ( โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) ) ) |
91 |
1 2
|
itgcnval |
โข ( ๐ โ โซ ๐ด ๐ต d ๐ฅ = ( โซ ๐ด ( โ โ ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) ) |
92 |
91
|
negeqd |
โข ( ๐ โ - โซ ๐ด ๐ต d ๐ฅ = - ( โซ ๐ด ( โ โ ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ ๐ต ) d ๐ฅ ) ) ) |
93 |
33 35
|
itgcnval |
โข ( ๐ โ โซ ๐ด - ๐ต d ๐ฅ = ( โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ + ( i ยท โซ ๐ด ( โ โ - ๐ต ) d ๐ฅ ) ) ) |
94 |
90 92 93
|
3eqtr4d |
โข ( ๐ โ - โซ ๐ด ๐ต d ๐ฅ = โซ ๐ด - ๐ต d ๐ฅ ) |