Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rpxrd | Structured version Visualization version GIF 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 12772 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | rexrd 11025 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ℝ*cxr 11008 ℝ+crp 12730 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-un 3892 df-in 3894 df-ss 3904 df-xr 11013 df-rp 12731 |
This theorem is referenced by: ssblex 23581 metequiv2 23666 metss2lem 23667 methaus 23676 met1stc 23677 met2ndci 23678 metcnp 23697 metcnpi3 23702 metustexhalf 23712 blval2 23718 metuel2 23721 nmoi2 23894 metdcnlem 23999 metdscnlem 24018 metnrmlem2 24023 metnrmlem3 24024 cnheibor 24118 cnllycmp 24119 lebnumlem3 24126 nmoleub2lem 24277 nmhmcn 24283 iscfil2 24430 cfil3i 24433 iscfil3 24437 cfilfcls 24438 iscmet3lem2 24456 caubl 24472 caublcls 24473 relcmpcmet 24482 bcthlem2 24489 bcthlem4 24491 bcthlem5 24492 ellimc3 25043 ftc1a 25201 ulmdvlem1 25559 psercnlem2 25583 psercn 25585 pserdvlem2 25587 pserdv 25588 efopn 25813 logccv 25818 efrlim 26119 lgamucov 26187 ftalem3 26224 logexprlim 26373 pntpbnd1a 26733 pntleme 26756 pntlem3 26757 pntleml 26759 ubthlem1 29232 ubthlem2 29233 tpr2rico 31862 xrmulc1cn 31880 omssubadd 32267 sgnmulrp2 32510 ptrecube 35777 poimirlem29 35806 heicant 35812 ftc1anclem6 35855 ftc1anclem7 35856 sstotbnd2 35932 equivtotbnd 35936 totbndbnd 35947 cntotbnd 35954 heibor1lem 35967 heiborlem3 35971 heiborlem6 35974 heiborlem8 35976 supxrge 42877 infrpge 42890 infleinflem1 42909 stoweid 43604 qndenserrnbl 43836 sge0rpcpnf 43959 sge0xaddlem1 43971 |
Copyright terms: Public domain | W3C validator |