![]() |
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
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
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: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |