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 ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0

Proof

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