Metamath Proof Explorer


Theorem voliccico

Description: A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses voliccico.1 ( 𝜑𝐴 ∈ ℝ )
voliccico.2 ( 𝜑𝐵 ∈ ℝ )
Assertion voliccico ( 𝜑 → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 voliccico.1 ( 𝜑𝐴 ∈ ℝ )
2 voliccico.2 ( 𝜑𝐵 ∈ ℝ )
3 iftrue ( 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) = ( 𝐵𝐴 ) )
4 3 adantl ( ( ( 𝜑𝐴𝐵 ) ∧ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) = ( 𝐵𝐴 ) )
5 2 recnd ( 𝜑𝐵 ∈ ℂ )
6 5 subidd ( 𝜑 → ( 𝐵𝐵 ) = 0 )
7 6 eqcomd ( 𝜑 → 0 = ( 𝐵𝐵 ) )
8 7 ad2antrr ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 0 = ( 𝐵𝐵 ) )
9 iffalse ( ¬ 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) = 0 )
10 9 adantl ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) = 0 )
11 simpll ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝜑 )
12 11 1 syl ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
13 11 2 syl ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
14 simpr ( ( 𝜑𝐴𝐵 ) → 𝐴𝐵 )
15 14 adantr ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴𝐵 )
16 simpr ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → ¬ 𝐴 < 𝐵 )
17 12 13 15 16 lenlteq ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 = 𝐵 )
18 oveq2 ( 𝐴 = 𝐵 → ( 𝐵𝐴 ) = ( 𝐵𝐵 ) )
19 18 adantl ( ( 𝜑𝐴 = 𝐵 ) → ( 𝐵𝐴 ) = ( 𝐵𝐵 ) )
20 11 17 19 syl2anc ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐵𝐴 ) = ( 𝐵𝐵 ) )
21 8 10 20 3eqtr4d ( ( ( 𝜑𝐴𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) = ( 𝐵𝐴 ) )
22 4 21 pm2.61dan ( ( 𝜑𝐴𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) = ( 𝐵𝐴 ) )
23 22 eqcomd ( ( 𝜑𝐴𝐵 ) → ( 𝐵𝐴 ) = if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) )
24 1 adantr ( ( 𝜑𝐴𝐵 ) → 𝐴 ∈ ℝ )
25 2 adantr ( ( 𝜑𝐴𝐵 ) → 𝐵 ∈ ℝ )
26 volicc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵𝐴 ) )
27 24 25 14 26 syl3anc ( ( 𝜑𝐴𝐵 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵𝐴 ) )
28 volico ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) )
29 1 2 28 syl2anc ( 𝜑 → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) )
30 29 adantr ( ( 𝜑𝐴𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵𝐴 ) , 0 ) )
31 23 27 30 3eqtr4d ( ( 𝜑𝐴𝐵 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
32 simpl ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → 𝜑 )
33 simpr ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → ¬ 𝐴𝐵 )
34 32 2 syl ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → 𝐵 ∈ ℝ )
35 32 1 syl ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → 𝐴 ∈ ℝ )
36 34 35 ltnled ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → ( 𝐵 < 𝐴 ↔ ¬ 𝐴𝐵 ) )
37 33 36 mpbird ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → 𝐵 < 𝐴 )
38 simpr ( ( 𝜑𝐵 < 𝐴 ) → 𝐵 < 𝐴 )
39 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
40 2 rexrd ( 𝜑𝐵 ∈ ℝ* )
41 icc0 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
42 39 40 41 syl2anc ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
43 42 adantr ( ( 𝜑𝐵 < 𝐴 ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
44 38 43 mpbird ( ( 𝜑𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
45 2 adantr ( ( 𝜑𝐵 < 𝐴 ) → 𝐵 ∈ ℝ )
46 1 adantr ( ( 𝜑𝐵 < 𝐴 ) → 𝐴 ∈ ℝ )
47 45 46 38 ltled ( ( 𝜑𝐵 < 𝐴 ) → 𝐵𝐴 )
48 46 rexrd ( ( 𝜑𝐵 < 𝐴 ) → 𝐴 ∈ ℝ* )
49 45 rexrd ( ( 𝜑𝐵 < 𝐴 ) → 𝐵 ∈ ℝ* )
50 ico0 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵𝐴 ) )
51 48 49 50 syl2anc ( ( 𝜑𝐵 < 𝐴 ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵𝐴 ) )
52 47 51 mpbird ( ( 𝜑𝐵 < 𝐴 ) → ( 𝐴 [,) 𝐵 ) = ∅ )
53 44 52 eqtr4d ( ( 𝜑𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ( 𝐴 [,) 𝐵 ) )
54 53 fveq2d ( ( 𝜑𝐵 < 𝐴 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
55 32 37 54 syl2anc ( ( 𝜑 ∧ ¬ 𝐴𝐵 ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
56 31 55 pm2.61dan ( 𝜑 → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )