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 ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = 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 ⊢ φ → if x ∈ A ∧ 0 ≤ − B − B 0 = if x ∈ A ∧ 0 ≤ − B 0 0
14 ifid ⊢ if x ∈ A ∧ 0 ≤ − B 0 0 = 0
15 13 14 eqtrdi ⊢ φ → if x ∈ A ∧ 0 ≤ − B − B 0 = 0
16 15 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = x ∈ ℝ ⟼ 0
17 fconstmpt ⊢ ℝ × 0 = x ∈ ℝ ⟼ 0
18 16 17 eqtr4di ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = ℝ × 0
19 18 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = ∫ 2 ⁡ ℝ × 0
20 itg20 ⊢ ∫ 2 ⁡ ℝ × 0 = 0
21 19 20 eqtrdi ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − B − B 0 = 0