Metamath Proof Explorer

Theorem itgrevallem1

Description: Lemma for itgposval and itgreval . (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblrelem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
itgreval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
Assertion itgrevallem1 ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢ φ ∧ x ∈ A → B ∈ ℝ
2 itgreval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
4 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
5 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
6 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
7 3 4 5 6 1 2 itgcnlem ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 - ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 + i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
8 1 rered ⊢ φ ∧ x ∈ A → ℜ ⁡ B = B
9 8 ibllem ⊢ φ → if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = if x ∈ A ∧ 0 ≤ B B 0
10 9 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0
11 10 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0
12 8 negeqd ⊢ φ ∧ x ∈ A → − ℜ ⁡ B = − B
13 12 ibllem ⊢ φ → if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = if x ∈ A ∧ 0 ≤ − B − B 0
14 13 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
15 14 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
16 11 15 oveq12d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
17 1 reim0d ⊢ φ ∧ x ∈ A → ℑ ⁡ B = 0
18 17 itgvallem3 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 = 0
19 17 negeqd ⊢ φ ∧ x ∈ A → − ℑ ⁡ B = − 0
20 neg0 ⊢ − 0 = 0
21 19 20 eqtrdi ⊢ φ ∧ x ∈ A → − ℑ ⁡ B = 0
22 21 itgvallem3 ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = 0
23 18 22 oveq12d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = 0 − 0
24 0m0e0 ⊢ 0 − 0 = 0
25 23 24 eqtrdi ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = 0
26 25 oveq2d ⊢ φ → i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = i ⋅ 0
27 it0e0 ⊢ i ⋅ 0 = 0
28 26 27 eqtrdi ⊢ φ → i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = 0
29 16 28 oveq12d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 - ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 + i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 - ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 + 0
30 1 iblrelem ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
31 2 30 mpbid ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
32 31 simp2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 ∈ ℝ
33 31 simp3d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
34 32 33 resubcld ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℝ
35 34 recnd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 ∈ ℂ
36 35 addid1d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 - ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 + 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0
37 7 29 36 3eqtrd ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ B B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0