Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > ovolre | Structured version Unicode version | |
| Description: The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
| Ref | Expression |
|---|---|
| ovolre |
         |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssid 3480 |
. . . 4
 | |
| 2 | ovolcl 22325 |
. . . 4
  | |
| 3 | 1, 2 | ax-mp 5 |
. . 3
|
| 4 | pnfge 11421 |
. . 3
 | |
| 5 | 3, 4 | ax-mp 5 |
. 2
|
| 6 | 0re 9632 |
. . . 4
 | |
| 7 | ovolicopnf 22372 |
. . . 4
 | |
| 8 | 6, 7 | ax-mp 5 |
. . 3
|
| 9 | rge0ssre 11727 |
. . . 4
| |
| 10 | ovolss 22332 |
. . . 4
![/\](wedge.gif "/\"){kind=small} | |
| 11 | 9, 1, 10 | mp2an 676 |
. . 3
|
| 12 | 8, 11 | eqbrtrri 4438 |
. 2
|
| 13 | pnfxr 11401 |
. . 3
| |
| 14 | xrletri3 11440 |
. . 3
| |
| 15 | 3, 13, 14 | mp2an 676 |
. 2
|
| 16 | 5, 12, 15 | mpbir2an 928 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints:
wb 187
wa 370
wceq 1437
wcel 1867
wss 3433
class class class wbr 4417 cfv 5592 (class class class)co 6296
cr 9527
cc0 9528
cpnf 9661
cxr 9663
cle 9665
cico 11626
covol 22307 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-inf2 8137 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-pre-sup 9606 |
| This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-se 4805 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-isom 5601 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-1o 7181 df-oadd 7185 df-er 7362 df-map 7473 df-en 7569 df-dom 7570 df-sdom 7571 df-fin 7572 df-fi 7922 df-sup 7953 df-inf 7954 df-oi 8016 df-card 8363 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-n0 10859 df-z 10927 df-uz 11149 df-q 11254 df-rp 11292 df-xneg 11398 df-xadd 11399 df-xmul 11400 df-ioo 11628 df-ico 11630 df-icc 11631 df-fz 11772 df-fzo 11903 df-seq 12200 df-exp 12259 df-hash 12502 df-cj 13130 df-re 13131 df-im 13132 df-sqrt 13266 df-abs 13267 df-clim 13519 df-sum 13720 df-rest 15273 df-topgen 15294 df-psmet 18890 df-xmet 18891 df-met 18892 df-bl 18893 df-mopn 18894 df-top 19845 df-bases 19846 df-topon 19847 df-cmp 20326 df-ovol 22310 |
| This theorem is referenced by: i1f0rn 22534 ovoliunnfl 31715 voliunnfl 31717 volsupnfl 31718 |
| Copyright terms: Public domain | W3C validator |