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 12514 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | rexrd 10769 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 ℝ*cxr 10752 ℝ+crp 12472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-xr 10757 df-rp 12473 |
This theorem is referenced by: ssblex 23181 metequiv2 23263 metss2lem 23264 methaus 23273 met1stc 23274 met2ndci 23275 metcnp 23294 metcnpi3 23299 metustexhalf 23309 blval2 23315 metuel2 23318 nmoi2 23483 metdcnlem 23588 metdscnlem 23607 metnrmlem2 23612 metnrmlem3 23613 cnheibor 23707 cnllycmp 23708 lebnumlem3 23715 nmoleub2lem 23866 nmhmcn 23872 iscfil2 24018 cfil3i 24021 iscfil3 24025 cfilfcls 24026 iscmet3lem2 24044 caubl 24060 caublcls 24061 relcmpcmet 24070 bcthlem2 24077 bcthlem4 24079 bcthlem5 24080 ellimc3 24631 ftc1a 24789 ulmdvlem1 25147 psercnlem2 25171 psercn 25173 pserdvlem2 25175 pserdv 25176 efopn 25401 logccv 25406 efrlim 25707 lgamucov 25775 ftalem3 25812 logexprlim 25961 pntpbnd1a 26321 pntleme 26344 pntlem3 26345 pntleml 26347 ubthlem1 28805 ubthlem2 28806 tpr2rico 31434 xrmulc1cn 31452 omssubadd 31837 sgnmulrp2 32080 ptrecube 35400 poimirlem29 35429 heicant 35435 ftc1anclem6 35478 ftc1anclem7 35479 sstotbnd2 35555 equivtotbnd 35559 totbndbnd 35570 cntotbnd 35577 heibor1lem 35590 heiborlem3 35594 heiborlem6 35597 heiborlem8 35599 supxrge 42415 infrpge 42428 infleinflem1 42447 stoweid 43146 qndenserrnbl 43378 sge0rpcpnf 43501 sge0xaddlem1 43513 |
Copyright terms: Public domain | W3C validator |