Theorem nn0red 12567

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 12509	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3936	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235  df-n0 12506

This theorem is referenced by:  nn0cnd  12568  nn0readdcl  12572  eluzmn  12870  flmulnn0  13862  quoremz  13890  quoremnn0ALT  13892  modaddmodup  13972  modaddmodlo  13973  expneg  14107  expnbnd  14270  facdiv  14325  faclbnd6  14337  hashdom  14417  hashun2  14421  hashunx  14424  hashfun  14476  hashf1  14496  seqcoll2  14504  hashge2el2dif  14519  hashtpg  14524  wrdlenge2n0  14591  ccatdmss  14621  ccatsymb  14622  ccatrn  14629  ccatalpha  14633  ccat2s1fvw  14678  swrdnd  14694  swrdnd0  14697  pfxnd0  14728  pfxsuffeqwrdeq  14737  swrdccat3blem  14778  cshwidxmod  14842  repswcshw  14851  swrds2  14979  modfsummods  15847  climcnds  15907  geomulcvg  15932  mertenslem1  15940  binomfallfaclem2  16095  binomrisefac  16097  fallfacval4  16098  efcllem  16132  eftlub  16166  ruclem10  16296  oddge22np1  16408  nn0oddm1d2  16444  divalglem5  16456  bitsfzolem  16493  bitsfzo  16494  bitsmod  16495  sadcaddlem  16516  sadaddlem  16525  sadasslem  16529  sadeq  16531  smuval2  16541  smupvallem  16542  smueqlem  16549  bezoutlem3  16600  bezoutlem4  16601  gcdzeq  16611  dvdssqlem  16625  nn0seqcvgd  16629  eucalglt  16644  lcmneg  16662  mulgcddvds  16714  qredeu  16717  prmdvdsbc  16786  prmdiveq  16846  odzdvds  16856  pythagtriplem3  16879  pythagtriplem6  16882  pythagtriplem7  16883  iserodd  16896  pclem  16899  pcpremul  16904  pcidlem  16933  pcgcd1  16938  pc2dvds  16940  pcz  16942  pcprmpw2  16943  fldivp1  16958  pcfaclem  16959  pcfac  16960  pcbc  16961  prmreclem2  16978  prmreclem3  16979  prmreclem4  16980  prmreclem5  16981  4sqlem11  17016  4sqlem12  17017  4sqlem14  17019  vdwlem11  17052  vdwlem12  17053  ramlb  17080  0ram  17081  ram0  17083  ramub1lem2  17088  ramcl  17090  psgnunilem2  19566  odmodnn0  19611  mndodconglem  19612  mndodcong  19613  oddvds  19618  odhash3  19647  gexdvds  19655  sylow1lem1  19669  sylow1lem5  19673  pgpfi  19676  pgpssslw  19685  efgsfo  19810  efgredlemd  19815  efgredlem  19818  efgred  19819  lt6abl  19966  telgsums  20064  pgpfaclem2  20155  srgbinomlem3  20311  zringlpirlem3  21595  psrbaglesupp  22053  psrbagcon  22056  psrbagleadd1  22059  mplmonmul  22168  psdmul  22310  coe1tmmul2  22418  coe1tmmul2fv  22420  coe1pwmulfv  22422  gsummoncoe1  22449  fvmptnn04if  22987  fvmptnn04ifc  22990  fvmptnn04ifd  22991  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  lebnumii  25106  dyadmaxlem  25737  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mdegmullem  26216  coe1mul3  26237  coe1mul4  26238  deg1sublt  26248  deg1mul2  26252  deg1tmle  26256  deg1tm  26257  ply1divmo  26274  ply1divex  26275  deg1submon1p  26291  dvdsq1p  26301  fta1glem2  26307  fta1blem  26309  plyco0  26330  plyeq0lem  26348  plypf1  26350  plyaddlem1  26351  coeeulem  26362  dgrub  26372  dgrlb  26374  dgreq  26382  coeaddlem  26387  coemullem  26388  coemulhi  26392  dgrlt  26404  dgradd2  26406  dgrmul  26408  dgrcolem2  26412  dgrco  26413  plydivlem3  26437  plydivlem4  26438  plydivex  26439  plydiveu  26440  fta1lem  26449  quotcan  26451  vieta1lem2  26453  radcnvlem1  26557  dvradcnv  26565  leibpi  27088  log2tlbnd  27091  birthdaylem2  27098  birthdaylem3  27099  fsumharmonic  27157  dmlogdmgm  27169  basellem3  27228  basellem5  27230  issqf  27281  ppip1le  27306  ppiltx  27322  mumullem2  27325  sgmppw  27342  ppiub  27349  chtublem  27356  chpub  27365  dchrabs  27405  bcmono  27422  bcmax  27423  bcp1ctr  27424  bclbnd  27425  bposlem5  27433  gausslemma2dlem0h  27508  gausslemma2dlem4  27514  gausslemma2dlem6  27517  lgseisenlem1  27520  2lgsoddprmlem2  27554  2sqlem7  27569  2sqlem8  27571  2sq2  27578  2sqmod  27581  chebbnd1lem1  27614  chtppilimlem1  27618  dchrisum0re  27658  mulogsumlem  27676  selberg2lem  27695  pntrlog2bndlem4  27725  pntlemr  27747  pntlemj  27748  pnt  27759  ostth2lem3  27780  vtxdgfival  29800  vtxdfiun  29813  vtxdginducedm1fi  29875  crctcsh  30154  wwlksnred  30222  wwlksnextproplem2  30240  rusgrnumwwlks  30307  eupth2lems  30570  eucrct2eupth  30577  numclwlk1lem1  30701  numclwwlk5  30720  numclwwlk6  30722  friendshipgt3  30730  nnmulge  33065  nndiffz1  33112  fzo0opth  33129  suppssnn0  33131  pfxlsw2ccat  33251  wrdt2ind  33254  gsumwrd2dccatlem  33378  cycpmrn  33444  cyc3conja  33458  1arithidomlem1  33806  1arithidomlem2  33807  1arithidom  33808  ply1unit  33846  ply1dg3rt0irred  33855  ply1degltel  33865  ply1degleel  33866  ply1degltlss  33867  psrmonmul  33921  esplyfval2  33936  esplyfval3  33943  exsslsb  33968  ply1degltdimlem  33993  ply1degltdim  33994  fldextrspundgdvdslem  34051  fldextrspundgdvds  34052  extdgfialglem1  34063  minplyirredlem  34081  irredminply  34087  nn0constr  34132  iconstr  34137  cos9thpiminplylem1  34153  oddpwdc  34725  eulerpartlems  34731  eulerpartlemgc  34733  eulerpartlemb  34739  coinfliplem  34850  signsplypnf  34918  signslema  34930  signstfvc  34942  signstfveq0  34945  fsum2dsub  34975  reprlt  34987  reprgt  34989  reprinfz1  34990  breprexplemc  35000  lpadmax  35053  lpadright  35055  usgrgt2cycl  35603  acycgr1v  35622  erdszelem8  35671  erdsze2lem2  35677  cvmliftlem7  35764  snmlff  35802  bcprod  36211  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem25  38277  poimirlem26  38278  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  rrnequiv  38467  lcmineqlem17  42793  lcmineqlem21  42797  3lexlogpow5ineq5  42808  aks4d1p1p4  42819  aks4d1p1p7  42822  aks4d1p3  42826  aks4d1p7d1  42830  aks6d1c1  42864  aks6d1c3  42871  aks6d1c2lem4  42875  hashnexinj  42876  aks6d1c2  42878  aks6d1c5lem1  42884  aks6d1c5lem3  42885  aks6d1c5lem2  42886  aks6d1c5  42887  2np3bcnp1  42892  2ap1caineq  42893  sticksstones6  42899  sticksstones7  42900  sticksstones22  42916  aks6d1c6lem3  42920  aks6d1c6lem4  42921  bcled  42926  bcle2d  42927  aks6d1c7lem1  42928  aks6d1c7lem2  42929  unitscyglem1  42943  unitscyglem4  42946  aks5lem8  42949  frlmvscadiccat  43261  fltnltalem  43377  eldioph2lem1  43474  pell1qrge1  43580  rmxypos  43657  ltrmynn0  43658  ltrmxnn0  43659  lermxnn0  43660  jm2.24nn  43669  jm2.24  43673  jm2.19  43703  jm2.26lem3  43711  jm2.27c  43717  hbt  43840  dgraa0p  43859  binomcxplemnn0  45042  fsumnncl  46271  mccllem  46296  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnxpaek  46639  dvnmul  46640  dvnprodlem2  46644  stoweidlem17  46714  stoweidlem24  46721  wallispilem5  46766  stirlinglem15  46785  fourierdlem48  46851  fourierdlem83  46886  fourierdlem103  46906  fourierdlem104  46907  sqwvfoura  46925  elaa2lem  46930  etransclem10  46941  etransclem19  46950  etransclem20  46951  etransclem21  46952  etransclem22  46953  etransclem23  46954  etransclem24  46955  etransclem27  46958  etransclem32  46963  etransclem35  46966  etransclem44  46975  etransclem45  46976  etransclem46  46977  etransclem47  46978  etransclem48  46979  etransc  46980  rrndistlt  46987  chnsubseqwl  47578  chnsubseq  47579  fmtnoge3  48265  sqrtpwpw2p  48273  fmtnosqrt  48274  flsqrt  48328  lighneallem4a  48343  ssnn0ssfz  49112  pgrple2abl  49128  nn0eo  49291  fllog2  49331  itcovalt2lem2lem1  49436  aacllem  50584