Theorem nnred 12172

Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 12161	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3933	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℕcn 12157

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-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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-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-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158

This theorem is referenced by:  nnne0  12191  uzwo3  12868  modmulnn  13821  bernneq3  14166  expmulnbnd  14170  expnngt1b  14177  facwordi  14224  faclbnd  14225  faclbnd2  14226  faclbnd3  14227  faclbnd5  14233  faclbnd6  14234  facubnd  14235  facavg  14236  bcp1nk  14252  hashf1  14392  swrds2  14875  isercolllem1  15600  isercoll  15603  o1fsum  15748  climcndslem1  15784  climcndslem2  15785  climcnds  15786  eftabs  16010  efcllem  16012  ege2le3  16025  efcj  16027  eftlub  16046  eflegeo  16058  eirrlem  16141  fzm1ndvds  16261  nno  16321  nnoddm1d2  16325  bitsfzolem  16373  bitsfzo  16374  bitsinv1lem  16380  sadcaddlem  16396  smueqlem  16429  bezoutlem3  16480  bezoutlem4  16481  sqgcd  16501  nn0expgcd  16503  lcmgcdlem  16545  lcmf  16572  prmind2  16624  coprm  16650  prmfac1  16659  prmndvdsfaclt  16664  divdenle  16688  qnumgt0  16689  zsqrtelqelz  16697  hashdvds  16714  eulerthlem2  16721  odzdvds  16735  vfermltl  16741  modprm0  16745  pythagtriplem11  16765  pythagtriplem13  16767  pythagtriplem19  16773  pclem  16778  pcpre1  16782  pcidlem  16812  dvdsprmpweqle  16826  pcadd  16829  pcmpt  16832  pcmpt2  16833  pcfaclem  16838  pcfac  16839  qexpz  16841  pockthlem  16845  pockthg  16846  prmreclem1  16856  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  1arithlem4  16866  1arith  16867  4sqlem5  16882  4sqlem6  16883  4sqlem10  16887  mul4sqlem  16893  4sqlem11  16895  4sqlem12  16896  4sqlem13  16897  4sqlem14  16898  4sqlem15  16899  4sqlem16  16900  4sqlem17  16901  vdwlem1  16921  vdwlem3  16923  vdwlem6  16926  vdwlem9  16929  vdwlem10  16930  vdwlem12  16932  vdwnnlem3  16937  ramub1lem1  16966  prmolefac  16986  prmgaplem4  16994  prmgaplem5  16995  prmgaplem6  16996  prmgaplem8  16998  2expltfac  17032  cshwshashnsame  17043  setsstruct2  17113  chnub  18557  psgnunilem4  19438  mndodconglem  19482  oddvds  19488  sylow1lem1  19539  sylow1lem5  19543  fislw  19566  efgredlem  19688  gexexlem  19793  zringlpirlem3  21431  prmirredlem  21439  fvmptnn04if  22805  fvmptnn04ifb  22807  fvmptnn04ifc  22808  fvmptnn04ifd  22809  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  lebnumii  24933  lmnn  25231  ovolunlem1a  25465  ovoliunlem1  25471  ovolicc2lem3  25488  ovolicc2lem4  25489  iundisj  25517  voliunlem1  25519  uniioombllem3  25554  dyadf  25560  dyadovol  25562  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  vitalilem4  25580  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2gt0  25729  itg2cnlem2  25731  dgreq0  26239  dgrco  26249  elqaalem2  26296  aaliou3lem2  26319  aaliou3lem8  26321  aaliou3lem9  26326  rtprmirr  26738  leibpi  26920  log2tlbnd  26923  birthdaylem3  26931  amgm  26969  emcllem2  26975  harmonicbnd4  26989  lgamgulmlem1  27007  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamucov  27016  lgamcvg2  27033  wilthlem1  27046  ftalem5  27055  basellem1  27059  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  basellem6  27064  basellem8  27066  chtge0  27090  chtwordi  27134  vma1  27144  dvdsflf1o  27165  dvdsflsumcom  27166  fsumfldivdiaglem  27167  sgmmul  27180  chtublem  27190  fsumvma2  27193  logfac2  27196  chpchtsum  27198  chpub  27199  logfaclbnd  27201  logexprlim  27204  mersenne  27206  perfectlem2  27209  dchrelbas4  27222  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem7  27269  bposlem9  27271  lgslem1  27276  lgsval2lem  27286  lgsdirprm  27310  lgsdir  27311  lgsne0  27314  lgsqrlem2  27326  gausslemma2dlem0h  27342  gausslemma2dlem0i  27343  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgseisen  27358  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  2sqlem3  27399  2sqlem8  27405  2sqblem  27410  2sqmod  27415  chebbnd1lem1  27448  chebbnd1lem3  27450  chtppilimlem1  27452  rplogsumlem1  27463  rplogsumlem2  27464  dchrisum0lem1a  27465  rpvmasumlem  27466  dchrisumlema  27467  dchrisumlem1  27468  dchrisumlem2  27469  dchrisumlem3  27470  dchrvmasumiflem1  27480  dchrisum0flblem2  27488  dchrisum0re  27492  dchrisum0lem1b  27494  dchrisum0lem1  27495  dirith2  27507  selbergb  27528  selberg2lem  27529  logdivbnd  27535  selberg3lem2  27537  selberg4lem1  27539  pntrsumo1  27544  pntrsumbnd2  27546  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntpbnd1a  27564  pntpbnd1  27565  pntibndlem2a  27569  pntibndlem2  27570  pntlemg  27577  pntlemh  27578  pntlemj  27582  pntlemf  27584  ostth2lem1  27597  padicabvf  27610  padicabvcxp  27611  ostth2lem2  27613  ostth2lem3  27614  ostth2lem4  27615  ostth2  27616  ostth3  27617  numclwwlk5  30475  numclwwlk7  30478  nrt2irr  30560  ubthlem2  30958  minvecolem4  30967  iundisjf  32675  ssnnssfz  32877  iundisjfi  32886  nexple  32935  2exple2exp  32936  pfxlsw2ccat  33042  pmtrto1cl  33192  psgnfzto1stlem  33193  fzto1st1  33195  fzto1st  33196  psgnfzto1st  33198  cycpmco2lem6  33224  cycpmco2lem7  33225  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  fldext2rspun  33859  smatrcl  33973  smattr  33976  smatbl  33977  smatbr  33978  1smat1  33981  submateqlem1  33984  submateqlem2  33985  submateq  33986  esumcst  34240  fiunelros  34351  oddpwdc  34531  eulerpartlems  34537  eulerpartlemgc  34539  fiblem  34575  dstfrvunirn  34652  dstfrvclim1  34655  ballotlemimin  34683  fsum2dsub  34784  reprinfz1  34799  hgt750lemd  34825  hgt750lemb  34833  hgt750leme  34835  tgoldbachgtde  34837  tgoldbachgt  34840  subfaclim  35401  subfacval3  35402  erdszelem7  35410  erdszelem8  35411  erdsze2lem2  35417  cvmliftlem2  35499  cvmliftlem6  35503  cvmliftlem7  35504  cvmliftlem8  35505  cvmliftlem9  35506  cvmliftlem10  35507  cvmliftlem13  35509  bcprod  35951  bccolsum  35952  faclimlem2  35957  faclim2  35961  nn0prpwlem  36535  knoppcnlem10  36721  knoppndvlem15  36745  knoppndvlem17  36747  knoppndvlem18  36748  knoppndvlem19  36749  knoppndvlem20  36750  knoppndvlem21  36751  poimirlem3  37868  poimirlem6  37871  poimirlem7  37872  poimirlem8  37873  poimirlem9  37874  poimirlem10  37875  poimirlem11  37876  poimirlem12  37877  poimirlem13  37878  poimirlem15  37880  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem21  37886  poimirlem22  37887  poimirlem23  37888  poimirlem26  37891  poimirlem28  37893  opnmbllem0  37901  mblfinlem2  37903  incsequz  37993  nninfnub  37996  lcmineqlem4  42396  lcmineqlem10  42402  lcmineqlem11  42403  lcmineqlem15  42407  lcmineqlem18  42410  lcmineqlem19  42411  lcmineqlem20  42412  lcmineqlem21  42413  lcmineqlem22  42414  lcmineqlem23  42415  lcmineqlem  42416  3lexlogpow5ineq2  42419  3lexlogpow5ineq4  42420  3lexlogpow2ineq2  42423  3lexlogpow5ineq5  42424  aks4d1p1p3  42433  aks4d1p1p2  42434  aks4d1p1p4  42435  aks4d1p1p5  42439  aks4d1p1  42440  aks4d1p3  42442  aks4d1p4  42443  aks4d1p5  42444  aks4d1p6  42445  aks4d1p7  42447  aks4d1p8d2  42449  aks4d1p8  42451  aks4d1p9  42452  posbezout  42464  primrootlekpowne0  42469  primrootspoweq0  42470  aks6d1c1  42480  hashscontpow1  42485  aks6d1c3  42487  aks6d1c4  42488  aks6d1c2lem4  42491  aks6d1c2  42494  aks6d1c5lem1  42500  2ap1caineq  42509  sticksstones1  42510  sticksstones2  42511  sticksstones3  42512  sticksstones6  42515  sticksstones7  42516  sticksstones10  42519  sticksstones12a  42521  sticksstones12  42522  aks6d1c6lem4  42537  bcled  42542  bcle2d  42543  aks6d1c7lem1  42544  aks6d1c7lem2  42545  unitscyglem1  42559  unitscyglem2  42560  unitscyglem4  42562  unitscyglem5  42563  aks5lem8  42565  nnadddir  42634  oexpreposd  42686  fimgmcyclem  42897  fimgmcyc  42898  flt4lem5e  43008  flt4lem6  43010  flt4lem7  43011  fltltc  43013  fltnltalem  43014  fltnlta  43015  3cubeslem3r  43038  irrapxlem3  43175  irrapxlem4  43176  irrapxlem5  43177  pellexlem2  43181  pellexlem6  43185  pell14qrgt0  43210  pell14qrgapw  43227  pellfundgt1  43234  rmspecsqrtnq  43257  ltrmxnn0  43300  jm3.1lem1  43368  jm3.1lem3  43370  dgraa0p  43500  hashnzfz2  44671  rfcnnnub  45390  nnxrd  45630  fzisoeu  45656  fsumnncl  45926  sumnnodd  45984  limsup10exlem  46124  stoweidlem1  46353  stoweidlem3  46355  stoweidlem11  46363  stoweidlem17  46369  stoweidlem20  46372  stoweidlem25  46377  stoweidlem26  46378  stoweidlem34  46386  stoweidlem38  46390  stoweidlem42  46394  stoweidlem44  46396  stoweidlem51  46403  stoweidlem59  46411  stoweidlem60  46412  wallispi  46422  wallispi2  46425  stirlinglem3  46428  stirlinglem4  46429  stirlinglem8  46433  stirlinglem10  46435  stirlinglem12  46437  stirlinglem15  46440  dirkertrigeqlem2  46451  dirkertrigeqlem3  46452  dirkercncflem2  46456  fourierdlem11  46470  fourierdlem14  46473  fourierdlem15  46474  fourierdlem20  46479  fourierdlem31  46490  fourierdlem64  46522  fourierdlem93  46551  fourierdlem95  46553  fourierdlem103  46561  fourierdlem104  46562  fourierdlem112  46570  sqwvfourb  46581  etransclem3  46589  etransclem19  46605  etransclem23  46609  etransclem24  46610  etransclem25  46611  etransclem32  46618  etransclem35  46621  etransclem41  46627  etransclem48  46634  qndenserrnbllem  46646  hoiqssbllem1  46974  hoiqssbllem2  46975  ovolval5lem1  47004  ovolval5lem2  47005  iccpartlt  47778  iccpartgt  47781  odz2prm2pw  47917  fmtnoprmfac1lem  47918  2pwp1prm  47943  sfprmdvdsmersenne  47957  lighneallem2  47960  proththdlem  47967  perfectALTVlem2  48076  gbowge7  48117  ztprmneprm  48701  pgrple2abl  48719  logbpw2m1  48921  nnpw2pmod  48937  nnolog2flm1  48944  blennngt2o2  48946  itcovalt2lem2lem1  49027