Theorem nnrp 13027

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  ℝcr 11098  0cc0 11099   < clt 11242  ℕcn 12232  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-rp 13016

This theorem is referenced by:  nnrpd  13057  nn0ledivnn  13130  adddivflid  13850  divfl0  13856  fldivnn0le  13864  zmodcl  13923  zmodfz  13925  zmodid2  13931  m1modnnsub1  13952  addmodid  13954  modifeq2int  13968  modaddmodup  13969  modaddmodlo  13970  modsumfzodifsn  13979  addmodlteq  13981  nnesq  14262  digit2  14271  digit1  14272  bcrpcl  14343  bcval5  14353  lswccatn0lsw  14628  cshw0  14830  cshwmodn  14831  cshwsublen  14832  cshwidxmod  14839  cshwidxmodr  14840  cshwidxm1  14843  cshwidxm  14844  repswcshw  14848  2cshw  14849  cshweqrep  14857  modfsummods  15844  divcnv  15906  supcvg  15909  harmonic  15912  expcnv  15917  rpnnen2lem11  16279  sqrt2irr  16304  dvdsval3  16313  dvdsmodexp  16317  moddvds  16320  divalgmod  16463  flodddiv4  16472  modgcd  16589  divgcdcoprm0  16722  isprm5  16765  isprm6  16772  nnnn0modprm0  16865  pythagtriplem13  16886  fldivp1  16956  prmreclem5  16979  prmreclem6  16980  4sqlem12  17015  modxai  17127  modsubi  17131  smndex1iidm  18959  smndex1n0mnd  18973  mulgmodid  19178  odmodnn0  19609  gexdvds  19653  sylow1lem1  19667  gexexlem  19921  znf1o  21669  met1stc  24646  lmnn  25390  bcthlem5  25455  minveclem3  25556  vitali  25740  ismbf3d  25781  itg2seq  25869  plyeq0lem  26335  elqaalem3  26450  aalioulem6  26466  aaliou  26467  logtayllem  26789  sqrt2cxp2logb9e3  26929  atan1  27058  leibpi  27072  birthdaylem2  27082  dfef2  27100  divsqrtsumlem  27109  emcllem1  27125  emcllem2  27126  emcllem3  27127  emcllem4  27128  emcllem6  27130  zetacvg  27144  lgam1  27193  ppiub  27333  vmalelog  27334  logfacbnd3  27352  logexprlim  27354  bcmono  27406  bclbnd  27409  bposlem1  27413  bposlem7  27419  bposlem8  27420  bposlem9  27421  gausslemma2dlem1a  27494  gausslemma2dlem4  27498  gausslemma2dlem6  27501  m1lgs  27517  2lgslem1a1  27518  2lgslem3a1  27529  2lgslem3b1  27530  2lgslem3c1  27531  2lgslem3d1  27532  2lgslem4  27535  2lgsoddprmlem2  27538  2sqreultlem  27576  2sqreunnltlem  27579  rplogsumlem1  27613  dchrisumlema  27617  dchrisumlem2  27619  dchrisumlem3  27620  dchrvmasumlem2  27627  dchrvmasumiflem1  27630  dchrisum0lem1b  27644  dchrisum0lem2a  27646  rplogsum  27656  logdivsum  27662  mulog2sumlem2  27664  logsqvma  27671  logsqvma2  27672  log2sumbnd  27673  selberg2lem  27679  logdivbnd  27685  pntrsumo1  27694  pntrsumbnd  27695  pntibndlem1  27718  pntibndlem2  27720  pntibndlem3  27721  pntlemd  27723  pntlema  27725  pntlemb  27726  pntlemr  27731  pntlemj  27732  pntlemf  27734  pntlemo  27736  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  lnconi  32325  rpdp2cl  33141  rpdp2cl2  33142  hgt750lem  34982  hgt750lem2  34983  hgt750leme  34989  circum  36064  bccolsum  36129  faclimlem3  36135  faclim  36136  poimirlem29  38187  poimirlem30  38188  poimirlem31  38189  poimirlem32  38190  mblfinlem3  38197  itg2addnclem2  38210  itg2addnc  38212  3lexlogpow2ineq1  42714  2ap1caineq  42801  pellexlem4  43450  pell1qrgaplem  43491  pellqrex  43497  congrep  43591  acongeq  43601  proot1ex  43814  hashnzfzclim  44923  xrralrecnnle  45989  nnrecrp  45992  xrralrecnnge  45996  iooiinicc  46149  iooiinioc  46163  fprodsubrecnncnvlem  46512  fprodaddrecnncnvlem  46514  wallispilem4  46673  wallispi  46675  wallispi2lem1  46676  wallispi2lem2  46677  stirlinglem1  46679  stirlinglem2  46680  stirlinglem3  46681  stirlinglem4  46682  stirlinglem6  46684  stirlinglem7  46685  stirlinglem10  46688  stirlinglem11  46689  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  stirlingr  46695  dirkertrigeqlem1  46703  hoicvrrex  47161  ovnsubaddlem2  47176  hoiqssbllem3  47229  iinhoiicc  47279  iunhoiioo  47281  vonioolem1  47285  vonioolem2  47286  vonicclem1  47288  vonicclem2  47289  nnmul2  47955  flmrecm1  47968  addmodne  47975  submodlt  47981  mod0mul  47987  modn0mul  47988  m1modmmod  47989  difmodm1lt  47990  modlt0b  47994  mod2addne  47995  fsummmodsndifre  48007  mod42tp1mod8  48242  lighneallem2  48246  3exp4mod41  48256  41prothprmlem2  48258  perfectALTVlem2  48375  2exp340mod341  48386  8exp8mod9  48389  nfermltl8rev  48395  gpgedgvtx0  48714  gpgedgvtx1  48715  gpgvtxedg0  48716  gpgvtxedg1  48717  gpg3kgrtriexlem1  48736  gpg3kgrtriexlem2  48737  nnlog2ge0lt1  49230  blennnelnn  49240  nnpw2blen  49244  blen1b  49252  blennnt2  49253  blennn0e2  49258  dignn0fr  49265  dignn0ldlem  49266  dignnld  49267  dig2nn1st  49269  dig0  49270