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 12671

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 12661	. 2 ⊢ (𝐴 ∈ ℝ⁺ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ ℝ⁺ → 0 < 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2108 class class class wbr 5070 ℝcr 10801 0cc0 10802 < clt 10940 ℝ⁺crp 12659

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-br 5071 df-rp 12660

This theorem is referenced by: rpge0 12672 rpgecl 12687 0nrp 12694 rpgt0d 12704 addlelt 12773 0mod 13550 sgnrrp 14730 sqrlem2 14883 sqrlem4 14885 sqrlem6 14887 resqrex 14890 rpsqrtcl 14904 climconst 15180 rlimconst 15181 divrcnv 15492 rprisefaccl 15661 blcntrps 23473 blcntr 23474 stdbdmet 23578 stdbdmopn 23580 prdsxmslem2 23591 metustid 23616 nmoix 23799 metdseq0 23923 lebnumii 24035 itgulm 25472 pilem2 25516 cos02pilt1 25587 tanregt0 25600 logdmnrp 25701 cxple2 25757 asinneg 25941 asin1 25949 reasinsin 25951 atanbndlem 25980 atanbnd 25981 atan1 25983 rlimcnp 26020 chtrpcl 26229 ppiltx 26231 bposlem8 26344 pntlem3 26662 padicabvcxp 26685 0cnop 30242 0cnfn 30243 rpdp2cl 31058 xdivpnfrp 31109 pnfinf 31339 hgt750lem2 32532 taupilem1 35419 itg2gt0cn 35759 areacirclem1 35792 areacirclem4 35795 prdstotbnd 35879 prdsbnd2 35880 aks4d1p1p6 40009 irrapxlem3 40562 neglt 42712 xralrple2 42783 constlimc 43055 0cnv 43173 ioodvbdlimc1lem1 43362 fourierdlem103 43640 fourierdlem104 43641 etransclem18 43683 etransclem46 43711 hoidmvlelem3 44025