Theorem nn0red 12585

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℕ₀cn0 12523

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-rnegex 11223  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  df-n0 12524

This theorem is referenced by:  nn0cnd  12586  nn0readdcl  12590  eluzmn  12882  flmulnn0  13863  quoremz  13891  quoremnn0ALT  13893  modaddmodup  13971  modaddmodlo  13972  expneg  14106  expnbnd  14267  facdiv  14322  faclbnd6  14334  hashdom  14414  hashun2  14418  hashunx  14421  hashfun  14472  hashf1  14492  seqcoll2  14500  hashge2el2dif  14515  hashtpg  14520  wrdlenge2n0  14586  ccatsymb  14616  ccatrn  14623  ccatalpha  14627  ccat2s1fvw  14672  swrdnd  14688  swrdnd0  14691  pfxnd0  14722  pfxsuffeqwrdeq  14732  swrdccat3blem  14773  cshwidxmod  14837  repswcshw  14846  swrds2  14975  modfsummods  15825  climcnds  15883  geomulcvg  15908  mertenslem1  15916  binomfallfaclem2  16072  binomrisefac  16074  fallfacval4  16075  efcllem  16109  eftlub  16141  ruclem10  16271  oddge22np1  16382  nn0oddm1d2  16418  divalglem5  16430  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  sadcaddlem  16490  sadaddlem  16499  sadasslem  16503  sadeq  16505  smuval2  16515  smupvallem  16516  smueqlem  16523  bezoutlem3  16574  bezoutlem4  16575  gcdzeq  16585  dvdssqlem  16599  nn0seqcvgd  16603  eucalglt  16618  lcmneg  16636  mulgcddvds  16688  qredeu  16691  prmdvdsbc  16759  prmdiveq  16819  odzdvds  16828  pythagtriplem3  16851  pythagtriplem6  16854  pythagtriplem7  16855  iserodd  16868  pclem  16871  pcpremul  16876  pcidlem  16905  pcgcd1  16910  pc2dvds  16912  pcz  16914  pcprmpw2  16915  fldivp1  16930  pcfaclem  16931  pcfac  16932  pcbc  16933  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  4sqlem11  16988  4sqlem12  16989  4sqlem14  16991  vdwlem11  17024  vdwlem12  17025  ramlb  17052  0ram  17053  ram0  17055  ramub1lem2  17060  ramcl  17062  psgnunilem2  19527  odmodnn0  19572  mndodconglem  19573  mndodcong  19574  oddvds  19579  odhash3  19608  gexdvds  19616  sylow1lem1  19630  sylow1lem5  19634  pgpfi  19637  pgpssslw  19646  efgsfo  19771  efgredlemd  19776  efgredlem  19779  efgred  19780  lt6abl  19927  telgsums  20025  pgpfaclem2  20116  srgbinomlem3  20245  zringlpirlem3  21492  psrbaglesupp  21959  psrbagcon  21962  psrbagleadd1  21965  mplmonmul  22071  psdmul  22187  coe1tmmul2  22294  coe1tmmul2fv  22296  coe1pwmulfv  22298  gsummoncoe1  22327  fvmptnn04if  22870  fvmptnn04ifc  22873  fvmptnn04ifd  22874  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  lebnumii  25011  dyadmaxlem  25645  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mdegmullem  26131  coe1mul3  26152  coe1mul4  26153  deg1sublt  26163  deg1mul2  26167  deg1tmle  26171  deg1tm  26172  ply1divmo  26189  ply1divex  26190  deg1submon1p  26206  dvdsq1p  26216  fta1glem2  26222  fta1blem  26224  plyco0  26245  plyeq0lem  26263  plypf1  26265  plyaddlem1  26266  coeeulem  26277  dgrub  26287  dgrlb  26289  dgreq  26297  coeaddlem  26302  coemullem  26303  coemulhi  26307  dgrlt  26320  dgradd2  26322  dgrmul  26324  dgrcolem2  26328  dgrco  26329  plydivlem3  26351  plydivlem4  26352  plydivex  26353  plydiveu  26354  fta1lem  26363  quotcan  26365  vieta1lem2  26367  radcnvlem1  26470  dvradcnv  26478  leibpi  26999  log2tlbnd  27002  birthdaylem2  27009  birthdaylem3  27010  fsumharmonic  27069  dmlogdmgm  27081  basellem3  27140  basellem5  27142  issqf  27193  ppip1le  27218  ppiltx  27234  mumullem2  27237  sgmppw  27255  ppiub  27262  chtublem  27269  chpub  27278  dchrabs  27318  bcmono  27335  bcmax  27336  bcp1ctr  27337  bclbnd  27338  bposlem5  27346  gausslemma2dlem0h  27421  gausslemma2dlem4  27427  gausslemma2dlem6  27430  lgseisenlem1  27433  2lgsoddprmlem2  27467  2sqlem7  27482  2sqlem8  27484  2sq2  27491  2sqmod  27494  chebbnd1lem1  27527  chtppilimlem1  27531  dchrisum0re  27571  mulogsumlem  27589  selberg2lem  27608  pntrlog2bndlem4  27638  pntlemr  27660  pntlemj  27661  pnt  27672  ostth2lem3  27693  vtxdgfival  29501  vtxdfiun  29514  vtxdginducedm1fi  29576  crctcsh  29853  wwlksnred  29921  wwlksnextproplem2  29939  rusgrnumwwlks  30003  eupth2lems  30266  eucrct2eupth  30273  numclwlk1lem1  30397  numclwwlk5  30416  numclwwlk6  30418  friendshipgt3  30426  nnmulge  32755  nndiffz1  32794  fzo0opth  32812  suppssnn0  32814  ccatdmss  32918  pfxlsw2ccat  32919  wrdt2ind  32922  gsumwrd2dccatlem  33051  cycpmrn  33145  cyc3conja  33159  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  ply1unit  33579  ply1dg3rt0irred  33586  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ply1degltdimlem  33649  ply1degltdim  33650  minplyirredlem  33717  irredminply  33721  nexple  33989  oddpwdc  34335  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemb  34349  coinfliplem  34459  signsplypnf  34543  signslema  34555  signstfvc  34567  signstfveq0  34570  fsum2dsub  34600  reprlt  34612  reprgt  34614  reprinfz1  34615  breprexplemc  34625  lpadmax  34675  lpadright  34677  usgrgt2cycl  35114  acycgr1v  35133  erdszelem8  35182  erdsze2lem2  35188  cvmliftlem7  35275  snmlff  35313  bcprod  35717  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  rrnequiv  37821  lcmineqlem17  42026  lcmineqlem21  42030  3lexlogpow5ineq5  42041  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p3  42059  aks4d1p7d1  42063  aks6d1c1  42097  aks6d1c3  42104  aks6d1c2lem4  42108  hashnexinj  42109  aks6d1c2  42111  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  2np3bcnp1  42125  2ap1caineq  42126  sticksstones6  42132  sticksstones7  42133  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c6lem4  42154  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  unitscyglem1  42176  unitscyglem4  42179  aks5lem8  42182  frlmvscadiccat  42492  fltnltalem  42648  eldioph2lem1  42747  pell1qrge1  42857  rmxypos  42935  ltrmynn0  42936  ltrmxnn0  42937  lermxnn0  42938  jm2.24nn  42947  jm2.24  42951  jm2.19  42981  jm2.26lem3  42989  jm2.27c  42995  hbt  43118  dgraa0p  43137  binomcxplemnn0  44344  fsumnncl  45527  mccllem  45552  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnxpaek  45897  dvnmul  45898  dvnprodlem2  45902  stoweidlem17  45972  stoweidlem24  45979  wallispilem5  46024  stirlinglem15  46043  fourierdlem48  46109  fourierdlem83  46144  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  elaa2lem  46188  etransclem10  46199  etransclem19  46208  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem23  46212  etransclem24  46213  etransclem27  46216  etransclem32  46221  etransclem35  46224  etransclem44  46233  etransclem45  46234  etransclem46  46235  etransclem47  46236  etransclem48  46237  etransc  46238  rrndistlt  46245  fmtnoge3  47454  sqrtpwpw2p  47462  fmtnosqrt  47463  flsqrt  47517  lighneallem4a  47532  ssnn0ssfz  48193  pgrple2abl  48209  nn0eo  48377  fllog2  48417  itcovalt2lem2lem1  48522  aacllem  49031