Metamath Proof Explorer


Theorem itgneg

Description: Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ ๐‘‰ )
itgcnval.2 โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ต ) โˆˆ ๐ฟ1 )
Assertion itgneg ( ๐œ‘ โ†’ - โˆซ ๐ด ๐ต d ๐‘ฅ = โˆซ ๐ด - ๐ต d ๐‘ฅ )

Proof

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 ๐‘ฅ )