Theorem nnrp 12981

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 12215	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12239	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12972	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5147  ℝcr 11105  0cc0 11106   < clt 11244  ℕcn 12208  ℝ⁺crp 12970

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-rp 12971

This theorem is referenced by:  nnrpd  13010  nn0ledivnn  13083  adddivflid  13779  divfl0  13785  fldivnn0le  13793  zmodcl  13852  zmodfz  13854  zmodid2  13860  m1modnnsub1  13878  addmodid  13880  modifeq2int  13894  modaddmodup  13895  modaddmodlo  13896  modsumfzodifsn  13905  addmodlteq  13907  nnesq  14186  digit2  14195  digit1  14196  bcrpcl  14264  bcval5  14274  lswccatn0lsw  14537  cshw0  14740  cshwmodn  14741  cshwsublen  14742  cshwidxmod  14749  cshwidxmodr  14750  cshwidxm1  14753  cshwidxm  14754  repswcshw  14758  2cshw  14759  cshweqrep  14767  modfsummods  15735  divcnv  15795  supcvg  15798  harmonic  15801  expcnv  15806  rpnnen2lem11  16163  sqrt2irr  16188  dvdsval3  16197  dvdsmodexp  16201  moddvds  16204  divalgmod  16345  flodddiv4  16352  modgcd  16470  divgcdcoprm0  16598  isprm5  16640  isprm6  16647  nnnn0modprm0  16735  pythagtriplem13  16756  fldivp1  16826  prmreclem5  16849  prmreclem6  16850  4sqlem12  16885  modxai  16997  modsubi  17001  smndex1iidm  18778  smndex1n0mnd  18789  mulgmodid  18987  odmodnn0  19402  gexdvds  19446  sylow1lem1  19460  gexexlem  19714  znf1o  21098  met1stc  24021  lmnn  24771  bcthlem5  24836  minveclem3  24937  vitali  25121  ismbf3d  25162  itg2seq  25251  plyeq0lem  25715  elqaalem3  25825  aalioulem6  25841  aaliou  25842  logtayllem  26158  sqrt2cxp2logb9e3  26293  atan1  26422  leibpi  26436  birthdaylem2  26446  dfef2  26464  divsqrtsumlem  26473  emcllem1  26489  emcllem2  26490  emcllem3  26491  emcllem4  26492  emcllem6  26494  zetacvg  26508  lgam1  26557  ppiub  26696  vmalelog  26697  logfacbnd3  26715  logexprlim  26717  bcmono  26769  bclbnd  26772  bposlem1  26776  bposlem7  26782  bposlem8  26783  bposlem9  26784  gausslemma2dlem1a  26857  gausslemma2dlem4  26861  gausslemma2dlem6  26864  m1lgs  26880  2lgslem1a1  26881  2lgslem3a1  26892  2lgslem3b1  26893  2lgslem3c1  26894  2lgslem3d1  26895  2lgslem4  26898  2lgsoddprmlem2  26901  2sqreultlem  26939  2sqreunnltlem  26942  rplogsumlem1  26976  dchrisumlema  26980  dchrisumlem2  26982  dchrisumlem3  26983  dchrvmasumlem2  26990  dchrvmasumiflem1  26993  dchrisum0lem1b  27007  dchrisum0lem2a  27009  rplogsum  27019  logdivsum  27025  mulog2sumlem2  27027  logsqvma  27034  logsqvma2  27035  log2sumbnd  27036  selberg2lem  27042  logdivbnd  27048  pntrsumo1  27057  pntrsumbnd  27058  pntibndlem1  27081  pntibndlem2  27083  pntibndlem3  27084  pntlemd  27086  pntlema  27088  pntlemb  27089  pntlemr  27094  pntlemj  27095  pntlemf  27097  pntlemo  27099  crctcshwlkn0lem5  29057  crctcshwlkn0lem6  29058  lnconi  31273  rpdp2cl  32035  rpdp2cl2  32036  hgt750lem  33651  hgt750lem2  33652  hgt750leme  33658  circum  34647  bccolsum  34697  faclimlem3  34703  faclim  34704  poimirlem29  36505  poimirlem30  36506  poimirlem31  36507  poimirlem32  36508  mblfinlem3  36515  itg2addnclem2  36528  itg2addnc  36530  3lexlogpow2ineq1  40911  2ap1caineq  40949  pellexlem4  41555  pell1qrgaplem  41596  pellqrex  41602  congrep  41697  acongeq  41707  proot1ex  41928  hashnzfzclim  43066  xrralrecnnle  44079  nnrecrp  44082  xrralrecnnge  44086  iooiinicc  44241  iooiinioc  44255  fprodsubrecnncnvlem  44609  fprodaddrecnncnvlem  44611  wallispilem4  44770  wallispi  44772  wallispi2lem1  44773  wallispi2lem2  44774  stirlinglem1  44776  stirlinglem2  44777  stirlinglem3  44778  stirlinglem4  44779  stirlinglem6  44781  stirlinglem7  44782  stirlinglem10  44785  stirlinglem11  44786  stirlinglem13  44788  stirlinglem14  44789  stirlinglem15  44790  stirlingr  44792  dirkertrigeqlem1  44800  hoicvrrex  45258  ovnsubaddlem2  45273  hoiqssbllem3  45326  iinhoiicc  45376  iunhoiioo  45378  vonioolem1  45382  vonioolem2  45383  vonicclem1  45385  vonicclem2  45386  preimageiingt  45422  preimaleiinlt  45423  fsummmodsndifre  46028  mod42tp1mod8  46256  lighneallem2  46260  3exp4mod41  46270  41prothprmlem2  46272  perfectALTVlem2  46376  2exp340mod341  46387  8exp8mod9  46390  nfermltl8rev  46396  mod0mul  47158  modn0mul  47159  m1modmmod  47160  difmodm1lt  47161  nnlog2ge0lt1  47205  blennnelnn  47215  nnpw2blen  47219  blen1b  47227  blennnt2  47228  blennn0e2  47233  dignn0fr  47240  dignn0ldlem  47241  dignnld  47242  dig2nn1st  47244  dig0  47245