Theorem nn0red 12540

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  ℕ₀cn0 12478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-i2m1 11138  ax-1ne0 11139  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-nn 12208  df-n0 12479

This theorem is referenced by:  nn0cnd  12541  nn0readdcl  12545  eluzmn  12843  flmulnn0  13834  quoremz  13862  quoremnn0ALT  13864  modaddmodup  13944  modaddmodlo  13945  expneg  14079  expnbnd  14242  facdiv  14297  faclbnd6  14309  hashdom  14389  hashun2  14393  hashunx  14396  hashfun  14447  hashf1  14467  seqcoll2  14475  hashge2el2dif  14490  hashtpg  14495  wrdlenge2n0  14562  ccatdmss  14592  ccatsymb  14593  ccatrn  14600  ccatalpha  14604  ccat2s1fvw  14649  swrdnd  14665  swrdnd0  14668  pfxnd0  14699  pfxsuffeqwrdeq  14708  swrdccat3blem  14749  cshwidxmod  14813  repswcshw  14822  swrds2  14950  modfsummods  15804  climcnds  15864  geomulcvg  15889  mertenslem1  15897  binomfallfaclem2  16053  binomrisefac  16055  fallfacval4  16056  efcllem  16090  eftlub  16124  ruclem10  16254  oddge22np1  16366  nn0oddm1d2  16402  divalglem5  16414  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  sadcaddlem  16474  sadaddlem  16483  sadasslem  16487  sadeq  16489  smuval2  16499  smupvallem  16500  smueqlem  16507  bezoutlem3  16558  bezoutlem4  16559  gcdzeq  16569  dvdssqlem  16583  nn0seqcvgd  16587  eucalglt  16602  lcmneg  16620  mulgcddvds  16672  qredeu  16675  prmdvdsbc  16744  prmdiveq  16804  odzdvds  16814  pythagtriplem3  16837  pythagtriplem6  16840  pythagtriplem7  16841  iserodd  16854  pclem  16857  pcpremul  16862  pcidlem  16891  pcgcd1  16896  pc2dvds  16898  pcz  16900  pcprmpw2  16901  fldivp1  16916  pcfaclem  16917  pcfac  16918  pcbc  16919  prmreclem2  16936  prmreclem3  16937  prmreclem4  16938  prmreclem5  16939  4sqlem11  16974  4sqlem12  16975  4sqlem14  16977  vdwlem11  17010  vdwlem12  17011  ramlb  17038  0ram  17039  ram0  17041  ramub1lem2  17046  ramcl  17048  psgnunilem2  19518  odmodnn0  19563  mndodconglem  19564  mndodcong  19565  oddvds  19570  odhash3  19599  gexdvds  19607  sylow1lem1  19621  sylow1lem5  19625  pgpfi  19628  pgpssslw  19637  efgsfo  19762  efgredlemd  19767  efgredlem  19770  efgred  19771  lt6abl  19918  telgsums  20016  pgpfaclem2  20107  srgbinomlem3  20257  zringlpirlem3  21496  psrbaglesupp  21954  psrbagcon  21957  psrbagleadd1  21960  mplmonmul  22069  psdmul  22211  coe1tmmul2  22319  coe1tmmul2fv  22321  coe1pwmulfv  22323  gsummoncoe1  22351  fvmptnn04if  22889  fvmptnn04ifc  22892  fvmptnn04ifd  22893  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  lebnumii  25008  dyadmaxlem  25639  mbfi1fseqlem3  25759  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  mdegmullem  26118  coe1mul3  26139  coe1mul4  26140  deg1sublt  26150  deg1mul2  26154  deg1tmle  26158  deg1tm  26159  ply1divmo  26176  ply1divex  26177  deg1submon1p  26193  dvdsq1p  26203  fta1glem2  26209  fta1blem  26211  plyco0  26232  plyeq0lem  26250  plypf1  26252  plyaddlem1  26253  coeeulem  26264  dgrub  26274  dgrlb  26276  dgreq  26284  coeaddlem  26289  coemullem  26290  coemulhi  26294  dgrlt  26306  dgradd2  26308  dgrmul  26310  dgrcolem2  26314  dgrco  26315  plydivlem3  26336  plydivlem4  26337  plydivex  26338  plydiveu  26339  fta1lem  26348  quotcan  26350  vieta1lem2  26352  radcnvlem1  26453  dvradcnv  26461  leibpi  26984  log2tlbnd  26987  birthdaylem2  26994  birthdaylem3  26995  fsumharmonic  27053  dmlogdmgm  27065  basellem3  27124  basellem5  27126  issqf  27177  ppip1le  27202  ppiltx  27218  mumullem2  27221  sgmppw  27238  ppiub  27245  chtublem  27252  chpub  27261  dchrabs  27301  bcmono  27318  bcmax  27319  bcp1ctr  27320  bclbnd  27321  bposlem5  27329  gausslemma2dlem0h  27404  gausslemma2dlem4  27410  gausslemma2dlem6  27413  lgseisenlem1  27416  2lgsoddprmlem2  27450  2sqlem7  27465  2sqlem8  27467  2sq2  27474  2sqmod  27477  chebbnd1lem1  27510  chtppilimlem1  27514  dchrisum0re  27554  mulogsumlem  27572  selberg2lem  27591  pntrlog2bndlem4  27621  pntlemr  27643  pntlemj  27644  pnt  27655  ostth2lem3  27676  vtxdgfival  29616  vtxdfiun  29629  vtxdginducedm1fi  29691  crctcsh  29970  wwlksnred  30038  wwlksnextproplem2  30056  rusgrnumwwlks  30123  eupth2lems  30386  eucrct2eupth  30393  numclwlk1lem1  30517  numclwwlk5  30536  numclwwlk6  30538  friendshipgt3  30546  nnmulge  32891  nndiffz1  32938  fzo0opth  32955  suppssnn0  32957  pfxlsw2ccat  33089  wrdt2ind  33092  gsumwrd2dccatlem  33218  cycpmrn  33284  cyc3conja  33298  1arithidomlem1  33692  1arithidomlem2  33693  1arithidom  33694  ply1unit  33732  ply1dg3rt0irred  33741  ply1degltel  33751  ply1degleel  33752  ply1degltlss  33753  psrmonmul  33808  esplyfval2  33823  esplyfval3  33830  exsslsb  33855  ply1degltdimlem  33880  ply1degltdim  33881  fldextrspundgdvdslem  33938  fldextrspundgdvds  33939  extdgfialglem1  33950  minplyirredlem  33968  irredminply  33974  nn0constr  34019  iconstr  34024  cos9thpiminplylem1  34040  oddpwdc  34612  eulerpartlems  34618  eulerpartlemgc  34620  eulerpartlemb  34626  coinfliplem  34737  signsplypnf  34808  signslema  34820  signstfvc  34832  signstfveq0  34835  fsum2dsub  34865  reprlt  34877  reprgt  34879  reprinfz1  34880  breprexplemc  34890  lpadmax  34943  lpadright  34945  usgrgt2cycl  35444  acycgr1v  35463  erdszelem8  35512  erdsze2lem2  35518  cvmliftlem7  35605  snmlff  35643  bcprod  36052  poimirlem3  38086  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem13  38096  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem23  38106  poimirlem24  38107  poimirlem25  38108  poimirlem26  38109  poimirlem29  38112  poimirlem30  38113  poimirlem31  38114  rrnequiv  38298  lcmineqlem17  42626  lcmineqlem21  42630  3lexlogpow5ineq5  42641  aks4d1p1p4  42652  aks4d1p1p7  42655  aks4d1p3  42659  aks4d1p7d1  42663  aks6d1c1  42697  aks6d1c3  42704  aks6d1c2lem4  42708  hashnexinj  42709  aks6d1c2  42711  aks6d1c5lem1  42717  aks6d1c5lem3  42718  aks6d1c5lem2  42719  aks6d1c5  42720  2np3bcnp1  42725  2ap1caineq  42726  sticksstones6  42732  sticksstones7  42733  sticksstones22  42749  aks6d1c6lem3  42753  aks6d1c6lem4  42754  bcled  42759  bcle2d  42760  aks6d1c7lem1  42761  aks6d1c7lem2  42762  unitscyglem1  42776  unitscyglem4  42779  aks5lem8  42782  frlmvscadiccat  43092  fltnltalem  43208  eldioph2lem1  43305  pell1qrge1  43411  rmxypos  43488  ltrmynn0  43489  ltrmxnn0  43490  lermxnn0  43491  jm2.24nn  43500  jm2.24  43504  jm2.19  43534  jm2.26lem3  43542  jm2.27c  43548  hbt  43671  dgraa0p  43690  binomcxplemnn0  44889  fsumnncl  46112  mccllem  46137  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnxpaek  46480  dvnmul  46481  dvnprodlem2  46485  stoweidlem17  46555  stoweidlem24  46562  wallispilem5  46607  stirlinglem15  46626  fourierdlem48  46692  fourierdlem83  46727  fourierdlem103  46747  fourierdlem104  46748  sqwvfoura  46766  elaa2lem  46771  etransclem10  46782  etransclem19  46791  etransclem20  46792  etransclem21  46793  etransclem22  46794  etransclem23  46795  etransclem24  46796  etransclem27  46799  etransclem32  46804  etransclem35  46807  etransclem44  46816  etransclem45  46817  etransclem46  46818  etransclem47  46819  etransclem48  46820  etransc  46821  rrndistlt  46828  chnsubseqwl  47419  chnsubseq  47420  fmtnoge3  48103  sqrtpwpw2p  48111  fmtnosqrt  48112  flsqrt  48166  lighneallem4a  48181  ssnn0ssfz  48935  pgrple2abl  48951  nn0eo  49114  fllog2  49154  itcovalt2lem2lem1  49259  aacllem  50386