Theorem elrpd 9885

Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
elrpd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
elrpd.2	⊢ (𝜑 → 0 < 𝐴)

Assertion

Ref	Expression
elrpd	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Proof of Theorem elrpd

Step	Hyp	Ref	Expression
1		elrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		elrpd.2	. 2 ⊢ (𝜑 → 0 < 𝐴)
3		elrp 9847	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 417	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4082  ℝcr 7994  0cc0 7995   < clt 8177  ℝ⁺crp 9845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-rp 9846

This theorem is referenced by:  mul2lt0rgt0  9952  mul2lt0np  9955  zltaddlt1le  10199  modqval  10541  ltexp2a  10808  leexp2a  10809  expnlbnd2  10882  nn0ltexp2  10926  resqrexlem1arp  11511  resqrexlemp1rp  11512  resqrexlemcalc2  11521  resqrexlemcalc3  11522  resqrexlemgt0  11526  resqrexlemglsq  11528  rpsqrtcl  11547  absrpclap  11567  rpmaxcl  11729  rpmincl  11744  xrminrpcl  11780  xrbdtri  11782  mulcn2  11818  reccn2ap  11819  climge0  11831  divcnv  12003  georeclim  12019  cvgratnnlembern  12029  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratnn  12037  cvgratz  12038  rpefcl  12191  efltim  12204  ef01bndlem  12262  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  bdmopn  15172  mulcncflem  15275  ivthinclemlopn  15304  ivthinclemuopn  15306  dveflem  15394  reeff1olem  15439  pilem3  15451  tanrpcl  15505  cosordlem  15517  rplogcl  15547  logdivlti  15549  cxplt  15584  cxple  15585  rpabscxpbnd  15608  ltexp2  15609  iooref1o  16361