Theorem volico 43037

Description: The measure of left-closed, right-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Assertion

Ref	Expression
volico	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0))

Proof of Theorem volico

Step	Hyp	Ref	Expression
1		rexr 10739	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2	1	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ*)
3		rexr 10739	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
4	3	3ad2ant2 1132	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ*)
5		simp3 1136	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
6		snunioo1 42561	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵))
7	2, 4, 5, 6	syl3anc 1369	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵))
8	7	eqcomd 2765	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴[,)𝐵) = ((𝐴(,)𝐵) ∪ {𝐴}))
9	8	fveq2d 6668	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = (vol‘((𝐴(,)𝐵) ∪ {𝐴})))
10		ioombl 24280	. . . . . . 7 ⊢ (𝐴(,)𝐵) ∈ dom vol
11	10	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐴(,)𝐵) ∈ dom vol)
12		snmbl 43017	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → {𝐴} ∈ dom vol)
13	12	3ad2ant1 1131	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → {𝐴} ∈ dom vol)
14		lbioo 12824	. . . . . . . 8 ⊢ ¬ 𝐴 ∈ (𝐴(,)𝐵)
15		disjsn 4608	. . . . . . . 8 ⊢ (((𝐴(,)𝐵) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝐵))
16	14, 15	mpbir 234	. . . . . . 7 ⊢ ((𝐴(,)𝐵) ∩ {𝐴}) = ∅
17	16	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∩ {𝐴}) = ∅)
18		ioovolcl 24285	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
19	18	3adant3 1130	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
20		volsn 43021	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (vol‘{𝐴}) = 0)
21		0red 10696	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
22	20, 21	eqeltrd 2853	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (vol‘{𝐴}) ∈ ℝ)
23	22	3ad2ant1 1131	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘{𝐴}) ∈ ℝ)
24		volun 24260	. . . . . 6 ⊢ ((((𝐴(,)𝐵) ∈ dom vol ∧ {𝐴} ∈ dom vol ∧ ((𝐴(,)𝐵) ∩ {𝐴}) = ∅) ∧ ((vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ (vol‘{𝐴}) ∈ ℝ)) → (vol‘((𝐴(,)𝐵) ∪ {𝐴})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴})))
25	11, 13, 17, 19, 23, 24	syl32anc 1376	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐴})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴})))
26		simp1 1134	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℝ)
27		simp2 1135	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ)
28	26, 27, 5	ltled 10840	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ≤ 𝐵)
29		volioo 24284	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
30	26, 27, 28, 29	syl3anc 1369	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
31	20	3ad2ant1 1131	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘{𝐴}) = 0)
32	30, 31	oveq12d 7175	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴})) = ((𝐵 − 𝐴) + 0))
33	27	recnd 10721	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ)
34		recn 10679	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
35	34	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℂ)
36	33, 35	subcld 11049	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈ ℂ)
37	36	addid1d 10892	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐵 − 𝐴) + 0) = (𝐵 − 𝐴))
38	32, 37	eqtrd 2794	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴})) = (𝐵 − 𝐴))
39	9, 25, 38	3eqtrd 2798	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = (𝐵 − 𝐴))
40	39	3expa 1116	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = (𝐵 − 𝐴))
41		iftrue 4430	. . . 4 ⊢ (𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴))
42	41	adantl 485	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = (𝐵 − 𝐴))
43	40, 42	eqtr4d 2797	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0))
44		simpl 486	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
45		simpr 488	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → ¬ 𝐴 < 𝐵)
46	44	simprd 499	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → 𝐵 ∈ ℝ)
47	44	simpld 498	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → 𝐴 ∈ ℝ)
48	46, 47	lenltd 10838	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
49	45, 48	mpbird 260	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → 𝐵 ≤ 𝐴)
50		simpr 488	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → 𝐵 ≤ 𝐴)
51	1	ad2antrr 725	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → 𝐴 ∈ ℝ*)
52	3	ad2antlr 726	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → 𝐵 ∈ ℝ*)
53		ico0 12839	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
54	51, 52, 53	syl2anc 587	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → ((𝐴[,)𝐵) = ∅ ↔ 𝐵 ≤ 𝐴))
55	50, 54	mpbird 260	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (𝐴[,)𝐵) = ∅)
56	55	fveq2d 6668	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (vol‘(𝐴[,)𝐵)) = (vol‘∅))
57		vol0 43013	. . . . . 6 ⊢ (vol‘∅) = 0
58	57	a1i 11	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (vol‘∅) = 0)
59	56, 58	eqtrd 2794	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≤ 𝐴) → (vol‘(𝐴[,)𝐵)) = 0)
60	44, 49, 59	syl2anc 587	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = 0)
61		iffalse 4433	. . . 4 ⊢ (¬ 𝐴 < 𝐵 → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0)
62	61	adantl 485	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → if(𝐴 < 𝐵, (𝐵 − 𝐴), 0) = 0)
63	60, 62	eqtr4d 2797	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ 𝐴 < 𝐵) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0))
64	43, 63	pm2.61dan 812	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) = if(𝐴 < 𝐵, (𝐵 − 𝐴), 0))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ∪ cun 3859   ∩ cin 3860  ∅c0 4228  ifcif 4424  {csn 4526   class class class wbr 5037  dom cdm 5529  ‘cfv 6341  (class class class)co 7157  ℂcc 10587  ℝcr 10588  0cc0 10589   + caddc 10592  ℝ^*cxr 10726   < clt 10727   ≤ cle 10728   − cmin 10922  (,)cioo 12793  [,)cico 12795  volcvol 24178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-inf2 9151  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-pre-sup 10667

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-se 5489  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-of 7412  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-1o 8119  df-2o 8120  df-er 8306  df-map 8425  df-pm 8426  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-fi 8922  df-sup 8953  df-inf 8954  df-oi 9021  df-dju 9377  df-card 9415  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-div 11350  df-nn 11689  df-2 11751  df-3 11752  df-n0 11949  df-z 12035  df-uz 12297  df-q 12403  df-rp 12445  df-xneg 12562  df-xadd 12563  df-xmul 12564  df-ioo 12797  df-ico 12799  df-icc 12800  df-fz 12954  df-fzo 13097  df-fl 13225  df-seq 13433  df-exp 13494  df-hash 13755  df-cj 14520  df-re 14521  df-im 14522  df-sqrt 14656  df-abs 14657  df-clim 14907  df-rlim 14908  df-sum 15105  df-rest 16769  df-topgen 16790  df-psmet 20173  df-xmet 20174  df-met 20175  df-bl 20176  df-mopn 20177  df-top 21609  df-topon 21626  df-bases 21661  df-cmp 22102  df-ovol 24179  df-vol 24180

This theorem is referenced by:  sublevolico  43038  voliooico  43046  voliccico  43053  volicorecl  43597  hoiprodcl  43598  hoicvrrex  43607  volicon0  43626  hoiprodcl3  43631  volicore  43632  hoidmvcl  43633  hoidmvval0  43638  hoidmv1lelem2  43643  hoidmv1le  43645  hoidmvlelem2  43647  hoidmvlelem3  43648  hoidmvlelem4  43649  hspmbllem1  43677  volico2  43692  ovolval2lem  43694  vonioolem1  43731  vonioo  43733  vonicclem1  43734