sublevolico

Description: The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	sublevolico.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	sublevolico.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	sublevolico	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sublevolico.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		sublevolico.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
4		eqidd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
5	3 4	eqled	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( 𝐵 − 𝐴 ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ≤ ( 𝐵 − 𝐴 ) )
7		volico	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
10		iftrue	⊢ ( 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
12	9 11	eqtr2d	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
13	6 12	breqtrd	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
14		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → ¬ 𝐴 < 𝐵 )
15	2 1	lenltd	⊢ ( 𝜑 → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
17	14 16	mpbird	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ≤ 𝐴 )
18	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
19	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
20	18 19	suble0d	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → ( ( 𝐵 − 𝐴 ) ≤ 0 ↔ 𝐵 ≤ 𝐴 ) )
21	17 20	mpbird	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ≤ 0 )
22	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
23		iffalse	⊢ ( ¬ 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
24	23	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
25	22 24	eqtr2d	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → 0 = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
26	21 25	breqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
27	13 26	pm2.61dan	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )

Metamath Proof Explorer

Theorem sublevolico

Proof