Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > ovolre | Structured version Visualization 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 3463 |
. . . 4
 | |
| 2 | ovolcl 22486 |
. . . 4
  | |
| 3 | 1, 2 | ax-mp 5 |
. . 3
|
| 4 | pnfge 11466 |
. . 3
 | |
| 5 | 3, 4 | ax-mp 5 |
. 2
|
| 6 | 0re 9674 |
. . . 4
 | |
| 7 | ovolicopnf 22533 |
. . . 4
 | |
| 8 | 6, 7 | ax-mp 5 |
. . 3
|
| 9 | rge0ssre 11775 |
. . . 4
| |
| 10 | ovolss 22493 |
. . . 4
![/\](wedge.gif "/\"){kind=small} | |
| 11 | 9, 1, 10 | mp2an 683 |
. . 3
|
| 12 | 8, 11 | eqbrtrri 4440 |
. 2
|
| 13 | pnfxr 11446 |
. . 3
| |
| 14 | xrletri3 11485 |
. . 3
| |
| 15 | 3, 13, 14 | mp2an 683 |
. 2
|
| 16 | 5, 12, 15 | mpbir2an 936 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints:
wb 189
wa 375
wceq 1455
wcel 1898
wss 3416
class class class wbr 4418 cfv 5605 (class class class)co 6320
cr 9569
cc0 9570
cpnf 9703
cxr 9705
cle 9707
cico 11671
covol 22468 |
| 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-om 6725 df-1st 6825 df-2nd 6826 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-oadd 7217 df-er 7394 df-map 7505 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-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-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-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 |
| This theorem is referenced by: i1f0rn 22696 ovoliunnfl 32028 voliunnfl 32030 volsupnfl 32031 |
| Copyright terms: Public domain | W3C validator |