![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpgt0d | Structured version Visualization version GIF version |
Description: A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
rpred.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
Ref | Expression |
---|---|
rpgt0d | ⊢ (𝜑 → 0 < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpred.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+) | |
2 | rpgt0 12983 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 class class class wbr 5138 0cc0 11106 < clt 11245 ℝ+crp 12971 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-br 5139 df-rp 12972 |
This theorem is referenced by: rpregt0d 13019 ltmulgt11d 13048 ltmulgt12d 13049 gt0divd 13050 ge0divd 13051 lediv12ad 13072 prodge0rd 13078 expgt0 14058 nnesq 14187 bccl2 14280 01sqrexlem7 15192 sqrtgt0d 15356 iseralt 15628 fsumlt 15743 geomulcvg 15819 eirrlem 16144 sqrt2irrlem 16188 prmind2 16619 4sqlem11 16887 4sqlem12 16888 ssblex 24256 nrginvrcn 24531 mulc1cncf 24747 nmoleub2lem2 24965 itg2mulclem 25598 itggt0 25695 dvgt0 25859 ftc1lem5 25897 aaliou3lem2 26197 abelthlem8 26293 tanord 26389 tanregt0 26390 logccv 26513 cxpgt0d 26588 cxpcn3lem 26598 jensenlem2 26836 dmlogdmgm 26872 basellem1 26929 sgmnncl 26995 chpdifbndlem2 27403 pntibndlem1 27438 pntibnd 27442 pntlemc 27444 abvcxp 27464 ostth2lem1 27467 ostth2lem3 27484 ostth2 27486 xrge0iifhom 33406 omssubadd 33788 sgnmulrp2 34031 signsply0 34051 sinccvglem 35146 unblimceq0lem 35872 unbdqndv2lem2 35876 knoppndvlem14 35891 taupilem1 36692 poimirlem29 37007 heicant 37013 itggt0cn 37048 ftc1cnnc 37050 bfplem1 37180 rrncmslem 37190 aks4d1p1 41434 irrapxlem4 42052 irrapxlem5 42053 imo72b2lem1 43410 dvdivbd 45124 ioodvbdlimc1lem2 45133 ioodvbdlimc2lem 45135 stoweidlem1 45202 stoweidlem7 45208 stoweidlem11 45212 stoweidlem25 45226 stoweidlem26 45227 stoweidlem34 45235 stoweidlem49 45250 stoweidlem52 45253 stoweidlem60 45261 wallispi 45271 stirlinglem6 45280 stirlinglem11 45285 fourierdlem30 45338 qndenserrnbl 45496 ovnsubaddlem1 45771 hoiqssbllem2 45824 pimrecltpos 45909 smfmullem1 45992 smfmullem2 45993 smfmullem3 45994 |
Copyright terms: Public domain | W3C validator |