Theorem iccvolcl 25495

Description: A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.)

Assertion

Ref	Expression
iccvolcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)

Proof of Theorem iccvolcl

Step	Hyp	Ref	Expression
1		iccmbl 25494	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
2		mblvol 25458	. . 3 ⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
3	1, 2	syl 17	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
4		rexr 11246	. . . . . 6 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
5		rexr 11246	. . . . . 6 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
6		icc0 13380	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
7	4, 5, 6	syl2an 596	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴))
8	7	biimpar 477	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅)
9		fveq2 6866	. . . . . 6 ⊢ ((𝐴[,]𝐵) = ∅ → (vol*‘(𝐴[,]𝐵)) = (vol*‘∅))
10		ovol0 25421	. . . . . 6 ⊢ (vol*‘∅) = 0
11	9, 10	eqtrdi 2781	. . . . 5 ⊢ ((𝐴[,]𝐵) = ∅ → (vol*‘(𝐴[,]𝐵)) = 0)
12		0re 11202	. . . . 5 ⊢ 0 ∈ ℝ
13	11, 12	eqeltrdi 2837	. . . 4 ⊢ ((𝐴[,]𝐵) = ∅ → (vol*‘(𝐴[,]𝐵)) ∈ ℝ)
14	8, 13	syl 17	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (vol*‘(𝐴[,]𝐵)) ∈ ℝ)
15		ovolicc 25451	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
16	15	3expa 1118	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
17		resubcl 11512	. . . . . 6 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 − 𝐴) ∈ ℝ)
18	17	ancoms 458	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 − 𝐴) ∈ ℝ)
19	18	adantr 480	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) ∈ ℝ)
20	16, 19	eqeltrd 2829	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) ∈ ℝ)
21		simpr 484	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
22		simpl 482	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
23	14, 20, 21, 22	ltlecasei 11308	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol*‘(𝐴[,]𝐵)) ∈ ℝ)
24	3, 23	eqeltrd 2829	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∅c0 4304   class class class wbr 5115  dom cdm 5646  ‘cfv 6519  (class class class)co 7395  ℝcr 11093  0cc0 11094  ℝ^*cxr 11233   < clt 11234   ≤ cle 11235   − cmin 11431  [,]cicc 13335  vol*covol 25390  volcvol 25391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5242  ax-sep 5259  ax-nul 5269  ax-pow 5328  ax-pr 5395  ax-un 7719  ax-inf2 9620  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171  ax-pre-sup 11172

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ne 2928  df-nel 3032  df-ral 3047  df-rex 3056  df-rmo 3357  df-reu 3358  df-rab 3412  df-v 3457  df-sbc 3762  df-csb 3871  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-pss 3942  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-op 4604  df-uni 4880  df-int 4919  df-iun 4965  df-br 5116  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5541  df-eprel 5546  df-po 5554  df-so 5555  df-fr 5599  df-se 5600  df-we 5601  df-xp 5652  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-rn 5657  df-res 5658  df-ima 5659  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6472  df-fun 6521  df-fn 6522  df-f 6523  df-f1 6524  df-fo 6525  df-f1o 6526  df-fv 6527  df-isom 6528  df-riota 7352  df-ov 7398  df-oprab 7399  df-mpo 7400  df-of 7661  df-om 7852  df-1st 7978  df-2nd 7979  df-frecs 8270  df-wrecs 8301  df-recs 8350  df-rdg 8388  df-1o 8444  df-2o 8445  df-er 8683  df-map 8813  df-pm 8814  df-en 8931  df-dom 8932  df-sdom 8933  df-fin 8934  df-fi 9388  df-sup 9419  df-inf 9420  df-oi 9489  df-dju 9880  df-card 9918  df-pnf 11236  df-mnf 11237  df-xr 11238  df-ltxr 11239  df-le 11240  df-sub 11433  df-neg 11434  df-div 11862  df-nn 12208  df-2 12270  df-3 12271  df-n0 12469  df-z 12556  df-uz 12820  df-q 12934  df-rp 12978  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13336  df-ico 13338  df-icc 13339  df-fz 13495  df-fzo 13642  df-fl 13780  df-seq 13993  df-exp 14053  df-hash 14322  df-cj 15091  df-re 15092  df-im 15093  df-sqrt 15227  df-abs 15228  df-clim 15480  df-rlim 15481  df-sum 15679  df-rest 17411  df-topgen 17432  df-psmet 21282  df-xmet 21283  df-met 21284  df-bl 21285  df-mopn 21286  df-top 22807  df-topon 22824  df-bases 22859  df-cmp 23300  df-ovol 25392  df-vol 25393

This theorem is referenced by:  volcn  25534  mbfi1fseqlem4  25646  cniccibl  25769  cnicciblnc  25771  ftc1lem4  25973  ftc1cnnclem  37701  fourierdlem87  46205