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

Proof

Step	Hyp	Ref	Expression
1		voliooico.1	|- ( ph -> A e. RR )
2		voliooico.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		volioo	|- ( ( 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	2	adantr	|- ( ( ph /\ B < A ) -> B e. RR )
39	1	adantr	|- ( ( ph /\ B < A ) -> A e. RR )
40		simpr	|- ( ( ph /\ B < A ) -> B < A )
41	38 39 40	ltled	|- ( ( ph /\ B < A ) -> B <_ A )
42	39	rexrd	|- ( ( ph /\ B < A ) -> A e. RR* )
43	38	rexrd	|- ( ( ph /\ B < A ) -> B e. RR* )
44		ioo0	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
45	42 43 44	syl2anc	|- ( ( ph /\ B < A ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
46	41 45	mpbird	|- ( ( ph /\ B < A ) -> ( A (,) B ) = (/) )
47		ico0	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
48	42 43 47	syl2anc	|- ( ( ph /\ B < A ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
49	41 48	mpbird	|- ( ( ph /\ B < A ) -> ( A [,) B ) = (/) )
50	46 49	eqtr4d	|- ( ( ph /\ B < A ) -> ( A (,) B ) = ( A [,) B ) )
51	50	fveq2d	|- ( ( ph /\ B < A ) -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )
52	32 37 51	syl2anc	|- ( ( ph /\ -. A <_ B ) -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )
53	31 52	pm2.61dan	|- ( ph -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )