Metamath Proof Explorer

Theorem itgneg

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

Ref Expression
Hypotheses itgcnval.1 ⊢φ∧x∈A→B∈V
itgcnval.2 ⊢φ→x∈A⟼B∈𝐿1
Assertion itgneg ⊢φ→−∫ABdx=∫A−Bdx

Proof

Step Hyp Ref Expression
1 itgcnval.1 ⊢φ∧x∈A→B∈V
2 itgcnval.2 ⊢φ→x∈A⟼B∈𝐿1
3 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
4 2 3 syl ⊢φ→x∈A⟼B∈MblFn
5 4 1 mbfmptcl ⊢φ∧x∈A→B∈ℂ
6 5 recld ⊢φ∧x∈A→ℜ⁡B∈ℝ
7 5 iblcn ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
8 2 7 mpbid ⊢φ→x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
9 8 simpld ⊢φ→x∈A⟼ℜ⁡B∈𝐿1
10 6 9 itgcl ⊢φ→∫Aℜ⁡Bdx∈ℂ
11 ax-icn ⊢i∈ℂ
12 5 imcld ⊢φ∧x∈A→ℑ⁡B∈ℝ
13 8 simprd ⊢φ→x∈A⟼ℑ⁡B∈𝐿1
14 12 13 itgcl ⊢φ→∫Aℑ⁡Bdx∈ℂ
15 mulcl ⊢i∈ℂ∧∫Aℑ⁡Bdx∈ℂ→i⁢∫Aℑ⁡Bdx∈ℂ
16 11 14 15 sylancr ⊢φ→i⁢∫Aℑ⁡Bdx∈ℂ
17 10 16 negdid ⊢φ→−∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=-∫Aℜ⁡Bdx+−i⁢∫Aℑ⁡Bdx
18 0re ⊢0∈ℝ
19 ifcl ⊢ℜ⁡B∈ℝ∧0∈ℝ→if0≤ℜ⁡Bℜ⁡B0∈ℝ
20 6 18 19 sylancl ⊢φ∧x∈A→if0≤ℜ⁡Bℜ⁡B0∈ℝ
21 6 iblre ⊢φ→x∈A⟼ℜ⁡B∈𝐿1↔x∈A⟼if0≤ℜ⁡Bℜ⁡B0∈𝐿1∧x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0∈𝐿1
22 9 21 mpbid ⊢φ→x∈A⟼if0≤ℜ⁡Bℜ⁡B0∈𝐿1∧x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0∈𝐿1
23 22 simpld ⊢φ→x∈A⟼if0≤ℜ⁡Bℜ⁡B0∈𝐿1
24 20 23 itgcl ⊢φ→∫Aif0≤ℜ⁡Bℜ⁡B0dx∈ℂ
25 6 renegcld ⊢φ∧x∈A→−ℜ⁡B∈ℝ
26 ifcl ⊢−ℜ⁡B∈ℝ∧0∈ℝ→if0≤−ℜ⁡B−ℜ⁡B0∈ℝ
27 25 18 26 sylancl ⊢φ∧x∈A→if0≤−ℜ⁡B−ℜ⁡B0∈ℝ
28 22 simprd ⊢φ→x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0∈𝐿1
29 27 28 itgcl ⊢φ→∫Aif0≤−ℜ⁡B−ℜ⁡B0dx∈ℂ
30 24 29 negsubdi2d ⊢φ→−∫Aif0≤ℜ⁡Bℜ⁡B0dx−∫Aif0≤−ℜ⁡B−ℜ⁡B0dx=∫Aif0≤−ℜ⁡B−ℜ⁡B0dx−∫Aif0≤ℜ⁡Bℜ⁡B0dx
31 6 9 itgreval ⊢φ→∫Aℜ⁡Bdx=∫Aif0≤ℜ⁡Bℜ⁡B0dx−∫Aif0≤−ℜ⁡B−ℜ⁡B0dx
32 31 negeqd ⊢φ→−∫Aℜ⁡Bdx=−∫Aif0≤ℜ⁡Bℜ⁡B0dx−∫Aif0≤−ℜ⁡B−ℜ⁡B0dx
33 5 negcld ⊢φ∧x∈A→−B∈ℂ
34 33 recld ⊢φ∧x∈A→ℜ⁡−B∈ℝ
35 1 2 iblneg ⊢φ→x∈A⟼−B∈𝐿1
36 33 iblcn ⊢φ→x∈A⟼−B∈𝐿1↔x∈A⟼ℜ⁡−B∈𝐿1∧x∈A⟼ℑ⁡−B∈𝐿1
37 35 36 mpbid ⊢φ→x∈A⟼ℜ⁡−B∈𝐿1∧x∈A⟼ℑ⁡−B∈𝐿1
38 37 simpld ⊢φ→x∈A⟼ℜ⁡−B∈𝐿1
39 34 38 itgreval ⊢φ→∫Aℜ⁡−Bdx=∫Aif0≤ℜ⁡−Bℜ⁡−B0dx−∫Aif0≤−ℜ⁡−B−ℜ⁡−B0dx
40 5 renegd ⊢φ∧x∈A→ℜ⁡−B=−ℜ⁡B
41 40 breq2d ⊢φ∧x∈A→0≤ℜ⁡−B↔0≤−ℜ⁡B
42 41 40 ifbieq1d ⊢φ∧x∈A→if0≤ℜ⁡−Bℜ⁡−B0=if0≤−ℜ⁡B−ℜ⁡B0
43 42 itgeq2dv ⊢φ→∫Aif0≤ℜ⁡−Bℜ⁡−B0dx=∫Aif0≤−ℜ⁡B−ℜ⁡B0dx
44 40 negeqd ⊢φ∧x∈A→−ℜ⁡−B=−−ℜ⁡B
45 6 recnd ⊢φ∧x∈A→ℜ⁡B∈ℂ
46 45 negnegd ⊢φ∧x∈A→−−ℜ⁡B=ℜ⁡B
47 44 46 eqtrd ⊢φ∧x∈A→−ℜ⁡−B=ℜ⁡B
48 47 breq2d ⊢φ∧x∈A→0≤−ℜ⁡−B↔0≤ℜ⁡B
49 48 47 ifbieq1d ⊢φ∧x∈A→if0≤−ℜ⁡−B−ℜ⁡−B0=if0≤ℜ⁡Bℜ⁡B0
50 49 itgeq2dv ⊢φ→∫Aif0≤−ℜ⁡−B−ℜ⁡−B0dx=∫Aif0≤ℜ⁡Bℜ⁡B0dx
51 43 50 oveq12d ⊢φ→∫Aif0≤ℜ⁡−Bℜ⁡−B0dx−∫Aif0≤−ℜ⁡−B−ℜ⁡−B0dx=∫Aif0≤−ℜ⁡B−ℜ⁡B0dx−∫Aif0≤ℜ⁡Bℜ⁡B0dx
52 39 51 eqtrd ⊢φ→∫Aℜ⁡−Bdx=∫Aif0≤−ℜ⁡B−ℜ⁡B0dx−∫Aif0≤ℜ⁡Bℜ⁡B0dx
53 30 32 52 3eqtr4d ⊢φ→−∫Aℜ⁡Bdx=∫Aℜ⁡−Bdx
54 mulneg2 ⊢i∈ℂ∧∫Aℑ⁡Bdx∈ℂ→i⁢−∫Aℑ⁡Bdx=−i⁢∫Aℑ⁡Bdx
55 11 14 54 sylancr ⊢φ→i⁢−∫Aℑ⁡Bdx=−i⁢∫Aℑ⁡Bdx
56 ifcl ⊢ℑ⁡B∈ℝ∧0∈ℝ→if0≤ℑ⁡Bℑ⁡B0∈ℝ
57 12 18 56 sylancl ⊢φ∧x∈A→if0≤ℑ⁡Bℑ⁡B0∈ℝ
58 12 iblre ⊢φ→x∈A⟼ℑ⁡B∈𝐿1↔x∈A⟼if0≤ℑ⁡Bℑ⁡B0∈𝐿1∧x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0∈𝐿1
59 13 58 mpbid ⊢φ→x∈A⟼if0≤ℑ⁡Bℑ⁡B0∈𝐿1∧x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0∈𝐿1
60 59 simpld ⊢φ→x∈A⟼if0≤ℑ⁡Bℑ⁡B0∈𝐿1
61 57 60 itgcl ⊢φ→∫Aif0≤ℑ⁡Bℑ⁡B0dx∈ℂ
62 12 renegcld ⊢φ∧x∈A→−ℑ⁡B∈ℝ
63 ifcl ⊢−ℑ⁡B∈ℝ∧0∈ℝ→if0≤−ℑ⁡B−ℑ⁡B0∈ℝ
64 62 18 63 sylancl ⊢φ∧x∈A→if0≤−ℑ⁡B−ℑ⁡B0∈ℝ
65 59 simprd ⊢φ→x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0∈𝐿1
66 64 65 itgcl ⊢φ→∫Aif0≤−ℑ⁡B−ℑ⁡B0dx∈ℂ
67 61 66 negsubdi2d ⊢φ→−∫Aif0≤ℑ⁡Bℑ⁡B0dx−∫Aif0≤−ℑ⁡B−ℑ⁡B0dx=∫Aif0≤−ℑ⁡B−ℑ⁡B0dx−∫Aif0≤ℑ⁡Bℑ⁡B0dx
68 5 imnegd ⊢φ∧x∈A→ℑ⁡−B=−ℑ⁡B
69 68 breq2d ⊢φ∧x∈A→0≤ℑ⁡−B↔0≤−ℑ⁡B
70 69 68 ifbieq1d ⊢φ∧x∈A→if0≤ℑ⁡−Bℑ⁡−B0=if0≤−ℑ⁡B−ℑ⁡B0
71 70 itgeq2dv ⊢φ→∫Aif0≤ℑ⁡−Bℑ⁡−B0dx=∫Aif0≤−ℑ⁡B−ℑ⁡B0dx
72 68 negeqd ⊢φ∧x∈A→−ℑ⁡−B=−−ℑ⁡B
73 12 recnd ⊢φ∧x∈A→ℑ⁡B∈ℂ
74 73 negnegd ⊢φ∧x∈A→−−ℑ⁡B=ℑ⁡B
75 72 74 eqtrd ⊢φ∧x∈A→−ℑ⁡−B=ℑ⁡B
76 75 breq2d ⊢φ∧x∈A→0≤−ℑ⁡−B↔0≤ℑ⁡B
77 76 75 ifbieq1d ⊢φ∧x∈A→if0≤−ℑ⁡−B−ℑ⁡−B0=if0≤ℑ⁡Bℑ⁡B0
78 77 itgeq2dv ⊢φ→∫Aif0≤−ℑ⁡−B−ℑ⁡−B0dx=∫Aif0≤ℑ⁡Bℑ⁡B0dx
79 71 78 oveq12d ⊢φ→∫Aif0≤ℑ⁡−Bℑ⁡−B0dx−∫Aif0≤−ℑ⁡−B−ℑ⁡−B0dx=∫Aif0≤−ℑ⁡B−ℑ⁡B0dx−∫Aif0≤ℑ⁡Bℑ⁡B0dx
80 67 79 eqtr4d ⊢φ→−∫Aif0≤ℑ⁡Bℑ⁡B0dx−∫Aif0≤−ℑ⁡B−ℑ⁡B0dx=∫Aif0≤ℑ⁡−Bℑ⁡−B0dx−∫Aif0≤−ℑ⁡−B−ℑ⁡−B0dx
81 12 13 itgreval ⊢φ→∫Aℑ⁡Bdx=∫Aif0≤ℑ⁡Bℑ⁡B0dx−∫Aif0≤−ℑ⁡B−ℑ⁡B0dx
82 81 negeqd ⊢φ→−∫Aℑ⁡Bdx=−∫Aif0≤ℑ⁡Bℑ⁡B0dx−∫Aif0≤−ℑ⁡B−ℑ⁡B0dx
83 33 imcld ⊢φ∧x∈A→ℑ⁡−B∈ℝ
84 37 simprd ⊢φ→x∈A⟼ℑ⁡−B∈𝐿1
85 83 84 itgreval ⊢φ→∫Aℑ⁡−Bdx=∫Aif0≤ℑ⁡−Bℑ⁡−B0dx−∫Aif0≤−ℑ⁡−B−ℑ⁡−B0dx
86 80 82 85 3eqtr4d ⊢φ→−∫Aℑ⁡Bdx=∫Aℑ⁡−Bdx
87 86 oveq2d ⊢φ→i⁢−∫Aℑ⁡Bdx=i⁢∫Aℑ⁡−Bdx
88 55 87 eqtr3d ⊢φ→−i⁢∫Aℑ⁡Bdx=i⁢∫Aℑ⁡−Bdx
89 53 88 oveq12d ⊢φ→-∫Aℜ⁡Bdx+−i⁢∫Aℑ⁡Bdx=∫Aℜ⁡−Bdx+i⁢∫Aℑ⁡−Bdx
90 17 89 eqtrd ⊢φ→−∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=∫Aℜ⁡−Bdx+i⁢∫Aℑ⁡−Bdx
91 1 2 itgcnval ⊢φ→∫ABdx=∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx
92 91 negeqd ⊢φ→−∫ABdx=−∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx
93 33 35 itgcnval ⊢φ→∫A−Bdx=∫Aℜ⁡−Bdx+i⁢∫Aℑ⁡−Bdx
94 90 92 93 3eqtr4d ⊢φ→−∫ABdx=∫A−Bdx