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 11720 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 class class class wbr 4583 0cc0 9815 < clt 9953 ℝ+crp 11708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-rp 11709 |
This theorem is referenced by: rpregt0d 11754 ltmulgt11d 11783 ltmulgt12d 11784 gt0divd 11785 ge0divd 11786 lediv12ad 11807 expgt0 12755 nnesq 12850 bccl2 12972 sqrlem7 13837 sqrtgt0d 13999 iseralt 14263 fsumlt 14373 geomulcvg 14446 eirrlem 14771 sqr2irrlem 14816 prmind2 15236 4sqlem11 15497 4sqlem12 15498 ssblex 22043 nrginvrcn 22306 mulc1cncf 22516 nmoleub2lem2 22724 itg2mulclem 23319 itggt0 23414 dvgt0 23571 ftc1lem5 23607 aaliou3lem2 23902 abelthlem8 23997 tanord 24088 tanregt0 24089 logccv 24209 cxpcn3lem 24288 jensenlem2 24514 dmlogdmgm 24550 basellem1 24607 sgmnncl 24673 chpdifbndlem2 25043 pntibndlem1 25078 pntibnd 25082 pntlemc 25084 abvcxp 25104 ostth2lem1 25107 ostth2lem3 25124 ostth2 25126 xrge0iifhom 29311 omssubadd 29689 sgnmulrp2 29932 signsply0 29954 sinccvglem 30820 unblimceq0lem 31667 unbdqndv2lem2 31671 knoppndvlem14 31686 taupilem1 32344 poimirlem29 32608 heicant 32614 itggt0cn 32652 ftc1cnnc 32654 bfplem1 32791 rrncmslem 32801 irrapxlem4 36407 irrapxlem5 36408 imo72b2lem1 37493 dvdivbd 38813 ioodvbdlimc1lem2 38822 ioodvbdlimc2lem 38824 stoweidlem1 38894 stoweidlem7 38900 stoweidlem11 38904 stoweidlem25 38918 stoweidlem26 38919 stoweidlem34 38927 stoweidlem49 38942 stoweidlem52 38945 stoweidlem60 38953 wallispi 38963 stirlinglem6 38972 stirlinglem11 38977 fourierdlem30 39030 qndenserrnbl 39191 ovnsubaddlem1 39460 hoiqssbllem2 39513 pimrecltpos 39596 smfmullem1 39676 smfmullem2 39677 smfmullem3 39678 |
Copyright terms: Public domain | W3C validator |