![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpgt0 | Structured version Visualization version GIF version |
Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.) |
Ref | Expression |
---|---|
rpgt0 | ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp 12972 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
2 | 1 | simprbi 498 | 1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 class class class wbr 5147 ℝcr 11105 0cc0 11106 < clt 11244 ℝ+crp 12970 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-rp 12971 |
This theorem is referenced by: rpge0 12983 rpgecl 12998 0nrp 13005 rpgt0d 13015 addlelt 13084 0mod 13863 sgnrrp 15034 01sqrexlem2 15186 01sqrexlem4 15188 01sqrexlem6 15190 resqrex 15193 rpsqrtcl 15207 climconst 15483 rlimconst 15484 divrcnv 15794 rprisefaccl 15963 blcntrps 23900 blcntr 23901 stdbdmet 24007 stdbdmopn 24009 prdsxmslem2 24020 metustid 24045 nmoix 24228 metdseq0 24352 lebnumii 24464 itgulm 25902 pilem2 25946 cos02pilt1 26017 tanregt0 26030 logdmnrp 26131 cxple2 26187 asinneg 26371 asin1 26379 reasinsin 26381 atanbndlem 26410 atanbnd 26411 atan1 26413 rlimcnp 26450 chtrpcl 26659 ppiltx 26661 bposlem8 26774 pntlem3 27092 padicabvcxp 27115 0cnop 31210 0cnfn 31211 rpdp2cl 32026 xdivpnfrp 32077 pnfinf 32307 hgt750lem2 33602 taupilem1 36140 itg2gt0cn 36481 areacirclem1 36514 areacirclem4 36517 prdstotbnd 36600 prdsbnd2 36601 aks4d1p1p6 40876 irrapxlem3 41495 neglt 43929 xralrple2 43999 constlimc 44275 0cnv 44393 ioodvbdlimc1lem1 44582 fourierdlem103 44860 fourierdlem104 44861 etransclem18 44903 etransclem46 44931 hoidmvlelem3 45248 |
Copyright terms: Public domain | W3C validator |