Metamath Proof Explorer

Theorem iblposlem

Description: Lemma for iblpos . (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 ℝ$
iblpos.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le {B}$
Assertion iblposlem ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)=0$

Proof

Step Hyp Ref Expression
1 iblrelem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 iblpos.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le {B}$
3 1 le0neg2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(0\le {B}↔-{B}\le 0\right)$
4 2 3 mpbid ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -{B}\le 0$
5 4 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le -{B}\right)\right)\to -{B}\le 0$
6 simprr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le -{B}\right)\right)\to 0\le -{B}$
7 1 adantrr ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le -{B}\right)\right)\to {B}\in ℝ$
8 7 renegcld ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le -{B}\right)\right)\to -{B}\in ℝ$
9 0re ${⊢}0\in ℝ$
10 letri3 ${⊢}\left(-{B}\in ℝ\wedge 0\in ℝ\right)\to \left(-{B}=0↔\left(-{B}\le 0\wedge 0\le -{B}\right)\right)$
11 8 9 10 sylancl ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le -{B}\right)\right)\to \left(-{B}=0↔\left(-{B}\le 0\wedge 0\le -{B}\right)\right)$
12 5 6 11 mpbir2and ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge 0\le -{B}\right)\right)\to -{B}=0$
13 12 ifeq1da ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)=if\left(\left({x}\in {A}\wedge 0\le -{B}\right),0,0\right)$
14 ifid ${⊢}if\left(\left({x}\in {A}\wedge 0\le -{B}\right),0,0\right)=0$
15 13 14 eqtrdi ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)=0$
16 15 mpteq2dv ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)=\left({x}\in ℝ⟼0\right)$
17 fconstmpt ${⊢}ℝ×\left\{0\right\}=\left({x}\in ℝ⟼0\right)$
18 16 17 eqtr4di ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)=ℝ×\left\{0\right\}$
19 18 fveq2d ${⊢}{\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\{0\right\}\right)$
20 itg20 ${⊢}{\int }^{2}\left(ℝ×\left\{0\right\}\right)=0$
21 19 20 eqtrdi ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)=0$