Theorem voliooico

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

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

Proof

Step	Hyp	Ref	Expression
1		voliooico.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		voliooico.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		volioo	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 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	2	adantr	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐵 ∈ ℝ )
39	1	adantr	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐴 ∈ ℝ )
40		simpr	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐵 < 𝐴 )
41	38 39 40	ltled	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐵 ≤ 𝐴 )
42	39	rexrd	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐴 ∈ ℝ* )
43	38	rexrd	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐵 ∈ ℝ* )
44		ioo0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
45	42 43 44	syl2anc	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
46	41 45	mpbird	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
47		ico0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
48	42 43 47	syl2anc	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
49	41 48	mpbird	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,) 𝐵 ) = ∅ )
50	46 49	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝐴 (,) 𝐵 ) = ( 𝐴 [,) 𝐵 ) )
51	50	fveq2d	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
52	32 37 51	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
53	31 52	pm2.61dan	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )