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 12389 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 class class class wbr 5057 0cc0 10525 < clt 10663 ℝ+crp 12377 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-rp 12378 |
This theorem is referenced by: rpregt0d 12425 ltmulgt11d 12454 ltmulgt12d 12455 gt0divd 12456 ge0divd 12457 lediv12ad 12478 prodge0rd 12484 expgt0 13450 nnesq 13576 bccl2 13671 sqrlem7 14596 sqrtgt0d 14760 iseralt 15029 fsumlt 15143 geomulcvg 15220 eirrlem 15545 sqrt2irrlem 15589 prmind2 16017 4sqlem11 16279 4sqlem12 16280 ssblex 22965 nrginvrcn 23228 mulc1cncf 23440 nmoleub2lem2 23647 itg2mulclem 24274 itggt0 24369 dvgt0 24528 ftc1lem5 24564 aaliou3lem2 24859 abelthlem8 24954 tanord 25049 tanregt0 25050 logccv 25173 cxpcn3lem 25255 jensenlem2 25492 dmlogdmgm 25528 basellem1 25585 sgmnncl 25651 chpdifbndlem2 26057 pntibndlem1 26092 pntibnd 26096 pntlemc 26098 abvcxp 26118 ostth2lem1 26121 ostth2lem3 26138 ostth2 26140 xrge0iifhom 31079 omssubadd 31457 sgnmulrp2 31700 signsply0 31720 sinccvglem 32812 unblimceq0lem 33742 unbdqndv2lem2 33746 knoppndvlem14 33761 taupilem1 34484 poimirlem29 34802 heicant 34808 itggt0cn 34845 ftc1cnnc 34847 bfplem1 34981 rrncmslem 34991 irrapxlem4 39300 irrapxlem5 39301 imo72b2lem1 40399 dvdivbd 42084 ioodvbdlimc1lem2 42093 ioodvbdlimc2lem 42095 stoweidlem1 42163 stoweidlem7 42169 stoweidlem11 42173 stoweidlem25 42187 stoweidlem26 42188 stoweidlem34 42196 stoweidlem49 42211 stoweidlem52 42214 stoweidlem60 42222 wallispi 42232 stirlinglem6 42241 stirlinglem11 42246 fourierdlem30 42299 qndenserrnbl 42457 ovnsubaddlem1 42729 hoiqssbllem2 42782 pimrecltpos 42864 smfmullem1 42943 smfmullem2 42944 smfmullem3 42945 |
Copyright terms: Public domain | W3C validator |