Theorem nnred 12161

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 12150	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3935	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  ℕcn 12146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147

This theorem is referenced by:  nnne0  12180  uzwo3  12862  modmulnn  13811  bernneq3  14156  expmulnbnd  14160  expnngt1b  14167  facwordi  14214  faclbnd  14215  faclbnd2  14216  faclbnd3  14217  faclbnd5  14223  faclbnd6  14224  facubnd  14225  facavg  14226  bcp1nk  14242  hashf1  14382  swrds2  14865  isercolllem1  15590  isercoll  15593  o1fsum  15738  climcndslem1  15774  climcndslem2  15775  climcnds  15776  eftabs  16000  efcllem  16002  ege2le3  16015  efcj  16017  eftlub  16036  eflegeo  16048  eirrlem  16131  fzm1ndvds  16251  nno  16311  nnoddm1d2  16315  bitsfzolem  16363  bitsfzo  16364  bitsinv1lem  16370  sadcaddlem  16386  smueqlem  16419  bezoutlem3  16470  bezoutlem4  16471  sqgcd  16491  nn0expgcd  16493  lcmgcdlem  16535  lcmf  16562  prmind2  16614  coprm  16640  prmfac1  16649  prmndvdsfaclt  16654  divdenle  16678  qnumgt0  16679  zsqrtelqelz  16687  hashdvds  16704  eulerthlem2  16711  odzdvds  16725  vfermltl  16731  modprm0  16735  pythagtriplem11  16755  pythagtriplem13  16757  pythagtriplem19  16763  pclem  16768  pcpre1  16772  pcidlem  16802  dvdsprmpweqle  16816  pcadd  16819  pcmpt  16822  pcmpt2  16823  pcfaclem  16828  pcfac  16829  qexpz  16831  pockthlem  16835  pockthg  16836  prmreclem1  16846  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  1arithlem4  16856  1arith  16857  4sqlem5  16872  4sqlem6  16873  4sqlem10  16877  mul4sqlem  16883  4sqlem11  16885  4sqlem12  16886  4sqlem13  16887  4sqlem14  16888  4sqlem15  16889  4sqlem16  16890  4sqlem17  16891  vdwlem1  16911  vdwlem3  16913  vdwlem6  16916  vdwlem9  16919  vdwlem10  16920  vdwlem12  16922  vdwnnlem3  16927  ramub1lem1  16956  prmolefac  16976  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  prmgaplem8  16988  2expltfac  17022  cshwshashnsame  17033  setsstruct2  17103  psgnunilem4  19394  mndodconglem  19438  oddvds  19444  sylow1lem1  19495  sylow1lem5  19499  fislw  19522  efgredlem  19644  gexexlem  19749  zringlpirlem3  21389  prmirredlem  21397  fvmptnn04if  22752  fvmptnn04ifb  22754  fvmptnn04ifc  22755  fvmptnn04ifd  22756  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  lebnumii  24881  lmnn  25179  ovolunlem1a  25413  ovoliunlem1  25419  ovolicc2lem3  25436  ovolicc2lem4  25437  iundisj  25465  voliunlem1  25467  uniioombllem3  25502  dyadf  25508  dyadovol  25510  dyaddisjlem  25512  dyadmaxlem  25514  opnmbllem  25518  vitalilem4  25528  mbfi1fseqlem1  25632  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  itg2gt0  25677  itg2cnlem2  25679  dgreq0  26187  dgrco  26197  elqaalem2  26244  aaliou3lem2  26267  aaliou3lem8  26269  aaliou3lem9  26274  rtprmirr  26686  leibpi  26868  log2tlbnd  26871  birthdaylem3  26879  amgm  26917  emcllem2  26923  harmonicbnd4  26937  lgamgulmlem1  26955  lgamgulmlem2  26956  lgamgulmlem3  26957  lgamgulmlem4  26958  lgamgulmlem5  26959  lgamgulmlem6  26960  lgamucov  26964  lgamcvg2  26981  wilthlem1  26994  ftalem5  27003  basellem1  27007  basellem2  27008  basellem3  27009  basellem4  27010  basellem5  27011  basellem6  27012  basellem8  27014  chtge0  27038  chtwordi  27082  vma1  27092  dvdsflf1o  27113  dvdsflsumcom  27114  fsumfldivdiaglem  27115  sgmmul  27128  chtublem  27138  fsumvma2  27141  logfac2  27144  chpchtsum  27146  chpub  27147  logfaclbnd  27149  logexprlim  27152  mersenne  27154  perfectlem2  27157  dchrelbas4  27170  bposlem1  27211  bposlem2  27212  bposlem3  27213  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem7  27217  bposlem9  27219  lgslem1  27224  lgsval2lem  27234  lgsdirprm  27258  lgsdir  27259  lgsne0  27262  lgsqrlem2  27274  gausslemma2dlem0h  27290  gausslemma2dlem0i  27291  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  gausslemma2dlem7  27300  gausslemma2d  27301  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgseisenlem4  27305  lgseisen  27306  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  2sqlem3  27347  2sqlem8  27353  2sqblem  27358  2sqmod  27363  chebbnd1lem1  27396  chebbnd1lem3  27398  chtppilimlem1  27400  rplogsumlem1  27411  rplogsumlem2  27412  dchrisum0lem1a  27413  rpvmasumlem  27414  dchrisumlema  27415  dchrisumlem1  27416  dchrisumlem2  27417  dchrisumlem3  27418  dchrvmasumiflem1  27428  dchrisum0flblem2  27436  dchrisum0re  27440  dchrisum0lem1b  27442  dchrisum0lem1  27443  dirith2  27455  selbergb  27476  selberg2lem  27477  logdivbnd  27483  selberg3lem2  27485  selberg4lem1  27487  pntrsumo1  27492  pntrsumbnd2  27494  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntpbnd1a  27512  pntpbnd1  27513  pntibndlem2a  27517  pntibndlem2  27518  pntlemg  27525  pntlemh  27526  pntlemj  27530  pntlemf  27532  ostth2lem1  27545  padicabvf  27558  padicabvcxp  27559  ostth2lem2  27561  ostth2lem3  27562  ostth2lem4  27563  ostth2  27564  ostth3  27565  numclwwlk5  30350  numclwwlk7  30353  nrt2irr  30435  ubthlem2  30833  minvecolem4  30842  iundisjf  32551  ssnnssfz  32743  iundisjfi  32752  nexple  32802  2exple2exp  32803  pfxlsw2ccat  32905  chnub  32967  pmtrto1cl  33054  psgnfzto1stlem  33055  fzto1st1  33057  fzto1st  33058  psgnfzto1st  33060  cycpmco2lem6  33086  cycpmco2lem7  33087  fldextrspundgdvdslem  33654  fldextrspundgdvds  33655  fldext2rspun  33656  smatrcl  33765  smattr  33768  smatbl  33769  smatbr  33770  1smat1  33773  submateqlem1  33776  submateqlem2  33777  submateq  33778  esumcst  34032  fiunelros  34143  oddpwdc  34324  eulerpartlems  34330  eulerpartlemgc  34332  fiblem  34368  dstfrvunirn  34445  dstfrvclim1  34448  ballotlemimin  34476  fsum2dsub  34577  reprinfz1  34592  hgt750lemd  34618  hgt750lemb  34626  hgt750leme  34628  tgoldbachgtde  34630  tgoldbachgt  34633  subfaclim  35163  subfacval3  35164  erdszelem7  35172  erdszelem8  35173  erdsze2lem2  35179  cvmliftlem2  35261  cvmliftlem6  35265  cvmliftlem7  35266  cvmliftlem8  35267  cvmliftlem9  35268  cvmliftlem10  35269  cvmliftlem13  35271  bcprod  35713  bccolsum  35714  faclimlem2  35719  faclim2  35723  nn0prpwlem  36298  knoppcnlem10  36478  knoppndvlem15  36502  knoppndvlem17  36504  knoppndvlem18  36505  knoppndvlem19  36506  knoppndvlem20  36507  knoppndvlem21  36508  poimirlem3  37605  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem9  37611  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem26  37628  poimirlem28  37630  opnmbllem0  37638  mblfinlem2  37640  incsequz  37730  nninfnub  37733  lcmineqlem4  42008  lcmineqlem10  42014  lcmineqlem11  42015  lcmineqlem15  42019  lcmineqlem18  42022  lcmineqlem19  42023  lcmineqlem20  42024  lcmineqlem21  42025  lcmineqlem22  42026  lcmineqlem23  42027  lcmineqlem  42028  3lexlogpow5ineq2  42031  3lexlogpow5ineq4  42032  3lexlogpow2ineq2  42035  3lexlogpow5ineq5  42036  aks4d1p1p3  42045  aks4d1p1p2  42046  aks4d1p1p4  42047  aks4d1p1p5  42051  aks4d1p1  42052  aks4d1p3  42054  aks4d1p4  42055  aks4d1p5  42056  aks4d1p6  42057  aks4d1p7  42059  aks4d1p8d2  42061  aks4d1p8  42063  aks4d1p9  42064  posbezout  42076  primrootlekpowne0  42081  primrootspoweq0  42082  aks6d1c1  42092  hashscontpow1  42097  aks6d1c3  42099  aks6d1c4  42100  aks6d1c2lem4  42103  aks6d1c2  42106  aks6d1c5lem1  42112  2ap1caineq  42121  sticksstones1  42122  sticksstones2  42123  sticksstones3  42124  sticksstones6  42127  sticksstones7  42128  sticksstones10  42131  sticksstones12a  42133  sticksstones12  42134  aks6d1c6lem4  42149  bcled  42154  bcle2d  42155  aks6d1c7lem1  42156  aks6d1c7lem2  42157  unitscyglem1  42171  unitscyglem2  42172  unitscyglem4  42174  unitscyglem5  42175  aks5lem8  42177  nnadddir  42246  oexpreposd  42298  fimgmcyclem  42509  fimgmcyc  42510  flt4lem5e  42632  flt4lem6  42634  flt4lem7  42635  fltltc  42637  fltnltalem  42638  fltnlta  42639  3cubeslem3r  42663  irrapxlem3  42800  irrapxlem4  42801  irrapxlem5  42802  pellexlem2  42806  pellexlem6  42810  pell14qrgt0  42835  pell14qrgapw  42852  pellfundgt1  42859  rmspecsqrtnq  42882  ltrmxnn0  42925  jm3.1lem1  42993  jm3.1lem3  42995  dgraa0p  43125  hashnzfz2  44297  rfcnnnub  45017  nnxrd  45259  fzisoeu  45285  fsumnncl  45557  sumnnodd  45615  limsup10exlem  45757  stoweidlem1  45986  stoweidlem3  45988  stoweidlem11  45996  stoweidlem17  46002  stoweidlem20  46005  stoweidlem25  46010  stoweidlem26  46011  stoweidlem34  46019  stoweidlem38  46023  stoweidlem42  46027  stoweidlem44  46029  stoweidlem51  46036  stoweidlem59  46044  stoweidlem60  46045  wallispi  46055  wallispi2  46058  stirlinglem3  46061  stirlinglem4  46062  stirlinglem8  46066  stirlinglem10  46068  stirlinglem12  46070  stirlinglem15  46073  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  dirkercncflem2  46089  fourierdlem11  46103  fourierdlem14  46106  fourierdlem15  46107  fourierdlem20  46112  fourierdlem31  46123  fourierdlem64  46155  fourierdlem93  46184  fourierdlem95  46186  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  sqwvfourb  46214  etransclem3  46222  etransclem19  46238  etransclem23  46242  etransclem24  46243  etransclem25  46244  etransclem32  46251  etransclem35  46254  etransclem41  46260  etransclem48  46267  qndenserrnbllem  46279  hoiqssbllem1  46607  hoiqssbllem2  46608  ovolval5lem1  46637  ovolval5lem2  46638  iccpartlt  47412  iccpartgt  47415  odz2prm2pw  47551  fmtnoprmfac1lem  47552  2pwp1prm  47577  sfprmdvdsmersenne  47591  lighneallem2  47594  proththdlem  47601  perfectALTVlem2  47710  gbowge7  47751  ztprmneprm  48335  pgrple2abl  48353  logbpw2m1  48556  nnpw2pmod  48572  nnolog2flm1  48579  blennngt2o2  48581  itcovalt2lem2lem1  48662