![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpxrd | Structured version Visualization version Unicode version |
Description: A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rpred.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
rpxrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpred.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | rpred 11369 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rexrd 9715 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-rab 2757 df-v 3058 df-un 3420 df-in 3422 df-ss 3429 df-xr 9704 df-rp 11331 |
This theorem is referenced by: ssblex 21491 metequiv2 21573 metss2lem 21574 methaus 21583 met1stc 21584 met2ndci 21585 metcnp 21604 metcnpi3 21609 metustexhalf 21619 blval2 21625 metuel2 21628 nmoi2 21783 nmoi2OLD 21799 metdcnlem 21902 metdscnlem 21920 metnrmlem2 21925 metnrmlem3 21926 metdscnlemOLD 21935 metnrmlem2OLD 21940 metnrmlem3OLD 21941 cnheibor 22031 cnllycmp 22032 lebnumlem3 22039 lebnumlem3OLD 22042 nmoleub2lem 22176 nmhmcn 22182 iscfil2 22284 cfil3i 22287 iscfil3 22291 iscmet3lem2 22310 caubl 22325 caublcls 22326 relcmpcmet 22334 bcthlem2 22341 bcthlem4 22343 bcthlem5 22344 ellimc3 22882 ftc1a 23037 ulmdvlem1 23403 psercnlem2 23427 psercn 23429 pserdvlem2 23431 pserdv 23432 efopn 23651 logccv 23656 efrlim 23943 lgamucov 24011 ftalem3 24047 logexprlim 24201 pntpbnd1a 24471 pntleme 24494 pntlem3 24495 pntleml 24497 ubthlem1 26560 ubthlem2 26561 tpr2rico 28766 xrmulc1cn 28784 omssubadd 29176 omssubaddOLD 29180 sgnmulrp2 29462 ptrecube 31984 poimirlem29 32013 heicant 32019 ftc1anclem6 32066 ftc1anclem7 32067 sstotbnd2 32150 equivtotbnd 32154 totbndbnd 32165 cntotbnd 32172 heibor1lem 32185 heiborlem3 32189 heiborlem6 32192 heiborlem8 32194 supxrge 37598 infrpge 37611 stoweid 37962 qndenserrnbl 38201 sge0rpcpnf 38300 sge0xaddlem1 38312 |
Copyright terms: Public domain | W3C validator |