Theorem nn0red 12649

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11180  ℕ₀cn0 12587

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-i2m1 11249  ax-1ne0 11250  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-nn 12317  df-n0 12588

This theorem is used by:  nn0cnd  12650  nn0readdcl  12654  eluzmn  12953  flmulnn0  13947  quoremz  13975  quoremnn0ALT  13977  modaddmodup  14057  modaddmodlo  14058  expneg  14192  expnbnd  14356  facdiv  14411  faclbnd6  14423  hashdom  14503  hashun2  14507  hashunx  14510  hashfun  14562  hashf1  14582  seqcoll2  14590  hashge2el2dif  14605  hashtpg  14610  wrdlenge2n0  14677  ccatdmss  14707  ccatsymb  14708  ccatrn  14715  ccatalpha  14720  ccat2s1fvw  14766  swrdnd  14784  swrdnd0  14787  pfxnd0  14818  pfxsuffeqwrdeq  14827  swrdccat3blem  14868  cshwidxmod  14934  repswcshw  14943  swrds2  15071  modfsummods  15940  climcnds  16000  geomulcvg  16025  mertenslem1  16033  binomfallfaclem2  16186  binomrisefac  16188  fallfacval4  16189  efcllem  16223  eftlub  16257  ruclem10  16387  oddge22np1  16499  nn0oddm1d2  16535  divalglem5  16547  bitsfzolem  16584  bitsfzo  16585  bitsmod  16586  sadcaddlem  16607  sadaddlem  16616  sadasslem  16620  sadeq  16622  smuval2  16632  smupvallem  16633  smueqlem  16640  bezoutlem3  16694  bezoutlem4  16695  gcdzeq  16705  nn0seqcvgd  16725  eucalglt  16740  lcmneg  16758  mulgcddvds  16810  qredeu  16813  prmdvdsbc  16882  prmdiveq  16943  odzdvds  16953  pythagtriplem3  16976  pythagtriplem6  16979  pythagtriplem7  16980  iserodd  16993  pclem  16996  pcpremul  17001  pcidlem  17030  pcgcd1  17035  pc2dvds  17037  pcz  17039  pcprmpw2  17040  fldivp1  17055  pcfaclem  17056  pcfac  17057  pcbc  17058  prmreclem2  17075  prmreclem3  17076  prmreclem4  17077  prmreclem5  17078  4sqlem11  17113  4sqlem12  17114  4sqlem14  17116  vdwlem11  17149  vdwlem12  17150  ramlb  17177  0ram  17178  ram0  17180  ramub1lem2  17185  ramcl  17187  psgnunilem2  19689  odmodnn0  19734  mndodconglem  19735  mndodcong  19736  oddvds  19741  odhash3  19770  gexdvds  19778  sylow1lem1  19792  sylow1lem5  19796  pgpfi  19799  pgpssslw  19808  efgsfo  19933  efgredlemd  19938  efgredlem  19941  efgred  19942  lt6abl  20089  telgsums  20187  pgpfaclem2  20278  srgbinomlem3  20434  zringlpirlem3  21750  psrbaglesupp  22210  psrbagcon  22213  psrbagleadd1  22216  mplmonmul  22325  psdmul  22467  coe1tmmul2  22575  coe1tmmul2fv  22577  coe1pwmulfv  22579  gsummoncoe1  22606  fvmptnn04if  23147  fvmptnn04ifc  23150  fvmptnn04ifd  23151  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  lebnumii  25267  dyadmaxlem  25898  mbfi1fseqlem3  26018  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  mdegmullem  26376  coe1mul3  26397  coe1mul4  26398  deg1sublt  26408  deg1mul2  26412  deg1tmle  26416  deg1tm  26417  ply1divmo  26434  ply1divex  26435  deg1submon1p  26451  dvdsq1p  26461  fta1glem2  26467  fta1blem  26469  plyco0  26490  plyeq0lem  26509  plypf1  26511  plyaddlem1  26512  coeeulem  26523  dgrub  26533  dgrlb  26535  dgreq  26543  coeaddlem  26548  coemullem  26549  coemulhi  26553  dgrlt  26565  dgradd2  26567  dgrmul  26569  dgrcolem2  26573  dgrco  26574  plydivlem3  26598  plydivlem4  26599  plydivex  26600  plydiveu  26601  fta1lem  26610  quotcan  26614  vieta1lem2  26616  radcnvlem1  26722  dvradcnv  26730  leibpi  27252  log2tlbnd  27255  birthdaylem2  27262  birthdaylem3  27263  fsumharmonic  27321  dmlogdmgm  27333  basellem3  27392  basellem5  27394  issqf  27445  ppip1le  27470  ppiltx  27486  mumullem2  27489  sgmppw  27506  ppiub  27513  chtublem  27520  chpub  27529  dchrabs  27569  bcmono  27586  bcmax  27587  bcp1ctr  27588  bclbnd  27589  bposlem5  27597  gausslemma2dlem0h  27672  gausslemma2dlem4  27678  gausslemma2dlem6  27681  lgseisenlem1  27684  2lgsoddprmlem2  27718  2sqlem7  27733  2sqlem8  27735  2sq2  27742  2sqmod  27745  chebbnd1lem1  27778  chtppilimlem1  27782  dchrisum0re  27822  mulogsumlem  27840  selberg2lem  27859  pntrlog2bndlem4  27889  pntlemr  27911  pntlemj  27912  pnt  27923  ostth2lem3  27944  vtxdgfival  30032  vtxdfiun  30045  vtxdginducedm1fi  30107  crctcsh  30395  wwlksnred  30463  wwlksnextproplem2  30481  rusgrnumwwlks  30548  eupth2lems  30821  eucrct2eupth  30828  numclwlk1lem1  30952  numclwwlk5  30971  numclwwlk6  30973  friendshipgt3  30981  nnmulge  33313  nndiffz1  33360  fzo0opth  33377  suppssnn0  33379  pfxlsw2ccat  33495  wrdt2ind  33498  gsumwrd2dccatlem  33620  cycpmrn  33686  cyc3conja  33700  1arithidomlem1  34049  1arithidomlem2  34050  1arithidom  34051  ply1unit  34089  ply1dg3rt0irred  34098  ply1degltel  34108  ply1degleel  34109  ply1degltlss  34110  psrmonmul  34164  esplyfval2  34179  esplyfval3  34186  exsslsb  34211  ply1degltdimlem  34236  ply1degltdim  34237  fldextrspundgdvdslem  34294  fldextrspundgdvds  34295  extdgfialglem1  34306  minplyirredlem  34324  irredminply  34330  nn0constr  34375  iconstr  34380  cos9thpiminplylem1  34396  oddpwdc  34969  eulerpartlems  34975  eulerpartlemgc  34977  eulerpartlemb  34983  coinfliplem  35094  signsplypnf  35162  signslema  35174  signstfvc  35186  signstfveq0  35189  fsum2dsub  35219  reprlt  35231  reprgt  35233  reprinfz1  35234  breprexplemc  35244  lpadmax  35297  lpadright  35299  usgrgt2cycl  35878  acycgr1v  35883  erdszelem8  35932  erdsze2lem2  35938  cvmliftlem7  36025  snmlff  36063  bcprod  36472  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem13  38519  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem26  38532  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  rrnequiv  38737  lcmineqlem17  43063  lcmineqlem21  43067  3lexlogpow5ineq5  43078  aks4d1p1p4  43089  aks4d1p1p7  43092  aks4d1p3  43096  aks4d1p7d1  43100  aks6d1c1  43134  aks6d1c3  43141  aks6d1c2lem4  43145  hashnexinj  43146  aks6d1c2  43148  aks6d1c5lem1  43154  aks6d1c5lem3  43155  aks6d1c5lem2  43156  aks6d1c5  43157  2np3bcnp1  43162  2ap1caineq  43163  sticksstones6  43169  sticksstones7  43170  sticksstones22  43186  aks6d1c6lem3  43190  aks6d1c6lem4  43191  bcled  43196  bcle2d  43197  aks6d1c7lem1  43198  aks6d1c7lem2  43199  unitscyglem1  43213  unitscyglem4  43216  aks5lem8  43219  frlmvscadiccat  43538  fltnltalem  43627  eldioph2lem1  43724  pell1qrge1  43830  rmxypos  43907  ltrmynn0  43908  ltrmxnn0  43909  lermxnn0  43910  jm2.24nn  43919  jm2.24  43923  jm2.19  43953  jm2.26lem3  43961  jm2.27c  43967  hbt  44090  dgraa0p  44109  binomcxplemnn0  45292  fsumnncl  46528  mccllem  46553  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvnxpaek  46896  dvnmul  46897  dvnprodlem2  46901  stoweidlem17  46971  stoweidlem24  46978  wallispilem5  47023  stirlinglem15  47042  fourierdlem48  47108  fourierdlem83  47143  fourierdlem103  47163  fourierdlem104  47164  sqwvfoura  47182  elaa2lem  47187  etransclem10  47198  etransclem19  47207  etransclem20  47208  etransclem21  47209  etransclem22  47210  etransclem23  47211  etransclem24  47212  etransclem27  47215  etransclem32  47220  etransclem35  47223  etransclem44  47232  etransclem45  47233  etransclem46  47234  etransclem47  47235  etransclem48  47236  etransc  47237  rrndistlt  47244  chnsubseqwl  47833  chnsubseq  47834  fmtnoge3  48559  sqrtpwpw2p  48567  fmtnosqrt  48568  flsqrt  48622  lighneallem4a  48637  ssnn0ssfz  49405  pgrple2abl  49421  nn0eo  49584  fllog2  49624  itcovalt2lem2lem1  49729  aacllem  50883