Theorem nnred 12278

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℕcn 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264

This theorem is referenced by:  nnne0  12297  uzwo3  12982  modmulnn  13925  bernneq3  14266  expmulnbnd  14270  expnngt1b  14277  facwordi  14324  faclbnd  14325  faclbnd2  14326  faclbnd3  14327  faclbnd5  14333  faclbnd6  14334  facubnd  14335  facavg  14336  bcp1nk  14352  hashf1  14492  swrds2  14975  isercolllem1  15697  isercoll  15700  o1fsum  15845  climcndslem1  15881  climcndslem2  15882  climcnds  15883  eftabs  16107  efcllem  16109  ege2le3  16122  efcj  16124  eftlub  16141  eflegeo  16153  eirrlem  16236  fzm1ndvds  16355  nno  16415  nnoddm1d2  16419  bitsfzolem  16467  bitsfzo  16468  bitsinv1lem  16474  sadcaddlem  16490  smueqlem  16523  bezoutlem3  16574  bezoutlem4  16575  sqgcd  16595  nn0expgcd  16597  lcmgcdlem  16639  lcmf  16666  prmind2  16718  coprm  16744  prmfac1  16753  prmndvdsfaclt  16758  divdenle  16782  qnumgt0  16783  zsqrtelqelz  16791  hashdvds  16808  eulerthlem2  16815  odzdvds  16828  vfermltl  16834  modprm0  16838  pythagtriplem11  16858  pythagtriplem13  16860  pythagtriplem19  16866  pclem  16871  pcpre1  16875  pcidlem  16905  dvdsprmpweqle  16919  pcadd  16922  pcmpt  16925  pcmpt2  16926  pcfaclem  16931  pcfac  16932  qexpz  16934  pockthlem  16938  pockthg  16939  prmreclem1  16949  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  1arithlem4  16959  1arith  16960  4sqlem5  16975  4sqlem6  16976  4sqlem10  16980  mul4sqlem  16986  4sqlem11  16988  4sqlem12  16989  4sqlem13  16990  4sqlem14  16991  4sqlem15  16992  4sqlem16  16993  4sqlem17  16994  vdwlem1  17014  vdwlem3  17016  vdwlem6  17019  vdwlem9  17022  vdwlem10  17023  vdwlem12  17025  vdwnnlem3  17030  ramub1lem1  17059  prmolefac  17079  prmgaplem4  17087  prmgaplem5  17088  prmgaplem6  17089  prmgaplem8  17091  2expltfac  17126  cshwshashnsame  17137  setsstruct2  17207  psgnunilem4  19529  mndodconglem  19573  oddvds  19579  sylow1lem1  19630  sylow1lem5  19634  fislw  19657  efgredlem  19779  gexexlem  19884  zringlpirlem3  21492  prmirredlem  21500  fvmptnn04if  22870  fvmptnn04ifb  22872  fvmptnn04ifc  22873  fvmptnn04ifd  22874  chfacfisf  22875  chfacfisfcpmat  22876  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  lebnumii  25011  lmnn  25310  ovolunlem1a  25544  ovoliunlem1  25550  ovolicc2lem3  25567  ovolicc2lem4  25568  iundisj  25596  voliunlem1  25598  uniioombllem3  25633  dyadf  25639  dyadovol  25641  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  vitalilem4  25659  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2gt0  25809  itg2cnlem2  25811  dgreq0  26319  dgrco  26329  elqaalem2  26376  aaliou3lem2  26399  aaliou3lem8  26401  aaliou3lem9  26406  rtprmirr  26817  leibpi  26999  log2tlbnd  27002  birthdaylem3  27010  amgm  27048  emcllem2  27054  harmonicbnd4  27068  lgamgulmlem1  27086  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamucov  27095  lgamcvg2  27112  wilthlem1  27125  ftalem5  27134  basellem1  27138  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  basellem6  27143  basellem8  27145  chtge0  27169  chtwordi  27213  vma1  27223  dvdsflf1o  27244  dvdsflsumcom  27245  fsumfldivdiaglem  27246  sgmmul  27259  chtublem  27269  fsumvma2  27272  logfac2  27275  chpchtsum  27277  chpub  27278  logfaclbnd  27280  logexprlim  27283  mersenne  27285  perfectlem2  27288  dchrelbas4  27301  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem7  27348  bposlem9  27350  lgslem1  27355  lgsval2lem  27365  lgsdirprm  27389  lgsdir  27390  lgsne0  27393  lgsqrlem2  27405  gausslemma2dlem0h  27421  gausslemma2dlem0i  27422  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  2sqlem3  27478  2sqlem8  27484  2sqblem  27489  2sqmod  27494  chebbnd1lem1  27527  chebbnd1lem3  27529  chtppilimlem1  27531  rplogsumlem1  27542  rplogsumlem2  27543  dchrisum0lem1a  27544  rpvmasumlem  27545  dchrisumlema  27546  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  dchrvmasumiflem1  27559  dchrisum0flblem2  27567  dchrisum0re  27571  dchrisum0lem1b  27573  dchrisum0lem1  27574  dirith2  27586  selbergb  27607  selberg2lem  27608  logdivbnd  27614  selberg3lem2  27616  selberg4lem1  27618  pntrsumo1  27623  pntrsumbnd2  27625  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntpbnd1a  27643  pntpbnd1  27644  pntibndlem2a  27648  pntibndlem2  27649  pntlemg  27656  pntlemh  27657  pntlemj  27661  pntlemf  27663  ostth2lem1  27676  padicabvf  27689  padicabvcxp  27690  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth2  27695  ostth3  27696  numclwwlk5  30416  numclwwlk7  30419  nrt2irr  30501  ubthlem2  30899  minvecolem4  30908  iundisjf  32608  ssnnssfz  32795  iundisjfi  32803  pfxlsw2ccat  32919  chnub  32985  pmtrto1cl  33101  psgnfzto1stlem  33102  fzto1st1  33104  fzto1st  33105  psgnfzto1st  33107  cycpmco2lem6  33133  cycpmco2lem7  33134  smatrcl  33756  smattr  33759  smatbl  33760  smatbr  33761  1smat1  33764  submateqlem1  33767  submateqlem2  33768  submateq  33769  esumcst  34043  fiunelros  34154  oddpwdc  34335  eulerpartlems  34341  eulerpartlemgc  34343  fiblem  34379  dstfrvunirn  34455  dstfrvclim1  34458  ballotlemimin  34486  fsum2dsub  34600  reprinfz1  34615  hgt750lemd  34641  hgt750lemb  34649  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgt  34656  subfaclim  35172  subfacval3  35173  erdszelem7  35181  erdszelem8  35182  erdsze2lem2  35188  cvmliftlem2  35270  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem8  35276  cvmliftlem9  35277  cvmliftlem10  35278  cvmliftlem13  35280  bcprod  35717  bccolsum  35718  faclimlem2  35723  faclim2  35727  nn0prpwlem  36304  knoppcnlem10  36484  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem18  36511  knoppndvlem19  36512  knoppndvlem20  36513  knoppndvlem21  36514  poimirlem3  37609  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem26  37632  poimirlem28  37634  opnmbllem0  37642  mblfinlem2  37644  incsequz  37734  nninfnub  37737  lcmineqlem4  42013  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem15  42024  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  lcmineqlem23  42032  lcmineqlem  42033  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p3  42059  aks4d1p4  42060  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootlekpowne0  42086  primrootspoweq0  42087  aks6d1c1  42097  hashscontpow1  42102  aks6d1c3  42104  aks6d1c4  42105  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem1  42117  2ap1caineq  42126  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem4  42154  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  unitscyglem1  42176  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  aks5lem8  42182  metakunt1  42186  metakunt2  42187  metakunt6  42191  metakunt7  42192  metakunt9  42194  metakunt10  42195  metakunt11  42196  metakunt12  42197  metakunt16  42201  metakunt18  42203  metakunt20  42205  metakunt22  42207  metakunt24  42209  metakunt27  42212  metakunt28  42213  metakunt29  42214  metakunt30  42215  nnadddir  42283  oexpreposd  42335  fimgmcyclem  42519  fimgmcyc  42520  flt4lem5e  42642  flt4lem6  42644  flt4lem7  42645  fltltc  42647  fltnltalem  42648  fltnlta  42649  3cubeslem3r  42674  irrapxlem3  42811  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pell14qrgt0  42846  pell14qrgapw  42863  pellfundgt1  42870  rmspecsqrtnq  42893  ltrmxnn0  42937  jm3.1lem1  43005  jm3.1lem3  43007  dgraa0p  43137  hashnzfz2  44316  rfcnnnub  44973  nnxrd  45223  fzisoeu  45250  fsumnncl  45527  sumnnodd  45585  limsup10exlem  45727  stoweidlem1  45956  stoweidlem3  45958  stoweidlem11  45966  stoweidlem17  45972  stoweidlem20  45975  stoweidlem25  45980  stoweidlem26  45981  stoweidlem34  45989  stoweidlem38  45993  stoweidlem42  45997  stoweidlem44  45999  stoweidlem51  46006  stoweidlem59  46014  stoweidlem60  46015  wallispi  46025  wallispi2  46028  stirlinglem3  46031  stirlinglem4  46032  stirlinglem8  46036  stirlinglem10  46038  stirlinglem12  46040  stirlinglem15  46043  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkercncflem2  46059  fourierdlem11  46073  fourierdlem14  46076  fourierdlem15  46077  fourierdlem20  46082  fourierdlem31  46093  fourierdlem64  46125  fourierdlem93  46154  fourierdlem95  46156  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  sqwvfourb  46184  etransclem3  46192  etransclem19  46208  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem32  46221  etransclem35  46224  etransclem41  46230  etransclem48  46237  qndenserrnbllem  46249  hoiqssbllem1  46577  hoiqssbllem2  46578  ovolval5lem1  46607  ovolval5lem2  46608  iccpartlt  47348  iccpartgt  47351  odz2prm2pw  47487  fmtnoprmfac1lem  47488  2pwp1prm  47513  sfprmdvdsmersenne  47527  lighneallem2  47530  proththdlem  47537  perfectALTVlem2  47646  gbowge7  47687  ztprmneprm  48191  pgrple2abl  48209  logbpw2m1  48416  nnpw2pmod  48432  nnolog2flm1  48439  blennngt2o2  48441  itcovalt2lem2lem1  48522