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 12563 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 class class class wbr 5039 0cc0 10694 < clt 10832 ℝ+crp 12551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-br 5040 df-rp 12552 |
This theorem is referenced by: rpregt0d 12599 ltmulgt11d 12628 ltmulgt12d 12629 gt0divd 12630 ge0divd 12631 lediv12ad 12652 prodge0rd 12658 expgt0 13633 nnesq 13759 bccl2 13854 sqrlem7 14777 sqrtgt0d 14941 iseralt 15213 fsumlt 15327 geomulcvg 15403 eirrlem 15728 sqrt2irrlem 15772 prmind2 16205 4sqlem11 16471 4sqlem12 16472 ssblex 23280 nrginvrcn 23544 mulc1cncf 23756 nmoleub2lem2 23967 itg2mulclem 24598 itggt0 24695 dvgt0 24855 ftc1lem5 24891 aaliou3lem2 25190 abelthlem8 25285 tanord 25381 tanregt0 25382 logccv 25505 cxpcn3lem 25587 jensenlem2 25824 dmlogdmgm 25860 basellem1 25917 sgmnncl 25983 chpdifbndlem2 26389 pntibndlem1 26424 pntibnd 26428 pntlemc 26430 abvcxp 26450 ostth2lem1 26453 ostth2lem3 26470 ostth2 26472 xrge0iifhom 31555 omssubadd 31933 sgnmulrp2 32176 signsply0 32196 sinccvglem 33297 unblimceq0lem 34372 unbdqndv2lem2 34376 knoppndvlem14 34391 taupilem1 35175 poimirlem29 35492 heicant 35498 itggt0cn 35533 ftc1cnnc 35535 bfplem1 35666 rrncmslem 35676 aks4d1p1 39766 irrapxlem4 40291 irrapxlem5 40292 imo72b2lem1 41398 dvdivbd 43082 ioodvbdlimc1lem2 43091 ioodvbdlimc2lem 43093 stoweidlem1 43160 stoweidlem7 43166 stoweidlem11 43170 stoweidlem25 43184 stoweidlem26 43185 stoweidlem34 43193 stoweidlem49 43208 stoweidlem52 43211 stoweidlem60 43219 wallispi 43229 stirlinglem6 43238 stirlinglem11 43243 fourierdlem30 43296 qndenserrnbl 43454 ovnsubaddlem1 43726 hoiqssbllem2 43779 pimrecltpos 43861 smfmullem1 43940 smfmullem2 43941 smfmullem3 43942 |
Copyright terms: Public domain | W3C validator |