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 ⊢ φ → − ∫ A B dx = ∫ A − B dx

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 ℜ ⁡ B dx ∈ ℂ
11 ax-icn ⊢ i ∈ ℂ
12 5 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
13 8 simprd ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
14 12 13 itgcl ⊢ φ → ∫ A ℑ ⁡ B dx ∈ ℂ
15 mulcl ⊢ i ∈ ℂ ∧ ∫ A ℑ ⁡ B dx ∈ ℂ → i ⁢ ∫ A ℑ ⁡ B dx ∈ ℂ
16 11 14 15 sylancr ⊢ φ → i ⁢ ∫ A ℑ ⁡ B dx ∈ ℂ
17 10 16 negdid ⊢ φ → − ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx = - ∫ A ℜ ⁡ B dx + − i ⁢ ∫ A ℑ ⁡ B dx
18 0re ⊢ 0 ∈ ℝ
19 ifcl ⊢ ℜ ⁡ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ
20 6 18 19 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ ℝ
21 6 iblre ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ 𝐿 1
22 9 21 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ 𝐿 1
23 22 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 ∈ 𝐿 1
24 20 23 itgcl ⊢ φ → ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx ∈ ℂ
25 6 renegcld ⊢ φ ∧ x ∈ A → − ℜ ⁡ B ∈ ℝ
26 ifcl ⊢ − ℜ ⁡ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ
27 25 18 26 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ ℝ
28 22 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 ∈ 𝐿 1
29 27 28 itgcl ⊢ φ → ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx ∈ ℂ
30 24 29 negsubdi2d ⊢ φ → − ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx − ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx = ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx − ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx
31 6 9 itgreval ⊢ φ → ∫ A ℜ ⁡ B dx = ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx − ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx
32 31 negeqd ⊢ φ → − ∫ A ℜ ⁡ B dx = − ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx − ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx
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 ℜ ⁡ − B dx = ∫ A if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 dx − ∫ A if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 dx
40 5 renegd ⊢ φ ∧ x ∈ A → ℜ ⁡ − B = − ℜ ⁡ B
41 40 breq2d ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ − B ↔ 0 ≤ − ℜ ⁡ B
42 41 40 ifbieq1d ⊢ φ ∧ x ∈ A → if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 = if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
43 42 itgeq2dv ⊢ φ → ∫ A if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 dx = ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx
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 → if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 = if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
50 49 itgeq2dv ⊢ φ → ∫ A if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 dx = ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx
51 43 50 oveq12d ⊢ φ → ∫ A if 0 ≤ ℜ ⁡ − B ℜ ⁡ − B 0 dx − ∫ A if 0 ≤ − ℜ ⁡ − B − ℜ ⁡ − B 0 dx = ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx − ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx
52 39 51 eqtrd ⊢ φ → ∫ A ℜ ⁡ − B dx = ∫ A if 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 dx − ∫ A if 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 dx
53 30 32 52 3eqtr4d ⊢ φ → − ∫ A ℜ ⁡ B dx = ∫ A ℜ ⁡ − B dx
54 mulneg2 ⊢ i ∈ ℂ ∧ ∫ A ℑ ⁡ B dx ∈ ℂ → i ⁢ − ∫ A ℑ ⁡ B dx = − i ⁢ ∫ A ℑ ⁡ B dx
55 11 14 54 sylancr ⊢ φ → i ⁢ − ∫ A ℑ ⁡ B dx = − i ⁢ ∫ A ℑ ⁡ B dx
56 ifcl ⊢ ℑ ⁡ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ
57 12 18 56 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ ℝ
58 12 iblre ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ 𝐿 1
59 13 58 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ 𝐿 1
60 59 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 ∈ 𝐿 1
61 57 60 itgcl ⊢ φ → ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx ∈ ℂ
62 12 renegcld ⊢ φ ∧ x ∈ A → − ℑ ⁡ B ∈ ℝ
63 ifcl ⊢ − ℑ ⁡ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
64 62 18 63 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ ℝ
65 59 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 ∈ 𝐿 1
66 64 65 itgcl ⊢ φ → ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx ∈ ℂ
67 61 66 negsubdi2d ⊢ φ → − ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx = ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx − ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx
68 5 imnegd ⊢ φ ∧ x ∈ A → ℑ ⁡ − B = − ℑ ⁡ B
69 68 breq2d ⊢ φ ∧ x ∈ A → 0 ≤ ℑ ⁡ − B ↔ 0 ≤ − ℑ ⁡ B
70 69 68 ifbieq1d ⊢ φ ∧ x ∈ A → if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 = if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
71 70 itgeq2dv ⊢ φ → ∫ A if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 dx = ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx
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 → if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 = if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
78 77 itgeq2dv ⊢ φ → ∫ A if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 dx = ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx
79 71 78 oveq12d ⊢ φ → ∫ A if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 dx = ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx − ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx
80 67 79 eqtr4d ⊢ φ → − ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx = ∫ A if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 dx
81 12 13 itgreval ⊢ φ → ∫ A ℑ ⁡ B dx = ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx
82 81 negeqd ⊢ φ → − ∫ A ℑ ⁡ B dx = − ∫ A if 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 dx
83 33 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ − B ∈ ℝ
84 37 simprd ⊢ φ → x ∈ A ⟼ ℑ ⁡ − B ∈ 𝐿 1
85 83 84 itgreval ⊢ φ → ∫ A ℑ ⁡ − B dx = ∫ A if 0 ≤ ℑ ⁡ − B ℑ ⁡ − B 0 dx − ∫ A if 0 ≤ − ℑ ⁡ − B − ℑ ⁡ − B 0 dx
86 80 82 85 3eqtr4d ⊢ φ → − ∫ A ℑ ⁡ B dx = ∫ A ℑ ⁡ − B dx
87 86 oveq2d ⊢ φ → i ⁢ − ∫ A ℑ ⁡ B dx = i ⁢ ∫ A ℑ ⁡ − B dx
88 55 87 eqtr3d ⊢ φ → − i ⁢ ∫ A ℑ ⁡ B dx = i ⁢ ∫ A ℑ ⁡ − B dx
89 53 88 oveq12d ⊢ φ → - ∫ A ℜ ⁡ B dx + − i ⁢ ∫ A ℑ ⁡ B dx = ∫ A ℜ ⁡ − B dx + i ⁢ ∫ A ℑ ⁡ − B dx
90 17 89 eqtrd ⊢ φ → − ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx = ∫ A ℜ ⁡ − B dx + i ⁢ ∫ A ℑ ⁡ − B dx
91 1 2 itgcnval ⊢ φ → ∫ A B dx = ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx
92 91 negeqd ⊢ φ → − ∫ A B dx = − ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx
93 33 35 itgcnval ⊢ φ → ∫ A − B dx = ∫ A ℜ ⁡ − B dx + i ⁢ ∫ A ℑ ⁡ − B dx
94 90 92 93 3eqtr4d ⊢ φ → − ∫ A B dx = ∫ A − B dx