This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
iblpos.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion iblposlem ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 iblpos.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
3 1 le0neg2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝐵 ↔ - 𝐵 ≤ 0 ) )
4 2 3 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ≤ 0 )
5 4 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → - 𝐵 ≤ 0 )
6 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → 0 ≤ - 𝐵 )
7 1 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → 𝐵 ∈ ℝ )
8 7 renegcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → - 𝐵 ∈ ℝ )
9 0re ⊢ 0 ∈ ℝ
10 letri3 ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝐵 = 0 ↔ ( - 𝐵 ≤ 0 ∧ 0 ≤ - 𝐵 ) ) )
11 8 9 10 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → ( - 𝐵 = 0 ↔ ( - 𝐵 ≤ 0 ∧ 0 ≤ - 𝐵 ) ) )
12 5 6 11 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) ) → - 𝐵 = 0 )
13 12 ifeq1da ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , 0 , 0 ) )
14 ifid ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , 0 , 0 ) = 0
15 13 14 eqtrdi ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) = 0 )
16 15 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
17 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
18 16 17 eqtr4di ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) = ( ℝ × { 0 } ) )
19 18 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) ) )
20 itg20 ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
21 19 20 eqtrdi ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) = 0 )