Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rpgt0 | Structured version Visualization version Unicode version |
Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.) |
Ref | Expression |
---|---|
rpgt0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp 11834 | . 2 | |
2 | 1 | simprbi 480 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wcel 1990 class class class wbr 4653 cr 9935 cc0 9936 clt 10074 crp 11832 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-rp 11833 |
This theorem is referenced by: rpge0 11845 rpgecl 11859 0nrp 11865 rpgt0d 11875 addlelt 11942 0mod 12701 sgnrrp 13831 sqrlem2 13984 sqrlem4 13986 sqrlem6 13988 resqrex 13991 rpsqrtcl 14005 climconst 14274 rlimconst 14275 divrcnv 14584 rprisefaccl 14754 blcntrps 22217 blcntr 22218 stdbdmet 22321 stdbdmopn 22323 prdsxmslem2 22334 metustid 22359 nmoix 22533 metdseq0 22657 lebnumii 22765 itgulm 24162 pilem2 24206 tanregt0 24285 logdmnrp 24387 cxple2 24443 asinneg 24613 asin1 24621 reasinsin 24623 atanbndlem 24652 atanbnd 24653 atan1 24655 rlimcnp 24692 chtrpcl 24901 ppiltx 24903 bposlem8 25016 pntlem3 25298 padicabvcxp 25321 0cnop 28838 0cnfn 28839 rpdp2cl 29589 xdivpnfrp 29641 pnfinf 29737 hgt750lem2 30730 taupilem1 33167 itg2gt0cn 33465 areacirclem1 33500 areacirclem4 33503 prdstotbnd 33593 prdsbnd2 33594 irrapxlem3 37388 neglt 39496 xralrple2 39570 constlimc 39856 0cnv 39974 ioodvbdlimc1lem1 40146 fourierdlem103 40426 fourierdlem104 40427 etransclem18 40469 etransclem46 40497 hoidmvlelem3 40811 |
Copyright terms: Public domain | W3C validator |