Theorem nnrp 12929

Description: A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)

Assertion

Ref	Expression
nnrp	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Proof of Theorem nnrp

Step	Hyp	Ref	Expression
1		nnre 12164	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12188	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12919	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  0cc0 11038   < clt 11178  ℕcn 12157  ℝ⁺crp 12917

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-rp 12918

This theorem is referenced by:  nnrpd  12959  nn0ledivnn  13032  adddivflid  13750  divfl0  13756  fldivnn0le  13764  zmodcl  13823  zmodfz  13825  zmodid2  13831  m1modnnsub1  13852  addmodid  13854  modifeq2int  13868  modaddmodup  13869  modaddmodlo  13870  modsumfzodifsn  13879  addmodlteq  13881  nnesq  14162  digit2  14171  digit1  14172  bcrpcl  14243  bcval5  14253  lswccatn0lsw  14527  cshw0  14729  cshwmodn  14730  cshwsublen  14731  cshwidxmod  14738  cshwidxmodr  14739  cshwidxm1  14742  cshwidxm  14743  repswcshw  14747  2cshw  14748  cshweqrep  14756  modfsummods  15728  divcnv  15788  supcvg  15791  harmonic  15794  expcnv  15799  rpnnen2lem11  16161  sqrt2irr  16186  dvdsval3  16195  dvdsmodexp  16199  moddvds  16202  divalgmod  16345  flodddiv4  16354  modgcd  16471  divgcdcoprm0  16604  isprm5  16646  isprm6  16653  nnnn0modprm0  16746  pythagtriplem13  16767  fldivp1  16837  prmreclem5  16860  prmreclem6  16861  4sqlem12  16896  modxai  17008  modsubi  17012  smndex1iidm  18838  smndex1n0mnd  18849  mulgmodid  19055  odmodnn0  19481  gexdvds  19525  sylow1lem1  19539  gexexlem  19793  znf1o  21518  met1stc  24477  lmnn  25231  bcthlem5  25296  minveclem3  25397  vitali  25582  ismbf3d  25623  itg2seq  25711  plyeq0lem  26183  elqaalem3  26297  aalioulem6  26313  aaliou  26314  logtayllem  26636  sqrt2cxp2logb9e3  26777  atan1  26906  leibpi  26920  birthdaylem2  26930  dfef2  26949  divsqrtsumlem  26958  emcllem1  26974  emcllem2  26975  emcllem3  26976  emcllem4  26977  emcllem6  26979  zetacvg  26993  lgam1  27042  ppiub  27183  vmalelog  27184  logfacbnd3  27202  logexprlim  27204  bcmono  27256  bclbnd  27259  bposlem1  27263  bposlem7  27269  bposlem8  27270  bposlem9  27271  gausslemma2dlem1a  27344  gausslemma2dlem4  27348  gausslemma2dlem6  27351  m1lgs  27367  2lgslem1a1  27368  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2lgslem4  27385  2lgsoddprmlem2  27388  2sqreultlem  27426  2sqreunnltlem  27429  rplogsumlem1  27463  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0lem1b  27494  dchrisum0lem2a  27496  rplogsum  27506  logdivsum  27512  mulog2sumlem2  27514  logsqvma  27521  logsqvma2  27522  log2sumbnd  27523  selberg2lem  27529  logdivbnd  27535  pntrsumo1  27544  pntrsumbnd  27545  pntibndlem1  27568  pntibndlem2  27570  pntibndlem3  27571  pntlemd  27573  pntlema  27575  pntlemb  27576  pntlemr  27581  pntlemj  27582  pntlemf  27584  pntlemo  27586  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  lnconi  32121  rpdp2cl  32974  rpdp2cl2  32975  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  circum  35890  bccolsum  35955  faclimlem3  35961  faclim  35962  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  mblfinlem3  37910  itg2addnclem2  37923  itg2addnc  37925  3lexlogpow2ineq1  42428  2ap1caineq  42515  pellexlem4  43189  pell1qrgaplem  43230  pellqrex  43236  congrep  43330  acongeq  43340  proot1ex  43553  hashnzfzclim  44678  xrralrecnnle  45741  nnrecrp  45744  xrralrecnnge  45748  iooiinicc  45902  iooiinioc  45916  fprodsubrecnncnvlem  46265  fprodaddrecnncnvlem  46267  wallispilem4  46426  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  stirlinglem1  46432  stirlinglem2  46433  stirlinglem3  46434  stirlinglem4  46435  stirlinglem6  46437  stirlinglem7  46438  stirlinglem10  46441  stirlinglem11  46442  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  stirlingr  46448  dirkertrigeqlem1  46456  hoicvrrex  46914  ovnsubaddlem2  46929  hoiqssbllem3  46982  iinhoiicc  47032  iunhoiioo  47034  vonioolem1  47038  vonioolem2  47039  vonicclem1  47041  vonicclem2  47042  addmodne  47704  submodlt  47710  mod0mul  47716  modn0mul  47717  m1modmmod  47718  difmodm1lt  47719  modlt0b  47723  mod2addne  47724  fsummmodsndifre  47734  mod42tp1mod8  47962  lighneallem2  47966  3exp4mod41  47976  41prothprmlem2  47978  perfectALTVlem2  48082  2exp340mod341  48093  8exp8mod9  48096  nfermltl8rev  48102  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  gpg3kgrtriexlem1  48443  gpg3kgrtriexlem2  48444  nnlog2ge0lt1  48926  blennnelnn  48936  nnpw2blen  48940  blen1b  48948  blennnt2  48949  blennn0e2  48954  dignn0fr  48961  dignn0ldlem  48962  dignnld  48963  dig2nn1st  48965  dig0  48966