Metamath Proof Explorer

Theorem 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 ${⊢}{\phi }\to {A}\in ℝ$
sublevolico.b ${⊢}{\phi }\to {B}\in ℝ$
Assertion sublevolico ${⊢}{\phi }\to {B}-{A}\le vol\left(\left[{A},{B}\right)\right)$

Proof

Step Hyp Ref Expression
1 sublevolico.a ${⊢}{\phi }\to {A}\in ℝ$
2 sublevolico.b ${⊢}{\phi }\to {B}\in ℝ$
3 2 1 resubcld ${⊢}{\phi }\to {B}-{A}\in ℝ$
4 eqidd ${⊢}{\phi }\to {B}-{A}={B}-{A}$
5 3 4 eqled ${⊢}{\phi }\to {B}-{A}\le {B}-{A}$
6 5 adantr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {B}-{A}\le {B}-{A}$
7 volico ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to vol\left(\left[{A},{B}\right)\right)=if\left({A}<{B},{B}-{A},0\right)$
8 1 2 7 syl2anc ${⊢}{\phi }\to vol\left(\left[{A},{B}\right)\right)=if\left({A}<{B},{B}-{A},0\right)$
9 8 adantr ${⊢}\left({\phi }\wedge {A}<{B}\right)\to vol\left(\left[{A},{B}\right)\right)=if\left({A}<{B},{B}-{A},0\right)$
10 iftrue ${⊢}{A}<{B}\to if\left({A}<{B},{B}-{A},0\right)={B}-{A}$
11 10 adantl ${⊢}\left({\phi }\wedge {A}<{B}\right)\to if\left({A}<{B},{B}-{A},0\right)={B}-{A}$
12 9 11 eqtr2d ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {B}-{A}=vol\left(\left[{A},{B}\right)\right)$
13 6 12 breqtrd ${⊢}\left({\phi }\wedge {A}<{B}\right)\to {B}-{A}\le vol\left(\left[{A},{B}\right)\right)$
14 simpr ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to ¬{A}<{B}$
15 2 1 lenltd ${⊢}{\phi }\to \left({B}\le {A}↔¬{A}<{B}\right)$
16 15 adantr ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
17 14 16 mpbird ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to {B}\le {A}$
18 2 adantr ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to {B}\in ℝ$
19 1 adantr ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to {A}\in ℝ$
20 18 19 suble0d ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to \left({B}-{A}\le 0↔{B}\le {A}\right)$
21 17 20 mpbird ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to {B}-{A}\le 0$
22 8 adantr ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to vol\left(\left[{A},{B}\right)\right)=if\left({A}<{B},{B}-{A},0\right)$
23 iffalse ${⊢}¬{A}<{B}\to if\left({A}<{B},{B}-{A},0\right)=0$
24 23 adantl ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to if\left({A}<{B},{B}-{A},0\right)=0$
25 22 24 eqtr2d ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to 0=vol\left(\left[{A},{B}\right)\right)$
26 21 25 breqtrd ${⊢}\left({\phi }\wedge ¬{A}<{B}\right)\to {B}-{A}\le vol\left(\left[{A},{B}\right)\right)$
27 13 26 pm2.61dan ${⊢}{\phi }\to {B}-{A}\le vol\left(\left[{A},{B}\right)\right)$