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 )