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 ‘ ( 𝐴 [,) 𝐵 ) ) )

Metamath Proof Explorer

Theorem voliccico

Proof