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  33651  fldextrspundgdvds  33652  fldext2rspun  33653  smatrcl  33762  smattr  33765  smatbl  33766  smatbr  33767  1smat1  33770  submateqlem1  33773  submateqlem2  33774  submateq  33775  esumcst  34029  fiunelros  34140  oddpwdc  34321  eulerpartlems  34327  eulerpartlemgc  34329  fiblem  34365  dstfrvunirn  34442  dstfrvclim1  34445  ballotlemimin  34473  fsum2dsub  34574  reprinfz1  34589  hgt750lemd  34615  hgt750lemb  34623  hgt750leme  34625  tgoldbachgtde  34627  tgoldbachgt  34630  subfaclim  35160  subfacval3  35161  erdszelem7  35169  erdszelem8  35170  erdsze2lem2  35176  cvmliftlem2  35258  cvmliftlem6  35262  cvmliftlem7  35263  cvmliftlem8  35264  cvmliftlem9  35265  cvmliftlem10  35266  cvmliftlem13  35268  bcprod  35710  bccolsum  35711  faclimlem2  35716  faclim2  35720  nn0prpwlem  36295  knoppcnlem10  36475  knoppndvlem15  36499  knoppndvlem17  36501  knoppndvlem18  36502  knoppndvlem19  36503  knoppndvlem20  36504  knoppndvlem21  36505  poimirlem3  37602  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem9  37608  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem23  37622  poimirlem26  37625  poimirlem28  37627  opnmbllem0  37635  mblfinlem2  37637  incsequz  37727  nninfnub  37730  lcmineqlem4  42005  lcmineqlem10  42011  lcmineqlem11  42012  lcmineqlem15  42016  lcmineqlem18  42019  lcmineqlem19  42020  lcmineqlem20  42021  lcmineqlem21  42022  lcmineqlem22  42023  lcmineqlem23  42024  lcmineqlem  42025  3lexlogpow5ineq2  42028  3lexlogpow5ineq4  42029  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p3  42051  aks4d1p4  42052  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7  42056  aks4d1p8d2  42058  aks4d1p8  42060  aks4d1p9  42061  posbezout  42073  primrootlekpowne0  42078  primrootspoweq0  42079  aks6d1c1  42089  hashscontpow1  42094  aks6d1c3  42096  aks6d1c4  42097  aks6d1c2lem4  42100  aks6d1c2  42103  aks6d1c5lem1  42109  2ap1caineq  42118  sticksstones1  42119  sticksstones2  42120  sticksstones3  42121  sticksstones6  42124  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  aks6d1c6lem4  42146  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7lem2  42154  unitscyglem1  42168  unitscyglem2  42169  unitscyglem4  42171  unitscyglem5  42172  aks5lem8  42174  nnadddir  42243  oexpreposd  42295  fimgmcyclem  42506  fimgmcyc  42507  flt4lem5e  42629  flt4lem6  42631  flt4lem7  42632  fltltc  42634  fltnltalem  42635  fltnlta  42636  3cubeslem3r  42660  irrapxlem3  42797  irrapxlem4  42798  irrapxlem5  42799  pellexlem2  42803  pellexlem6  42807  pell14qrgt0  42832  pell14qrgapw  42849  pellfundgt1  42856  rmspecsqrtnq  42879  ltrmxnn0  42922  jm3.1lem1  42990  jm3.1lem3  42992  dgraa0p  43122  hashnzfz2  44294  rfcnnnub  45014  nnxrd  45256  fzisoeu  45282  fsumnncl  45554  sumnnodd  45612  limsup10exlem  45754  stoweidlem1  45983  stoweidlem3  45985  stoweidlem11  45993  stoweidlem17  45999  stoweidlem20  46002  stoweidlem25  46007  stoweidlem26  46008  stoweidlem34  46016  stoweidlem38  46020  stoweidlem42  46024  stoweidlem44  46026  stoweidlem51  46033  stoweidlem59  46041  stoweidlem60  46042  wallispi  46052  wallispi2  46055  stirlinglem3  46058  stirlinglem4  46059  stirlinglem8  46063  stirlinglem10  46065  stirlinglem12  46067  stirlinglem15  46070  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  dirkercncflem2  46086  fourierdlem11  46100  fourierdlem14  46103  fourierdlem15  46104  fourierdlem20  46109  fourierdlem31  46120  fourierdlem64  46152  fourierdlem93  46181  fourierdlem95  46183  fourierdlem103  46191  fourierdlem104  46192  fourierdlem112  46200  sqwvfourb  46211  etransclem3  46219  etransclem19  46235  etransclem23  46239  etransclem24  46240  etransclem25  46241  etransclem32  46248  etransclem35  46251  etransclem41  46257  etransclem48  46264  qndenserrnbllem  46276  hoiqssbllem1  46604  hoiqssbllem2  46605  ovolval5lem1  46634  ovolval5lem2  46635  iccpartlt  47409  iccpartgt  47412  odz2prm2pw  47548  fmtnoprmfac1lem  47549  2pwp1prm  47574  sfprmdvdsmersenne  47588  lighneallem2  47591  proththdlem  47598  perfectALTVlem2  47707  gbowge7  47748  ztprmneprm  48332  pgrple2abl  48350  logbpw2m1  48553  nnpw2pmod  48569  nnolog2flm1  48576  blennngt2o2  48578  itcovalt2lem2lem1  48659