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 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
itgreval.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
Assertion itgrevallem1 ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 iblrelem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 itgreval.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
3 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)$
4 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)$
5 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)$
6 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)$
7 3 4 5 6 1 2 itgcnlem ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)+\mathrm{i}\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\right)$
8 1 rered ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left({B}\right)={B}$
9 8 ibllem ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)$
10 9 mpteq2dv ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)$
11 10 fveq2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)$
12 8 negeqd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -\Re \left({B}\right)=-{B}$
13 12 ibllem ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)$
14 13 mpteq2dv ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)$
15 14 fveq2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$
16 11 15 oveq12d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$
17 1 reim0d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Im \left({B}\right)=0$
18 17 itgvallem3 ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)=0$
19 17 negeqd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -\Im \left({B}\right)=-0$
20 neg0 ${⊢}-0=0$
21 19 20 syl6eq ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -\Im \left({B}\right)=0$
22 21 itgvallem3 ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)=0$
23 18 22 oveq12d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)=0-0$
24 0m0e0 ${⊢}0-0=0$
25 23 24 syl6eq ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)=0$
26 25 oveq2d ${⊢}{\phi }\to \mathrm{i}\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\right)=\mathrm{i}\cdot 0$
27 it0e0 ${⊢}\mathrm{i}\cdot 0=0$
28 26 27 syl6eq ${⊢}{\phi }\to \mathrm{i}\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\right)=0$
29 16 28 oveq12d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)+\mathrm{i}\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)+0$
30 1 iblrelem ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$
31 2 30 mpbid ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)$
32 31 simp2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ$
33 31 simp3d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ$
34 32 33 resubcld ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ$
35 34 recnd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℂ$
36 35 addid1d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)+0={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$
37 7 29 36 3eqtrd ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)-{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$