Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  volico Structured version   Visualization version   Unicode version

Theorem volico 37947
Description: The measure of left closed, right open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Assertion
Ref Expression
volico  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A [,) B ) )  =  if ( A  <  B ,  ( B  -  A ) ,  0 ) )

Proof of Theorem volico
StepHypRef Expression
1 rexr 9717 . . . . . . . . 9  |-  ( A  e.  RR  ->  A  e.  RR* )
213ad2ant1 1035 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  A  e.  RR* )
3 rexr 9717 . . . . . . . . 9  |-  ( B  e.  RR  ->  B  e.  RR* )
433ad2ant2 1036 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  B  e.  RR* )
5 simp3 1016 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  A  <  B )
6 snunioo1 37698 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  (
( A (,) B
)  u.  { A } )  =  ( A [,) B ) )
72, 4, 5, 6syl3anc 1276 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A (,) B
)  u.  { A } )  =  ( A [,) B ) )
87eqcomd 2468 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( A [,) B )  =  ( ( A (,) B )  u.  { A } ) )
98fveq2d 5896 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  ( A [,) B ) )  =  ( vol `  (
( A (,) B
)  u.  { A } ) ) )
10 ioombl 22574 . . . . . . 7  |-  ( A (,) B )  e. 
dom  vol
1110a1i 11 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( A (,) B )  e. 
dom  vol )
12 snmbl 37926 . . . . . . 7  |-  ( A  e.  RR  ->  { A }  e.  dom  vol )
13123ad2ant1 1035 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  { A }  e.  dom  vol )
14 lbioo 11701 . . . . . . . 8  |-  -.  A  e.  ( A (,) B
)
15 disjsn 4044 . . . . . . . 8  |-  ( ( ( A (,) B
)  i^i  { A } )  =  (/)  <->  -.  A  e.  ( A (,) B ) )
1614, 15mpbir 214 . . . . . . 7  |-  ( ( A (,) B )  i^i  { A }
)  =  (/)
1716a1i 11 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A (,) B
)  i^i  { A } )  =  (/) )
18 ioovolcl 22578 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A (,) B ) )  e.  RR )
19183adant3 1034 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  ( A (,) B ) )  e.  RR )
20 volsn 37930 . . . . . . . 8  |-  ( A  e.  RR  ->  ( vol `  { A }
)  =  0 )
21 0red 9675 . . . . . . . 8  |-  ( A  e.  RR  ->  0  e.  RR )
2220, 21eqeltrd 2540 . . . . . . 7  |-  ( A  e.  RR  ->  ( vol `  { A }
)  e.  RR )
23223ad2ant1 1035 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  { A }
)  e.  RR )
24 volun 22554 . . . . . 6  |-  ( ( ( ( A (,) B )  e.  dom  vol 
/\  { A }  e.  dom  vol  /\  (
( A (,) B
)  i^i  { A } )  =  (/) )  /\  ( ( vol `  ( A (,) B
) )  e.  RR  /\  ( vol `  { A } )  e.  RR ) )  ->  ( vol `  ( ( A (,) B )  u. 
{ A } ) )  =  ( ( vol `  ( A (,) B ) )  +  ( vol `  { A } ) ) )
2511, 13, 17, 19, 23, 24syl32anc 1284 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  ( ( A (,) B )  u. 
{ A } ) )  =  ( ( vol `  ( A (,) B ) )  +  ( vol `  { A } ) ) )
26 simp1 1014 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  A  e.  RR )
27 simp2 1015 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  B  e.  RR )
2826, 27, 5ltled 9814 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  A  <_  B )
29 volioo 37911 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( vol `  ( A (,) B ) )  =  ( B  -  A
) )
3026, 27, 28, 29syl3anc 1276 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  ( A (,) B ) )  =  ( B  -  A
) )
31203ad2ant1 1035 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  { A }
)  =  0 )
3230, 31oveq12d 6338 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( vol `  ( A (,) B ) )  +  ( vol `  { A } ) )  =  ( ( B  -  A )  +  0 ) )
3327recnd 9700 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  B  e.  CC )
34 recn 9660 . . . . . . . . 9  |-  ( A  e.  RR  ->  A  e.  CC )
35343ad2ant1 1035 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  A  e.  CC )
3633, 35subcld 10017 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( B  -  A )  e.  CC )
3736addid1d 9864 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( B  -  A
)  +  0 )  =  ( B  -  A ) )
3832, 37eqtrd 2496 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( vol `  ( A (,) B ) )  +  ( vol `  { A } ) )  =  ( B  -  A
) )
399, 25, 383eqtrd 2500 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  ( vol `  ( A [,) B ) )  =  ( B  -  A
) )
40393expa 1215 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <  B
)  ->  ( vol `  ( A [,) B
) )  =  ( B  -  A ) )
41 iftrue 3899 . . . 4  |-  ( A  <  B  ->  if ( A  <  B , 
( B  -  A
) ,  0 )  =  ( B  -  A ) )
4241adantl 472 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <  B
)  ->  if ( A  <  B ,  ( B  -  A ) ,  0 )  =  ( B  -  A
) )
4340, 42eqtr4d 2499 . 2  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  A  <  B
)  ->  ( vol `  ( A [,) B
) )  =  if ( A  <  B ,  ( B  -  A ) ,  0 ) )
44 simpl 463 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  ( A  e.  RR  /\  B  e.  RR ) )
45 simpr 467 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  -.  A  <  B )
4644simprd 469 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  B  e.  RR )
4744simpld 465 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  A  e.  RR )
4846, 47lenltd 9812 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  ( B  <_  A  <->  -.  A  <  B ) )
4945, 48mpbird 240 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  B  <_  A )
50 simpr 467 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  B  <_  A )
511ad2antrr 737 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  A  e.  RR* )
523ad2antlr 738 . . . . . . . 8  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  B  e.  RR* )
53 ico0 11716 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A [,) B
)  =  (/)  <->  B  <_  A ) )
5451, 52, 53syl2anc 671 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  ( ( A [,) B )  =  (/) 
<->  B  <_  A )
)
5550, 54mpbird 240 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  ( A [,) B )  =  (/) )
5655fveq2d 5896 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  ( vol `  ( A [,) B
) )  =  ( vol `  (/) ) )
57 vol0 37922 . . . . . 6  |-  ( vol `  (/) )  =  0
5857a1i 11 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  ( vol `  (/) )  =  0
)
5956, 58eqtrd 2496 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  B  <_  A
)  ->  ( vol `  ( A [,) B
) )  =  0 )
6044, 49, 59syl2anc 671 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  ( vol `  ( A [,) B ) )  =  0 )
61 iffalse 3902 . . . 4  |-  ( -.  A  <  B  ->  if ( A  <  B ,  ( B  -  A ) ,  0 )  =  0 )
6261adantl 472 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  if ( A  <  B , 
( B  -  A
) ,  0 )  =  0 )
6360, 62eqtr4d 2499 . 2  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  -.  A  < 
B )  ->  ( vol `  ( A [,) B ) )  =  if ( A  < 
B ,  ( B  -  A ) ,  0 ) )
6443, 63pm2.61dan 805 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( vol `  ( A [,) B ) )  =  if ( A  <  B ,  ( B  -  A ) ,  0 ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    u. cun 3414    i^i cin 3415   (/)c0 3743   ifcif 3893   {csn 3980   class class class wbr 4418   dom cdm 4856   ` cfv 5605  (class class class)co 6320   CCcc 9568   RRcr 9569   0cc0 9570    + caddc 9573   RR*cxr 9705    < clt 9706    <_ cle 9707    - cmin 9891   (,)cioo 11669   [,)cico 11671   volcvol 22470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-of 6563  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-2o 7214  df-oadd 7217  df-er 7394  df-map 7505  df-pm 7506  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fi 7956  df-sup 7987  df-inf 7988  df-oi 8056  df-card 8404  df-cda 8629  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-n0 10904  df-z 10972  df-uz 11194  df-q 11299  df-rp 11337  df-xneg 11443  df-xadd 11444  df-xmul 11445  df-ioo 11673  df-ico 11675  df-icc 11676  df-fz 11820  df-fzo 11953  df-fl 12066  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13217  df-re 13218  df-im 13219  df-sqrt 13353  df-abs 13354  df-clim 13607  df-rlim 13608  df-sum 13808  df-rest 15376  df-topgen 15397  df-psmet 19017  df-xmet 19018  df-met 19019  df-bl 19020  df-mopn 19021  df-top 19976  df-bases 19977  df-topon 19978  df-cmp 20457  df-ovol 22471  df-vol 22473
This theorem is referenced by:  sublevolico  37948  voliooico  37956  volicorecl  38475  hoiprodcl  38476  hoicvrrex  38485  volicon0  38504  hoiprodcl3  38509  volicore  38510  hoidmvcl  38511  hoidmvval0  38516  hoidmv1lelem2  38521  hoidmv1le  38523  hoidmvlelem2  38525  hoidmvlelem3  38526  hoidmvlelem4  38527  hspmbllem1  38555  volico2  38570  ovolval2lem  38572
  Copyright terms: Public domain W3C validator