Theorem nn0red 12584

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  ℕ₀cn0 12522

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-nn 12252  df-n0 12523

This theorem is used by:  nn0cnd  12585  nn0readdcl  12589  eluzmn  12887  flmulnn0  13880  quoremz  13908  quoremnn0ALT  13910  modaddmodup  13990  modaddmodlo  13991  expneg  14125  expnbnd  14288  facdiv  14343  faclbnd6  14355  hashdom  14435  hashun2  14439  hashunx  14442  hashfun  14494  hashf1  14514  seqcoll2  14522  hashge2el2dif  14537  hashtpg  14542  wrdlenge2n0  14609  ccatdmss  14639  ccatsymb  14640  ccatrn  14647  ccatalpha  14652  ccat2s1fvw  14698  swrdnd  14716  swrdnd0  14719  pfxnd0  14750  pfxsuffeqwrdeq  14759  swrdccat3blem  14800  cshwidxmod  14866  repswcshw  14875  swrds2  15003  modfsummods  15871  climcnds  15931  geomulcvg  15956  mertenslem1  15964  binomfallfaclem2  16119  binomrisefac  16121  fallfacval4  16122  efcllem  16156  eftlub  16190  ruclem10  16320  oddge22np1  16432  nn0oddm1d2  16468  divalglem5  16480  bitsfzolem  16517  bitsfzo  16518  bitsmod  16519  sadcaddlem  16540  sadaddlem  16549  sadasslem  16553  sadeq  16555  smuval2  16565  smupvallem  16566  smueqlem  16573  bezoutlem3  16624  bezoutlem4  16625  gcdzeq  16635  dvdssqlem  16649  nn0seqcvgd  16653  eucalglt  16668  lcmneg  16686  mulgcddvds  16738  qredeu  16741  prmdvdsbc  16810  prmdiveq  16870  odzdvds  16880  pythagtriplem3  16903  pythagtriplem6  16906  pythagtriplem7  16907  iserodd  16920  pclem  16923  pcpremul  16928  pcidlem  16957  pcgcd1  16962  pc2dvds  16964  pcz  16966  pcprmpw2  16967  fldivp1  16982  pcfaclem  16983  pcfac  16984  pcbc  16985  prmreclem2  17002  prmreclem3  17003  prmreclem4  17004  prmreclem5  17005  4sqlem11  17040  4sqlem12  17041  4sqlem14  17043  vdwlem11  17076  vdwlem12  17077  ramlb  17104  0ram  17105  ram0  17107  ramub1lem2  17112  ramcl  17114  psgnunilem2  19596  odmodnn0  19641  mndodconglem  19642  mndodcong  19643  oddvds  19648  odhash3  19677  gexdvds  19685  sylow1lem1  19699  sylow1lem5  19703  pgpfi  19706  pgpssslw  19715  efgsfo  19840  efgredlemd  19845  efgredlem  19848  efgred  19849  lt6abl  19996  telgsums  20094  pgpfaclem2  20185  srgbinomlem3  20341  zringlpirlem3  21651  psrbaglesupp  22109  psrbagcon  22112  psrbagleadd1  22115  mplmonmul  22224  psdmul  22366  coe1tmmul2  22474  coe1tmmul2fv  22476  coe1pwmulfv  22478  gsummoncoe1  22505  fvmptnn04if  23043  fvmptnn04ifc  23046  fvmptnn04ifd  23047  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  lebnumii  25162  dyadmaxlem  25793  mbfi1fseqlem3  25913  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mdegmullem  26272  coe1mul3  26293  coe1mul4  26294  deg1sublt  26304  deg1mul2  26308  deg1tmle  26312  deg1tm  26313  ply1divmo  26330  ply1divex  26331  deg1submon1p  26347  dvdsq1p  26357  fta1glem2  26363  fta1blem  26365  plyco0  26386  plyeq0lem  26404  plypf1  26406  plyaddlem1  26407  coeeulem  26418  dgrub  26428  dgrlb  26430  dgreq  26438  coeaddlem  26443  coemullem  26444  coemulhi  26448  dgrlt  26460  dgradd2  26462  dgrmul  26464  dgrcolem2  26468  dgrco  26469  plydivlem3  26493  plydivlem4  26494  plydivex  26495  plydiveu  26496  fta1lem  26505  quotcan  26507  vieta1lem2  26509  radcnvlem1  26613  dvradcnv  26621  leibpi  27144  log2tlbnd  27147  birthdaylem2  27154  birthdaylem3  27155  fsumharmonic  27213  dmlogdmgm  27225  basellem3  27284  basellem5  27286  issqf  27337  ppip1le  27362  ppiltx  27378  mumullem2  27381  sgmppw  27398  ppiub  27405  chtublem  27412  chpub  27421  dchrabs  27461  bcmono  27478  bcmax  27479  bcp1ctr  27480  bclbnd  27481  bposlem5  27489  gausslemma2dlem0h  27564  gausslemma2dlem4  27570  gausslemma2dlem6  27573  lgseisenlem1  27576  2lgsoddprmlem2  27610  2sqlem7  27625  2sqlem8  27627  2sq2  27634  2sqmod  27637  chebbnd1lem1  27670  chtppilimlem1  27674  dchrisum0re  27714  mulogsumlem  27732  selberg2lem  27751  pntrlog2bndlem4  27781  pntlemr  27803  pntlemj  27804  pnt  27815  ostth2lem3  27836  vtxdgfival  29856  vtxdfiun  29869  vtxdginducedm1fi  29931  crctcsh  30210  wwlksnred  30278  wwlksnextproplem2  30296  rusgrnumwwlks  30363  eupth2lems  30626  eucrct2eupth  30633  numclwlk1lem1  30757  numclwwlk5  30776  numclwwlk6  30778  friendshipgt3  30786  nnmulge  33121  nndiffz1  33168  fzo0opth  33185  suppssnn0  33187  pfxlsw2ccat  33303  wrdt2ind  33306  gsumwrd2dccatlem  33428  cycpmrn  33494  cyc3conja  33508  1arithidomlem1  33856  1arithidomlem2  33857  1arithidom  33858  ply1unit  33896  ply1dg3rt0irred  33905  ply1degltel  33915  ply1degleel  33916  ply1degltlss  33917  psrmonmul  33971  esplyfval2  33986  esplyfval3  33993  exsslsb  34018  ply1degltdimlem  34043  ply1degltdim  34044  fldextrspundgdvdslem  34101  fldextrspundgdvds  34102  extdgfialglem1  34113  minplyirredlem  34131  irredminply  34137  nn0constr  34182  iconstr  34187  cos9thpiminplylem1  34203  oddpwdc  34776  eulerpartlems  34782  eulerpartlemgc  34784  eulerpartlemb  34790  coinfliplem  34901  signsplypnf  34969  signslema  34981  signstfvc  34993  signstfveq0  34996  fsum2dsub  35026  reprlt  35038  reprgt  35040  reprinfz1  35041  breprexplemc  35051  lpadmax  35104  lpadright  35106  usgrgt2cycl  35643  acycgr1v  35662  erdszelem8  35711  erdsze2lem2  35717  cvmliftlem7  35804  snmlff  35842  bcprod  36251  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem13  38325  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem25  38337  poimirlem26  38338  poimirlem29  38341  poimirlem30  38342  poimirlem31  38343  rrnequiv  38527  lcmineqlem17  42853  lcmineqlem21  42857  3lexlogpow5ineq5  42868  aks4d1p1p4  42879  aks4d1p1p7  42882  aks4d1p3  42886  aks4d1p7d1  42890  aks6d1c1  42924  aks6d1c3  42931  aks6d1c2lem4  42935  hashnexinj  42936  aks6d1c2  42938  aks6d1c5lem1  42944  aks6d1c5lem3  42945  aks6d1c5lem2  42946  aks6d1c5  42947  2np3bcnp1  42952  2ap1caineq  42953  sticksstones6  42959  sticksstones7  42960  sticksstones22  42976  aks6d1c6lem3  42980  aks6d1c6lem4  42981  bcled  42986  bcle2d  42987  aks6d1c7lem1  42988  aks6d1c7lem2  42989  unitscyglem1  43003  unitscyglem4  43006  aks5lem8  43009  frlmvscadiccat  43321  fltnltalem  43435  eldioph2lem1  43532  pell1qrge1  43638  rmxypos  43715  ltrmynn0  43716  ltrmxnn0  43717  lermxnn0  43718  jm2.24nn  43727  jm2.24  43731  jm2.19  43761  jm2.26lem3  43769  jm2.27c  43775  hbt  43898  dgraa0p  43917  binomcxplemnn0  45100  fsumnncl  46329  mccllem  46354  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvnxpaek  46697  dvnmul  46698  dvnprodlem2  46702  stoweidlem17  46772  stoweidlem24  46779  wallispilem5  46824  stirlinglem15  46843  fourierdlem48  46909  fourierdlem83  46944  fourierdlem103  46964  fourierdlem104  46965  sqwvfoura  46983  elaa2lem  46988  etransclem10  46999  etransclem19  47008  etransclem20  47009  etransclem21  47010  etransclem22  47011  etransclem23  47012  etransclem24  47013  etransclem27  47016  etransclem32  47021  etransclem35  47024  etransclem44  47033  etransclem45  47034  etransclem46  47035  etransclem47  47036  etransclem48  47037  etransc  47038  rrndistlt  47045  chnsubseqwl  47636  chnsubseq  47637  fmtnoge3  48323  sqrtpwpw2p  48331  fmtnosqrt  48332  flsqrt  48386  lighneallem4a  48401  ssnn0ssfz  49170  pgrple2abl  49186  nn0eo  49349  fllog2  49389  itcovalt2lem2lem1  49494  aacllem  50662