![]() |
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 12211 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2048 class class class wbr 4923 0cc0 10327 < clt 10466 ℝ+crp 12197 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-rab 3091 df-v 3411 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4924 df-rp 12198 |
This theorem is referenced by: rpregt0d 12247 ltmulgt11d 12276 ltmulgt12d 12277 gt0divd 12278 ge0divd 12279 lediv12ad 12300 prodge0rd 12306 expgt0 13270 nnesq 13396 bccl2 13491 sqrlem7 14459 sqrtgt0d 14623 iseralt 14892 fsumlt 15005 geomulcvg 15082 eirrlem 15407 sqrt2irrlem 15451 prmind2 15875 4sqlem11 16137 4sqlem12 16138 ssblex 22731 nrginvrcn 22994 mulc1cncf 23206 nmoleub2lem2 23413 itg2mulclem 24040 itggt0 24135 dvgt0 24294 ftc1lem5 24330 aaliou3lem2 24625 abelthlem8 24720 tanord 24813 tanregt0 24814 logccv 24937 cxpcn3lem 25019 jensenlem2 25257 dmlogdmgm 25293 basellem1 25350 sgmnncl 25416 chpdifbndlem2 25822 pntibndlem1 25857 pntibnd 25861 pntlemc 25863 abvcxp 25883 ostth2lem1 25886 ostth2lem3 25903 ostth2 25905 xrge0iifhom 30781 omssubadd 31160 sgnmulrp2 31404 signsply0 31428 sinccvglem 32375 unblimceq0lem 33305 unbdqndv2lem2 33309 knoppndvlem14 33324 taupilem1 33979 poimirlem29 34310 heicant 34316 itggt0cn 34353 ftc1cnnc 34355 bfplem1 34490 rrncmslem 34500 irrapxlem4 38763 irrapxlem5 38764 imo72b2lem1 39831 dvdivbd 41584 ioodvbdlimc1lem2 41593 ioodvbdlimc2lem 41595 stoweidlem1 41663 stoweidlem7 41669 stoweidlem11 41673 stoweidlem25 41687 stoweidlem26 41688 stoweidlem34 41696 stoweidlem49 41711 stoweidlem52 41714 stoweidlem60 41722 wallispi 41732 stirlinglem6 41741 stirlinglem11 41746 fourierdlem30 41799 qndenserrnbl 41957 ovnsubaddlem1 42229 hoiqssbllem2 42282 pimrecltpos 42364 smfmullem1 42443 smfmullem2 42444 smfmullem3 42445 |
Copyright terms: Public domain | W3C validator |