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 𝑥 )