![]() |
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 11332 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 470 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 df-rp 11331 |
This theorem is referenced by: rpge0 11342 rpgecl 11356 0nrp 11362 rpgt0d 11372 0mod 12159 sgnrrp 13202 sqrlem2 13355 sqrlem4 13357 sqrlem6 13359 resqrex 13362 rpsqrtcl 13376 climconst 13655 rlimconst 13656 divrcnv 13958 rprisefaccl 14124 blcntrps 21475 blcntr 21476 stdbdmet 21579 stdbdmopn 21581 prdsxmslem2 21592 metustid 21617 nmoix 21782 nmoixOLD 21798 metdseq0 21919 metdseq0OLD 21934 lebnumii 22045 itgulm 23411 pilem2 23455 pilem2OLD 23456 tanregt0 23536 logdmnrp 23634 cxple2 23690 asinneg 23860 asin1 23868 reasinsin 23870 atanbndlem 23899 atanbnd 23900 atan1 23902 rlimcnp 23939 chtrpcl 24150 ppiltx 24152 bposlem8 24267 pntlem3 24495 padicabvcxp 24518 0cnop 27680 0cnfn 27681 xdivpnfrp 28450 pnfinf 28548 taupilem1 31766 itg2gt0cn 32041 areacirclem1 32076 areacirclem4 32079 prdstotbnd 32170 prdsbnd2 32171 irrapxlem3 35712 neglt 37531 xralrple2 37614 constlimc 37741 ioodvbdlimc1lem1 37840 ioodvbdlimc1lem1OLD 37842 fourierdlem103 38110 fourierdlem104 38111 etransclem18 38154 etransclem46 38182 hoidmvlelem3 38456 |
Copyright terms: Public domain | W3C validator |