| 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 13047 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 0 < 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 class class class wbr 5143 0cc0 11155 < clt 11295 ℝ+crp 13034 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-rp 13035 |
| This theorem is referenced by: rpregt0d 13083 ltmulgt11d 13112 ltmulgt12d 13113 gt0divd 13114 ge0divd 13115 lediv12ad 13136 prodge0rd 13142 expgt0 14136 nnesq 14266 bccl2 14362 01sqrexlem7 15287 sqrtgt0d 15451 iseralt 15721 fsumlt 15836 geomulcvg 15912 eirrlem 16240 sqrt2irrlem 16284 prmind2 16722 4sqlem11 16993 4sqlem12 16994 ssblex 24438 nrginvrcn 24713 mulc1cncf 24931 nmoleub2lem2 25149 itg2mulclem 25781 itggt0 25879 dvgt0 26043 ftc1lem5 26081 aaliou3lem2 26385 abelthlem8 26483 tanord 26580 tanregt0 26581 logccv 26705 cxpgt0d 26780 cxpcn3lem 26790 jensenlem2 27031 dmlogdmgm 27067 basellem1 27124 sgmnncl 27190 chpdifbndlem2 27598 pntibndlem1 27633 pntibnd 27637 pntlemc 27639 abvcxp 27659 ostth2lem1 27662 ostth2lem3 27679 ostth2 27681 xrge0iifhom 33936 omssubadd 34302 sgnmulrp2 34546 signsply0 34566 sinccvglem 35677 unblimceq0lem 36507 unbdqndv2lem2 36511 knoppndvlem14 36526 taupilem1 37322 poimirlem29 37656 heicant 37662 itggt0cn 37697 ftc1cnnc 37699 bfplem1 37829 rrncmslem 37839 aks4d1p1 42077 aks6d1c2 42131 irrapxlem4 42836 irrapxlem5 42837 imo72b2lem1 44182 dvdivbd 45938 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 stoweidlem1 46016 stoweidlem7 46022 stoweidlem11 46026 stoweidlem25 46040 stoweidlem26 46041 stoweidlem34 46049 stoweidlem49 46064 stoweidlem52 46067 stoweidlem60 46075 wallispi 46085 stirlinglem6 46094 stirlinglem11 46099 fourierdlem30 46152 qndenserrnbl 46310 ovnsubaddlem1 46585 hoiqssbllem2 46638 pimrecltpos 46723 smfmullem1 46806 smfmullem2 46807 smfmullem3 46808 |
| Copyright terms: Public domain | W3C validator |