Theorem elrpd 9918

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 9880	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 417	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4086  ℝcr 8021  0cc0 8022   < clt 8204  ℝ⁺crp 9878

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-rp 9879

This theorem is referenced by:  mul2lt0rgt0  9985  mul2lt0np  9988  zltaddlt1le  10232  modqval  10576  ltexp2a  10843  leexp2a  10844  expnlbnd2  10917  nn0ltexp2  10961  resqrexlem1arp  11556  resqrexlemp1rp  11557  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemgt0  11571  resqrexlemglsq  11573  rpsqrtcl  11592  absrpclap  11612  rpmaxcl  11774  rpmincl  11789  xrminrpcl  11825  xrbdtri  11827  mulcn2  11863  reccn2ap  11864  climge0  11876  divcnv  12048  georeclim  12064  cvgratnnlembern  12074  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  rpefcl  12236  efltim  12249  ef01bndlem  12307  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  bdmopn  15218  mulcncflem  15321  ivthinclemlopn  15350  ivthinclemuopn  15352  dveflem  15440  reeff1olem  15485  pilem3  15497  tanrpcl  15551  cosordlem  15563  rplogcl  15593  logdivlti  15595  cxplt  15630  cxple  15631  rpabscxpbnd  15654  ltexp2  15655  iooref1o  16574