Theorem nn0red 12497

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  ℕ₀cn0 12435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-nn 12173  df-n0 12436

This theorem is referenced by:  nn0cnd  12498  nn0readdcl  12502  eluzmn  12793  flmulnn0  13784  quoremz  13812  quoremnn0ALT  13814  modaddmodup  13894  modaddmodlo  13895  expneg  14029  expnbnd  14192  facdiv  14247  faclbnd6  14259  hashdom  14339  hashun2  14343  hashunx  14346  hashfun  14397  hashf1  14417  seqcoll2  14425  hashge2el2dif  14440  hashtpg  14445  wrdlenge2n0  14512  ccatdmss  14542  ccatsymb  14543  ccatrn  14550  ccatalpha  14554  ccat2s1fvw  14599  swrdnd  14615  swrdnd0  14618  pfxnd0  14649  pfxsuffeqwrdeq  14658  swrdccat3blem  14699  cshwidxmod  14763  repswcshw  14772  swrds2  14900  modfsummods  15754  climcnds  15814  geomulcvg  15839  mertenslem1  15847  binomfallfaclem2  16003  binomrisefac  16005  fallfacval4  16006  efcllem  16040  eftlub  16074  ruclem10  16204  oddge22np1  16316  nn0oddm1d2  16352  divalglem5  16364  bitsfzolem  16401  bitsfzo  16402  bitsmod  16403  sadcaddlem  16424  sadaddlem  16433  sadasslem  16437  sadeq  16439  smuval2  16449  smupvallem  16450  smueqlem  16457  bezoutlem3  16508  bezoutlem4  16509  gcdzeq  16519  dvdssqlem  16533  nn0seqcvgd  16537  eucalglt  16552  lcmneg  16570  mulgcddvds  16622  qredeu  16625  prmdvdsbc  16694  prmdiveq  16754  odzdvds  16764  pythagtriplem3  16787  pythagtriplem6  16790  pythagtriplem7  16791  iserodd  16804  pclem  16807  pcpremul  16812  pcidlem  16841  pcgcd1  16846  pc2dvds  16848  pcz  16850  pcprmpw2  16851  fldivp1  16866  pcfaclem  16867  pcfac  16868  pcbc  16869  prmreclem2  16886  prmreclem3  16887  prmreclem4  16888  prmreclem5  16889  4sqlem11  16924  4sqlem12  16925  4sqlem14  16927  vdwlem11  16960  vdwlem12  16961  ramlb  16988  0ram  16989  ram0  16991  ramub1lem2  16996  ramcl  16998  psgnunilem2  19468  odmodnn0  19513  mndodconglem  19514  mndodcong  19515  oddvds  19520  odhash3  19549  gexdvds  19557  sylow1lem1  19571  sylow1lem5  19575  pgpfi  19578  pgpssslw  19587  efgsfo  19712  efgredlemd  19717  efgredlem  19720  efgred  19721  lt6abl  19868  telgsums  19966  pgpfaclem2  20057  srgbinomlem3  20207  zringlpirlem3  21446  psrbaglesupp  21904  psrbagcon  21907  psrbagleadd1  21910  mplmonmul  22019  psdmul  22161  coe1tmmul2  22269  coe1tmmul2fv  22271  coe1pwmulfv  22273  gsummoncoe1  22301  fvmptnn04if  22839  fvmptnn04ifc  22842  fvmptnn04ifd  22843  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  lebnumii  24958  dyadmaxlem  25589  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mdegmullem  26068  coe1mul3  26089  coe1mul4  26090  deg1sublt  26100  deg1mul2  26104  deg1tmle  26108  deg1tm  26109  ply1divmo  26126  ply1divex  26127  deg1submon1p  26143  dvdsq1p  26153  fta1glem2  26159  fta1blem  26161  plyco0  26182  plyeq0lem  26200  plypf1  26202  plyaddlem1  26203  coeeulem  26214  dgrub  26224  dgrlb  26226  dgreq  26234  coeaddlem  26239  coemullem  26240  coemulhi  26244  dgrlt  26256  dgradd2  26258  dgrmul  26260  dgrcolem2  26264  dgrco  26265  plydivlem3  26286  plydivlem4  26287  plydivex  26288  plydiveu  26289  fta1lem  26298  quotcan  26300  vieta1lem2  26302  radcnvlem1  26403  dvradcnv  26411  leibpi  26931  log2tlbnd  26934  birthdaylem2  26941  birthdaylem3  26942  fsumharmonic  27000  dmlogdmgm  27012  basellem3  27071  basellem5  27073  issqf  27124  ppip1le  27149  ppiltx  27165  mumullem2  27168  sgmppw  27185  ppiub  27192  chtublem  27199  chpub  27208  dchrabs  27248  bcmono  27265  bcmax  27266  bcp1ctr  27267  bclbnd  27268  bposlem5  27276  gausslemma2dlem0h  27351  gausslemma2dlem4  27357  gausslemma2dlem6  27360  lgseisenlem1  27363  2lgsoddprmlem2  27397  2sqlem7  27412  2sqlem8  27414  2sq2  27421  2sqmod  27424  chebbnd1lem1  27457  chtppilimlem1  27461  dchrisum0re  27501  mulogsumlem  27519  selberg2lem  27538  pntrlog2bndlem4  27568  pntlemr  27590  pntlemj  27591  pnt  27602  ostth2lem3  27623  vtxdgfival  29563  vtxdfiun  29576  vtxdginducedm1fi  29638  crctcsh  29917  wwlksnred  29985  wwlksnextproplem2  30003  rusgrnumwwlks  30070  eupth2lems  30333  eucrct2eupth  30340  numclwlk1lem1  30464  numclwwlk5  30483  numclwwlk6  30485  friendshipgt3  30493  nnmulge  32838  nndiffz1  32885  fzo0opth  32902  suppssnn0  32904  pfxlsw2ccat  33036  wrdt2ind  33039  gsumwrd2dccatlem  33165  cycpmrn  33231  cyc3conja  33245  1arithidomlem1  33625  1arithidomlem2  33626  1arithidom  33627  ply1unit  33665  ply1dg3rt0irred  33674  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  psrmonmul  33741  esplyfval2  33756  esplyfval3  33763  exsslsb  33788  ply1degltdimlem  33813  ply1degltdim  33814  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  extdgfialglem1  33883  minplyirredlem  33901  irredminply  33907  nn0constr  33952  iconstr  33957  cos9thpiminplylem1  33973  oddpwdc  34545  eulerpartlems  34551  eulerpartlemgc  34553  eulerpartlemb  34559  coinfliplem  34670  signsplypnf  34741  signslema  34753  signstfvc  34765  signstfveq0  34768  fsum2dsub  34798  reprlt  34810  reprgt  34812  reprinfz1  34813  breprexplemc  34823  lpadmax  34873  lpadright  34875  usgrgt2cycl  35365  acycgr1v  35384  erdszelem8  35433  erdsze2lem2  35439  cvmliftlem7  35526  snmlff  35564  bcprod  35973  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem26  38020  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  rrnequiv  38209  lcmineqlem17  42537  lcmineqlem21  42541  3lexlogpow5ineq5  42552  aks4d1p1p4  42563  aks4d1p1p7  42566  aks4d1p3  42570  aks4d1p7d1  42574  aks6d1c1  42608  aks6d1c3  42615  aks6d1c2lem4  42619  hashnexinj  42620  aks6d1c2  42622  aks6d1c5lem1  42628  aks6d1c5lem3  42629  aks6d1c5lem2  42630  aks6d1c5  42631  2np3bcnp1  42636  2ap1caineq  42637  sticksstones6  42643  sticksstones7  42644  sticksstones22  42660  aks6d1c6lem3  42664  aks6d1c6lem4  42665  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  aks6d1c7lem2  42673  unitscyglem1  42687  unitscyglem4  42690  aks5lem8  42693  frlmvscadiccat  43003  fltnltalem  43119  eldioph2lem1  43216  pell1qrge1  43322  rmxypos  43399  ltrmynn0  43400  ltrmxnn0  43401  lermxnn0  43402  jm2.24nn  43411  jm2.24  43415  jm2.19  43445  jm2.26lem3  43453  jm2.27c  43459  hbt  43582  dgraa0p  43601  binomcxplemnn0  44800  fsumnncl  46024  mccllem  46049  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnxpaek  46392  dvnmul  46393  dvnprodlem2  46397  stoweidlem17  46467  stoweidlem24  46474  wallispilem5  46519  stirlinglem15  46538  fourierdlem48  46604  fourierdlem83  46639  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  elaa2lem  46683  etransclem10  46694  etransclem19  46703  etransclem20  46704  etransclem21  46705  etransclem22  46706  etransclem23  46707  etransclem24  46708  etransclem27  46711  etransclem32  46716  etransclem35  46719  etransclem44  46728  etransclem45  46729  etransclem46  46730  etransclem47  46731  etransclem48  46732  etransc  46733  rrndistlt  46740  chnsubseqwl  47331  chnsubseq  47332  fmtnoge3  48015  sqrtpwpw2p  48023  fmtnosqrt  48024  flsqrt  48078  lighneallem4a  48093  ssnn0ssfz  48847  pgrple2abl  48863  nn0eo  49026  fllog2  49066  itcovalt2lem2lem1  49171  aacllem  50298