MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolioo Structured version   Visualization version   GIF version

Theorem ovolioo 24151
Description: The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.)
Assertion
Ref Expression
ovolioo ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵𝐴))

Proof of Theorem ovolioo
StepHypRef Expression
1 ioombl 24148 . . 3 (𝐴(,)𝐵) ∈ dom vol
2 mblvol 24113 . . 3 ((𝐴(,)𝐵) ∈ dom vol → (vol‘(𝐴(,)𝐵)) = (vol*‘(𝐴(,)𝐵)))
31, 2ax-mp 5 . 2 (vol‘(𝐴(,)𝐵)) = (vol*‘(𝐴(,)𝐵))
4 iccmbl 24149 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
5 mblvol 24113 . . . . 5 ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
64, 5syl 17 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
763adant3 1129 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
81a1i 11 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (𝐴(,)𝐵) ∈ dom vol)
9 prssi 4727 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {𝐴, 𝐵} ⊆ ℝ)
1093adant3 1129 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → {𝐴, 𝐵} ⊆ ℝ)
11 prfi 8769 . . . . . . 7 {𝐴, 𝐵} ∈ Fin
12 ovolfi 24077 . . . . . . 7 (({𝐴, 𝐵} ∈ Fin ∧ {𝐴, 𝐵} ⊆ ℝ) → (vol*‘{𝐴, 𝐵}) = 0)
1311, 10, 12sylancr 590 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘{𝐴, 𝐵}) = 0)
14 nulmbl 24118 . . . . . 6 (({𝐴, 𝐵} ⊆ ℝ ∧ (vol*‘{𝐴, 𝐵}) = 0) → {𝐴, 𝐵} ∈ dom vol)
1510, 13, 14syl2anc 587 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → {𝐴, 𝐵} ∈ dom vol)
16 df-pr 4543 . . . . . . . 8 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
1716ineq2i 4161 . . . . . . 7 ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ((𝐴(,)𝐵) ∩ ({𝐴} ∪ {𝐵}))
18 indi 4225 . . . . . . 7 ((𝐴(,)𝐵) ∩ ({𝐴} ∪ {𝐵})) = (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵}))
1917, 18eqtri 2844 . . . . . 6 ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵}))
20 simp1 1133 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → 𝐴 ∈ ℝ)
2120ltnrd 10751 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ¬ 𝐴 < 𝐴)
22 eliooord 12774 . . . . . . . . . . 11 (𝐴 ∈ (𝐴(,)𝐵) → (𝐴 < 𝐴𝐴 < 𝐵))
2322simpld 498 . . . . . . . . . 10 (𝐴 ∈ (𝐴(,)𝐵) → 𝐴 < 𝐴)
2421, 23nsyl 142 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ¬ 𝐴 ∈ (𝐴(,)𝐵))
25 disjsn 4620 . . . . . . . . 9 (((𝐴(,)𝐵) ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ (𝐴(,)𝐵))
2624, 25sylibr 237 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((𝐴(,)𝐵) ∩ {𝐴}) = ∅)
27 simp2 1134 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → 𝐵 ∈ ℝ)
2827ltnrd 10751 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ¬ 𝐵 < 𝐵)
29 eliooord 12774 . . . . . . . . . . 11 (𝐵 ∈ (𝐴(,)𝐵) → (𝐴 < 𝐵𝐵 < 𝐵))
3029simprd 499 . . . . . . . . . 10 (𝐵 ∈ (𝐴(,)𝐵) → 𝐵 < 𝐵)
3128, 30nsyl 142 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ¬ 𝐵 ∈ (𝐴(,)𝐵))
32 disjsn 4620 . . . . . . . . 9 (((𝐴(,)𝐵) ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ (𝐴(,)𝐵))
3331, 32sylibr 237 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((𝐴(,)𝐵) ∩ {𝐵}) = ∅)
3426, 33uneq12d 4116 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵})) = (∅ ∪ ∅))
35 un0 4317 . . . . . . 7 (∅ ∪ ∅) = ∅
3634, 35syl6eq 2872 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (((𝐴(,)𝐵) ∩ {𝐴}) ∪ ((𝐴(,)𝐵) ∩ {𝐵})) = ∅)
3719, 36syl5eq 2868 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅)
38 ioossicc 12801 . . . . . . 7 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
39 iccssre 12797 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
40393adant3 1129 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (𝐴[,]𝐵) ⊆ ℝ)
41 ovolicc 24106 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴))
4227, 20resubcld 11045 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (𝐵𝐴) ∈ ℝ)
4341, 42eqeltrd 2912 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) ∈ ℝ)
44 ovolsscl 24069 . . . . . . 7 (((𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (vol*‘(𝐴[,]𝐵)) ∈ ℝ) → (vol*‘(𝐴(,)𝐵)) ∈ ℝ)
4538, 40, 43, 44mp3an2i 1463 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴(,)𝐵)) ∈ ℝ)
463, 45eqeltrid 2916 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
47 mblvol 24113 . . . . . . . 8 ({𝐴, 𝐵} ∈ dom vol → (vol‘{𝐴, 𝐵}) = (vol*‘{𝐴, 𝐵}))
4815, 47syl 17 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘{𝐴, 𝐵}) = (vol*‘{𝐴, 𝐵}))
4948, 13eqtrd 2856 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘{𝐴, 𝐵}) = 0)
50 0re 10620 . . . . . 6 0 ∈ ℝ
5149, 50eqeltrdi 2920 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘{𝐴, 𝐵}) ∈ ℝ)
52 volun 24128 . . . . 5 ((((𝐴(,)𝐵) ∈ dom vol ∧ {𝐴, 𝐵} ∈ dom vol ∧ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅) ∧ ((vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ (vol‘{𝐴, 𝐵}) ∈ ℝ)) → (vol‘((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵})))
538, 15, 37, 46, 51, 52syl32anc 1375 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) = ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵})))
54 rexr 10664 . . . . . 6 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
55 rexr 10664 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
56 id 22 . . . . . 6 (𝐴𝐵𝐴𝐵)
57 prunioo 12849 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
5854, 55, 56, 57syl3an 1157 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵))
5958fveq2d 6647 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) = (vol‘(𝐴[,]𝐵)))
6049oveq2d 7146 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵})) = ((vol‘(𝐴(,)𝐵)) + 0))
6146recnd 10646 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴(,)𝐵)) ∈ ℂ)
6261addid1d 10817 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((vol‘(𝐴(,)𝐵)) + 0) = (vol‘(𝐴(,)𝐵)))
6360, 62eqtrd 2856 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → ((vol‘(𝐴(,)𝐵)) + (vol‘{𝐴, 𝐵})) = (vol‘(𝐴(,)𝐵)))
6453, 59, 633eqtr3d 2864 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴[,]𝐵)) = (vol‘(𝐴(,)𝐵)))
657, 64, 413eqtr3d 2864 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵𝐴))
663, 65syl5eqr 2870 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  cun 3908  cin 3909  wss 3910  c0 4266  {csn 4540  {cpr 4542   class class class wbr 5039  dom cdm 5528  cfv 6328  (class class class)co 7130  Fincfn 8484  cr 10513  0cc0 10514   + caddc 10517  *cxr 10651   < clt 10652  cle 10653  cmin 10847  (,)cioo 12716  [,]cicc 12719  vol*covol 24045  volcvol 24046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-inf2 9080  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-of 7384  df-om 7556  df-1st 7664  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-2o 8078  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-fi 8851  df-sup 8882  df-inf 8883  df-oi 8950  df-dju 9306  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-n0 11876  df-z 11960  df-uz 12222  df-q 12327  df-rp 12368  df-xneg 12485  df-xadd 12486  df-xmul 12487  df-ioo 12720  df-ico 12722  df-icc 12723  df-fz 12876  df-fzo 13017  df-fl 13145  df-seq 13353  df-exp 13414  df-hash 13675  df-cj 14437  df-re 14438  df-im 14439  df-sqrt 14573  df-abs 14574  df-clim 14824  df-rlim 14825  df-sum 15022  df-rest 16675  df-topgen 16696  df-psmet 20513  df-xmet 20514  df-met 20515  df-bl 20516  df-mopn 20517  df-top 21478  df-topon 21495  df-bases 21530  df-cmp 21971  df-ovol 24047  df-vol 24048
This theorem is referenced by:  volioo  24152  ioovolcl  24153  ovolfs2  24154  ioorcl2  24155  uniioovol  24162  uniioombllem2  24166  uniioombllem3a  24167  uniioombllem4  24169  uniioombllem6  24171  ftc1lem4  24621  itg2gt0cn  34994  ftc1cnnclem  35010  ftc1anclem7  35018
  Copyright terms: Public domain W3C validator