rpgt0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rpgt0		Structured version Visualization version GIF version

Theorem rpgt0 12455

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

**Assertion**
Ref	Expression
rpgt0	⊢ (𝐴 ∈ ℝ⁺ → 0 < 𝐴)

**Proof of Theorem rpgt0**
Step	Hyp	Ref	Expression
1		elrp 12445	. 2 ⊢ (𝐴 ∈ ℝ⁺ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 500	1 ⊢ (𝐴 ∈ ℝ⁺ → 0 < 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2111 class class class wbr 5036 ℝcr 10587 0cc0 10588 < clt 10726 ℝ⁺crp 12443

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-rab 3079 df-v 3411 df-un 3865 df-sn 4526 df-pr 4528 df-op 4532 df-br 5037 df-rp 12444

This theorem is referenced by: rpge0 12456 rpgecl 12471 0nrp 12478 rpgt0d 12488 addlelt 12557 0mod 13332 sgnrrp 14511 sqrlem2 14664 sqrlem4 14666 sqrlem6 14668 resqrex 14671 rpsqrtcl 14685 climconst 14961 rlimconst 14962 divrcnv 15268 rprisefaccl 15438 blcntrps 23127 blcntr 23128 stdbdmet 23231 stdbdmopn 23233 prdsxmslem2 23244 metustid 23269 nmoix 23444 metdseq0 23568 lebnumii 23680 itgulm 25115 pilem2 25159 cos02pilt1 25230 tanregt0 25243 logdmnrp 25344 cxple2 25400 asinneg 25584 asin1 25592 reasinsin 25594 atanbndlem 25623 atanbnd 25624 atan1 25626 rlimcnp 25663 chtrpcl 25872 ppiltx 25874 bposlem8 25987 pntlem3 26305 padicabvcxp 26328 0cnop 29874 0cnfn 29875 rpdp2cl 30692 xdivpnfrp 30743 pnfinf 30975 hgt750lem2 32163 taupilem1 35049 itg2gt0cn 35426 areacirclem1 35459 areacirclem4 35462 prdstotbnd 35546 prdsbnd2 35547 aks4d1p1p6 39673 irrapxlem3 40173 neglt 42318 xralrple2 42389 constlimc 42667 0cnv 42785 ioodvbdlimc1lem1 42974 fourierdlem103 43252 fourierdlem104 43253 etransclem18 43295 etransclem46 43323 hoidmvlelem3 43637