Theorem nn0red 12464

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

Hypothesis

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

Assertion

Ref	Expression
nn0red	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nn0red

Step	Hyp	Ref	Expression
1		nn0ssre 12406	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3935	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  ℕ₀cn0 12402

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-rnegex 11099  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  df-n0 12403

This theorem is referenced by:  nn0cnd  12465  nn0readdcl  12469  eluzmn  12760  flmulnn0  13749  quoremz  13777  quoremnn0ALT  13779  modaddmodup  13859  modaddmodlo  13860  expneg  13994  expnbnd  14157  facdiv  14212  faclbnd6  14224  hashdom  14304  hashun2  14308  hashunx  14311  hashfun  14362  hashf1  14382  seqcoll2  14390  hashge2el2dif  14405  hashtpg  14410  wrdlenge2n0  14477  ccatsymb  14507  ccatrn  14514  ccatalpha  14518  ccat2s1fvw  14563  swrdnd  14579  swrdnd0  14582  pfxnd0  14613  pfxsuffeqwrdeq  14622  swrdccat3blem  14663  cshwidxmod  14727  repswcshw  14736  swrds2  14865  modfsummods  15718  climcnds  15776  geomulcvg  15801  mertenslem1  15809  binomfallfaclem2  15965  binomrisefac  15967  fallfacval4  15968  efcllem  16002  eftlub  16036  ruclem10  16166  oddge22np1  16278  nn0oddm1d2  16314  divalglem5  16326  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  sadcaddlem  16386  sadaddlem  16395  sadasslem  16399  sadeq  16401  smuval2  16411  smupvallem  16412  smueqlem  16419  bezoutlem3  16470  bezoutlem4  16471  gcdzeq  16481  dvdssqlem  16495  nn0seqcvgd  16499  eucalglt  16514  lcmneg  16532  mulgcddvds  16584  qredeu  16587  prmdvdsbc  16655  prmdiveq  16715  odzdvds  16725  pythagtriplem3  16748  pythagtriplem6  16751  pythagtriplem7  16752  iserodd  16765  pclem  16768  pcpremul  16773  pcidlem  16802  pcgcd1  16807  pc2dvds  16809  pcz  16811  pcprmpw2  16812  fldivp1  16827  pcfaclem  16828  pcfac  16829  pcbc  16830  prmreclem2  16847  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  4sqlem11  16885  4sqlem12  16886  4sqlem14  16888  vdwlem11  16921  vdwlem12  16922  ramlb  16949  0ram  16950  ram0  16952  ramub1lem2  16957  ramcl  16959  psgnunilem2  19392  odmodnn0  19437  mndodconglem  19438  mndodcong  19439  oddvds  19444  odhash3  19473  gexdvds  19481  sylow1lem1  19495  sylow1lem5  19499  pgpfi  19502  pgpssslw  19511  efgsfo  19636  efgredlemd  19641  efgredlem  19644  efgred  19645  lt6abl  19792  telgsums  19890  pgpfaclem2  19981  srgbinomlem3  20131  zringlpirlem3  21389  psrbaglesupp  21847  psrbagcon  21850  psrbagleadd1  21853  mplmonmul  21959  psdmul  22069  coe1tmmul2  22178  coe1tmmul2fv  22180  coe1pwmulfv  22182  gsummoncoe1  22211  fvmptnn04if  22752  fvmptnn04ifc  22755  fvmptnn04ifd  22756  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  lebnumii  24881  dyadmaxlem  25514  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mdegmullem  25999  coe1mul3  26020  coe1mul4  26021  deg1sublt  26031  deg1mul2  26035  deg1tmle  26039  deg1tm  26040  ply1divmo  26057  ply1divex  26058  deg1submon1p  26074  dvdsq1p  26084  fta1glem2  26090  fta1blem  26092  plyco0  26113  plyeq0lem  26131  plypf1  26133  plyaddlem1  26134  coeeulem  26145  dgrub  26155  dgrlb  26157  dgreq  26165  coeaddlem  26170  coemullem  26171  coemulhi  26175  dgrlt  26188  dgradd2  26190  dgrmul  26192  dgrcolem2  26196  dgrco  26197  plydivlem3  26219  plydivlem4  26220  plydivex  26221  plydiveu  26222  fta1lem  26231  quotcan  26233  vieta1lem2  26235  radcnvlem1  26338  dvradcnv  26346  leibpi  26868  log2tlbnd  26871  birthdaylem2  26878  birthdaylem3  26879  fsumharmonic  26938  dmlogdmgm  26950  basellem3  27009  basellem5  27011  issqf  27062  ppip1le  27087  ppiltx  27103  mumullem2  27106  sgmppw  27124  ppiub  27131  chtublem  27138  chpub  27147  dchrabs  27187  bcmono  27204  bcmax  27205  bcp1ctr  27206  bclbnd  27207  bposlem5  27215  gausslemma2dlem0h  27290  gausslemma2dlem4  27296  gausslemma2dlem6  27299  lgseisenlem1  27302  2lgsoddprmlem2  27336  2sqlem7  27351  2sqlem8  27353  2sq2  27360  2sqmod  27363  chebbnd1lem1  27396  chtppilimlem1  27400  dchrisum0re  27440  mulogsumlem  27458  selberg2lem  27477  pntrlog2bndlem4  27507  pntlemr  27529  pntlemj  27530  pnt  27541  ostth2lem3  27562  vtxdgfival  29433  vtxdfiun  29446  vtxdginducedm1fi  29508  crctcsh  29787  wwlksnred  29855  wwlksnextproplem2  29873  rusgrnumwwlks  29937  eupth2lems  30200  eucrct2eupth  30207  numclwlk1lem1  30331  numclwwlk5  30350  numclwwlk6  30352  friendshipgt3  30360  nnmulge  32695  nndiffz1  32742  fzo0opth  32761  suppssnn0  32763  ccatdmss  32904  pfxlsw2ccat  32905  wrdt2ind  32908  gsumwrd2dccatlem  33032  cycpmrn  33098  cyc3conja  33112  1arithidomlem1  33485  1arithidomlem2  33486  1arithidom  33487  ply1unit  33523  ply1dg3rt0irred  33530  ply1degltel  33539  ply1degleel  33540  ply1degltlss  33541  exsslsb  33571  ply1degltdimlem  33597  ply1degltdim  33598  fldextrspundgdvdslem  33654  fldextrspundgdvds  33655  minplyirredlem  33679  irredminply  33685  nn0constr  33730  iconstr  33735  cos9thpiminplylem1  33751  oddpwdc  34324  eulerpartlems  34330  eulerpartlemgc  34332  eulerpartlemb  34338  coinfliplem  34449  signsplypnf  34520  signslema  34532  signstfvc  34544  signstfveq0  34547  fsum2dsub  34577  reprlt  34589  reprgt  34591  reprinfz1  34592  breprexplemc  34602  lpadmax  34652  lpadright  34654  usgrgt2cycl  35105  acycgr1v  35124  erdszelem8  35173  erdsze2lem2  35179  cvmliftlem7  35266  snmlff  35304  bcprod  35713  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem26  37628  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  rrnequiv  37817  lcmineqlem17  42021  lcmineqlem21  42025  3lexlogpow5ineq5  42036  aks4d1p1p4  42047  aks4d1p1p7  42050  aks4d1p3  42054  aks4d1p7d1  42058  aks6d1c1  42092  aks6d1c3  42099  aks6d1c2lem4  42103  hashnexinj  42104  aks6d1c2  42106  aks6d1c5lem1  42112  aks6d1c5lem3  42113  aks6d1c5lem2  42114  aks6d1c5  42115  2np3bcnp1  42120  2ap1caineq  42121  sticksstones6  42127  sticksstones7  42128  sticksstones22  42144  aks6d1c6lem3  42148  aks6d1c6lem4  42149  bcled  42154  bcle2d  42155  aks6d1c7lem1  42156  aks6d1c7lem2  42157  unitscyglem1  42171  unitscyglem4  42174  aks5lem8  42177  frlmvscadiccat  42482  fltnltalem  42638  eldioph2lem1  42736  pell1qrge1  42846  rmxypos  42923  ltrmynn0  42924  ltrmxnn0  42925  lermxnn0  42926  jm2.24nn  42935  jm2.24  42939  jm2.19  42969  jm2.26lem3  42977  jm2.27c  42983  hbt  43106  dgraa0p  43125  binomcxplemnn0  44325  fsumnncl  45557  mccllem  45582  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnxpaek  45927  dvnmul  45928  dvnprodlem2  45932  stoweidlem17  46002  stoweidlem24  46009  wallispilem5  46054  stirlinglem15  46073  fourierdlem48  46139  fourierdlem83  46174  fourierdlem103  46194  fourierdlem104  46195  sqwvfoura  46213  elaa2lem  46218  etransclem10  46229  etransclem19  46238  etransclem20  46239  etransclem21  46240  etransclem22  46241  etransclem23  46242  etransclem24  46243  etransclem27  46246  etransclem32  46251  etransclem35  46254  etransclem44  46263  etransclem45  46264  etransclem46  46265  etransclem47  46266  etransclem48  46267  etransc  46268  rrndistlt  46275  fmtnoge3  47518  sqrtpwpw2p  47526  fmtnosqrt  47527  flsqrt  47581  lighneallem4a  47596  ssnn0ssfz  48337  pgrple2abl  48353  nn0eo  48517  fllog2  48557  itcovalt2lem2lem1  48662  aacllem  49790