Theorem nnrp 13139

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 12349	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12376	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 13129	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11206  0cc0 11207   < clt 11350  ℕcn 12342  ℝ⁺crp 13127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-rp 13128

This theorem is used by:  nnrpd  13169  nn0ledivnn  13242  adddivflid  13965  divfl0  13971  fldivnn0le  13979  zmodcl  14038  zmodfz  14040  zmodid2  14046  m1modnnsub1  14067  addmodid  14069  modifeq2int  14083  modaddmodup  14084  modaddmodlo  14085  modsumfzodifsn  14094  addmodlteq  14096  nnesq  14378  digit2  14387  digit1  14388  bcrpcl  14459  bcval5  14469  lswccatn0lsw  14745  cshw0  14953  cshwmodn  14954  cshwsublen  14955  cshwidxmod  14962  cshwidxmodr  14963  cshwidxm1  14966  cshwidxm  14967  repswcshw  14971  2cshw  14972  cshweqrep  14980  modfsummods  15969  divcnv  16031  supcvg  16034  harmonic  16037  expcnv  16042  rpnnen2lem11  16401  sqrt2irr  16426  dvdsval3  16435  dvdsmodexp  16439  moddvds  16442  divalgmod  16585  flodddiv4  16594  modgcd  16714  divgcdcoprm0  16849  isprm5  16892  isprm6  16899  nnnn0modprm0  16993  pythagtriplem13  17014  fldivp1  17084  prmreclem5  17107  prmreclem6  17108  4sqlem12  17143  modxai  17255  modsubi  17259  smndex1iidm  19106  smndex1n0mnd  19120  mulgmodid  19332  odmodnn0  19763  gexdvds  19807  sylow1lem1  19821  gexexlem  20075  znf1o  21866  met1stc  24849  lmnn  25593  bcthlem5  25658  minveclem3  25759  vitali  25943  ismbf3d  25984  itg2seq  26072  plyeq0lem  26538  elqaalem3  26653  aalioulem6  26673  aaliou  26674  logtayllem  26996  sqrt2cxp2logb9e3  27136  atan1  27265  leibpi  27279  birthdaylem2  27289  dfef2  27307  divsqrtsumlem  27316  emcllem1  27332  emcllem2  27333  emcllem3  27334  emcllem4  27335  emcllem6  27337  zetacvg  27351  lgam1  27400  ppiub  27540  vmalelog  27541  logfacbnd3  27559  logexprlim  27561  bcmono  27613  bclbnd  27616  bposlem1  27620  bposlem7  27626  bposlem8  27627  bposlem9  27628  gausslemma2dlem1a  27701  gausslemma2dlem4  27705  gausslemma2dlem6  27708  m1lgs  27724  2lgslem1a1  27725  2lgslem3a1  27736  2lgslem3b1  27737  2lgslem3c1  27738  2lgslem3d1  27739  2lgslem4  27742  2lgsoddprmlem2  27745  2sqreultlem  27783  2sqreunnltlem  27786  rplogsumlem1  27820  dchrisumlema  27824  dchrisumlem2  27826  dchrisumlem3  27827  dchrvmasumlem2  27834  dchrvmasumiflem1  27837  dchrisum0lem1b  27851  dchrisum0lem2a  27853  rplogsum  27863  logdivsum  27869  mulog2sumlem2  27871  logsqvma  27878  logsqvma2  27879  log2sumbnd  27880  selberg2lem  27886  logdivbnd  27892  pntrsumo1  27901  pntrsumbnd  27902  pntibndlem1  27925  pntibndlem2  27927  pntibndlem3  27928  pntlemd  27930  pntlema  27932  pntlemb  27933  pntlemr  27938  pntlemj  27939  pntlemf  27941  pntlemo  27943  crctcshwlkn0lem5  30412  crctcshwlkn0lem6  30413  lnconi  32644  rpdp2cl  33498  rpdp2cl2  33499  hgt750lem  35330  hgt750lem2  35331  hgt750leme  35337  circum  36529  bccolsum  36600  faclimlem3  36606  faclim  36607  poimirlem29  38676  poimirlem30  38677  poimirlem31  38678  poimirlem32  38679  mblfinlem3  38686  itg2addnclem2  38699  itg2addnc  38701  3lexlogpow2ineq1  43217  2ap1caineq  43304  pellexlem4  43948  pell1qrgaplem  43989  pellqrex  43995  congrep  44089  acongeq  44099  proot1ex  44307  hashnzfzclim  45415  xrralrecnnle  46502  nnrecrp  46505  xrralrecnnge  46509  iooiinicc  46662  iooiinioc  46676  fprodsubrecnncnvlem  47025  fprodaddrecnncnvlem  47027  wallispilem4  47186  wallispi  47188  wallispi2lem1  47189  wallispi2lem2  47190  stirlinglem1  47192  stirlinglem2  47193  stirlinglem3  47194  stirlinglem4  47195  stirlinglem6  47197  stirlinglem7  47198  stirlinglem10  47201  stirlinglem11  47202  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  stirlingr  47208  dirkertrigeqlem1  47216  hoicvrrex  47674  ovnsubaddlem2  47689  hoiqssbllem3  47742  iinhoiicc  47792  iunhoiioo  47794  vonioolem1  47798  vonioolem2  47799  vonicclem1  47801  vonicclem2  47802  nnmul2  48508  flmrecm1  48521  addmodne  48528  submodlt  48534  mod0mul  48540  modn0mul  48541  m1modmmod  48542  difmodm1lt  48543  modlt0b  48547  mod2addne  48548  fsummmodsndifre  48560  mod42tp1mod8  48795  lighneallem2  48799  3exp4mod41  48809  41prothprmlem2  48811  perfectALTVlem2  48928  2exp340mod341  48939  8exp8mod9  48942  nfermltl8rev  48948  gpgedgvtx0  49267  gpgedgvtx1  49268  gpgvtxedg0  49269  gpgvtxedg1  49270  gpg3kgrtriexlem1  49289  gpg3kgrtriexlem2  49290  nnlog2ge0lt1  49786  blennnelnn  49796  nnpw2blen  49800  blen1b  49808  blennnt2  49809  blennn0e2  49814  dignn0fr  49821  dignn0ldlem  49822  dignnld  49823  dig2nn1st  49825  dig0  49826