![]() |
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 11872 | . 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
2 | 1 | simprbi 479 | 1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 class class class wbr 4685 ℝcr 9973 0cc0 9974 < clt 10112 ℝ+crp 11870 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-rp 11871 |
This theorem is referenced by: rpge0 11883 rpgecl 11897 0nrp 11903 rpgt0d 11913 addlelt 11980 0mod 12741 sgnrrp 13875 sqrlem2 14028 sqrlem4 14030 sqrlem6 14032 resqrex 14035 rpsqrtcl 14049 climconst 14318 rlimconst 14319 divrcnv 14628 rprisefaccl 14798 blcntrps 22264 blcntr 22265 stdbdmet 22368 stdbdmopn 22370 prdsxmslem2 22381 metustid 22406 nmoix 22580 metdseq0 22704 lebnumii 22812 itgulm 24207 pilem2 24251 tanregt0 24330 logdmnrp 24432 cxple2 24488 asinneg 24658 asin1 24666 reasinsin 24668 atanbndlem 24697 atanbnd 24698 atan1 24700 rlimcnp 24737 chtrpcl 24946 ppiltx 24948 bposlem8 25061 pntlem3 25343 padicabvcxp 25366 0cnop 28966 0cnfn 28967 rpdp2cl 29717 xdivpnfrp 29769 pnfinf 29865 hgt750lem2 30858 taupilem1 33297 itg2gt0cn 33595 areacirclem1 33630 areacirclem4 33633 prdstotbnd 33723 prdsbnd2 33724 irrapxlem3 37705 neglt 39810 xralrple2 39883 constlimc 40174 0cnv 40292 ioodvbdlimc1lem1 40464 fourierdlem103 40744 fourierdlem104 40745 etransclem18 40787 etransclem46 40815 hoidmvlelem3 41132 |
Copyright terms: Public domain | W3C validator |