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

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢φ∧x∈A→B∈ℝ
2 iblpos.2 ⊢φ∧x∈A→0≤B
3 1 le0neg2d ⊢φ∧x∈A→0≤B↔−B≤0
4 2 3 mpbid ⊢φ∧x∈A→−B≤0
5 4 adantrr ⊢φ∧x∈A∧0≤−B→−B≤0
6 simprr ⊢φ∧x∈A∧0≤−B→0≤−B
7 1 adantrr ⊢φ∧x∈A∧0≤−B→B∈ℝ
8 7 renegcld ⊢φ∧x∈A∧0≤−B→−B∈ℝ
9 0re ⊢0∈ℝ
10 letri3 ⊢−B∈ℝ∧0∈ℝ→−B=0↔−B≤0∧0≤−B
11 8 9 10 sylancl ⊢φ∧x∈A∧0≤−B→−B=0↔−B≤0∧0≤−B
12 5 6 11 mpbir2and ⊢φ∧x∈A∧0≤−B→−B=0
13 12 ifeq1da ⊢φ→ifx∈A∧0≤−B−B0=ifx∈A∧0≤−B00
14 ifid ⊢ifx∈A∧0≤−B00=0
15 13 14 eqtrdi ⊢φ→ifx∈A∧0≤−B−B0=0
16 15 mpteq2dv ⊢φ→x∈ℝ⟼ifx∈A∧0≤−B−B0=x∈ℝ⟼0
17 fconstmpt ⊢ℝ×0=x∈ℝ⟼0
18 16 17 eqtr4di ⊢φ→x∈ℝ⟼ifx∈A∧0≤−B−B0=ℝ×0
19 18 fveq2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=∫2⁡ℝ×0
20 itg20 ⊢∫2⁡ℝ×0=0
21 19 20 eqtrdi ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=0