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	|- ( ph -> A e. RR )
	voliccico.2	|- ( ph -> B e. RR )
Assertion	voliccico	|- ( ph -> ( vol ` ( A [,] B ) ) = ( vol ` ( A [,) B ) ) )

Proof

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