Theorem nn0red 11229

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898  df-n0 11170

This theorem is referenced by:  nn0cnd  11230  nn0readdcl  11234  eluzmn  11570  flmulnn0  12490  quoremz  12516  quoremnn0ALT  12518  modaddmodup  12595  modaddmodlo  12596  expneg  12730  expnbnd  12855  facdiv  12936  faclbnd6  12948  hashdom  13029  hashun2  13033  hashunx  13036  hashfun  13084  hashf1  13098  seqcoll2  13106  hashge2el2dif  13117  hashtpg  13121  wrdlenge2n0  13196  ccatsymb  13219  ccatrn  13225  ccatalpha  13228  ccat2s1fvw  13267  swrdnd  13284  swrdccat3blem  13346  cshwidxmod  13400  repswcshw  13409  swrds2  13533  modfsummods  14366  climcnds  14422  geomulcvg  14446  mertenslem1  14455  binomfallfaclem2  14610  binomrisefac  14612  fallfacval4  14613  efcllem  14647  eftlub  14678  ruclem10  14807  oddge22np1  14911  nn0oddm1d2  14939  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  sadcaddlem  15017  sadaddlem  15026  sadasslem  15030  sadeq  15032  smuval2  15042  smupvallem  15043  smueqlem  15050  bezoutlem3  15096  bezoutlem4  15097  gcdzeq  15109  dvdssqlem  15117  nn0seqcvgd  15121  eucalglt  15136  lcmneg  15154  mulgcddvds  15207  qredeu  15210  prmdiveq  15329  odzdvds  15338  pythagtriplem3  15361  pythagtriplem6  15364  pythagtriplem7  15365  iserodd  15378  pclem  15381  pcpremul  15386  pcidlem  15414  pcgcd1  15419  pc2dvds  15421  pcz  15423  pcprmpw2  15424  fldivp1  15439  pcfaclem  15440  pcfac  15441  pcbc  15442  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  4sqlem11  15497  4sqlem12  15498  4sqlem14  15500  vdwlem11  15533  vdwlem12  15534  ramlb  15561  0ram  15562  ram0  15564  ramub1lem2  15569  ramcl  15571  psgnunilem2  17738  odmodnn0  17782  mndodconglem  17783  mndodcong  17784  oddvds  17789  odhash3  17814  gexdvds  17822  sylow1lem1  17836  sylow1lem5  17840  pgpfi  17843  pgpssslw  17852  efgsfo  17975  efgredlemd  17980  efgredlem  17983  efgred  17984  lt6abl  18119  telgsums  18213  pgpfaclem2  18304  srgbinomlem3  18365  psrbaglesupp  19189  mplmonmul  19285  coe1tmmul2  19467  coe1tmmul2fv  19469  coe1pwmulfv  19471  gsummoncoe1  19495  zringlpirlem3  19653  fvmptnn04if  20473  fvmptnn04ifc  20476  fvmptnn04ifd  20477  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  lebnumii  22573  dyadmaxlem  23171  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mdegmullem  23642  coe1mul3  23663  coe1mul4  23664  deg1sublt  23674  deg1mul2  23678  deg1tmle  23681  deg1tm  23682  ply1divmo  23699  ply1divex  23700  deg1submon1p  23716  dvdsq1p  23724  fta1glem2  23730  fta1blem  23732  plyco0  23752  plyeq0lem  23770  plypf1  23772  plyaddlem1  23773  coeeulem  23784  dgrub  23794  dgrlb  23796  dgreq  23804  coeaddlem  23809  coemullem  23810  coemulhi  23814  dgrlt  23826  dgradd2  23828  dgrmul  23830  dgrcolem2  23834  dgrco  23835  plydivlem3  23854  plydivlem4  23855  plydivex  23856  plydiveu  23857  fta1lem  23866  quotcan  23868  vieta1lem2  23870  radcnvlem1  23971  dvradcnv  23979  leibpilem1  24467  leibpi  24469  log2tlbnd  24472  birthdaylem2  24479  birthdaylem3  24480  fsumharmonic  24538  dmlogdmgm  24550  basellem3  24609  basellem5  24611  issqf  24662  ppip1le  24687  ppiltx  24703  mumullem2  24706  sgmppw  24722  ppiub  24729  chtublem  24736  chpub  24745  dchrabs  24785  bcmono  24802  bcmax  24803  bcp1ctr  24804  bclbnd  24805  bposlem5  24813  gausslemma2dlem0h  24888  gausslemma2dlem4  24894  gausslemma2dlem6  24897  lgseisenlem1  24900  2lgsoddprmlem2  24934  2sqlem7  24949  2sqlem8  24951  chebbnd1lem1  24958  chtppilimlem1  24962  dchrisum0re  25002  mulogsumlem  25020  selberg2lem  25039  pntrlog2bndlem4  25069  pntlemr  25091  pntlemj  25092  pnt  25103  ostth2lem3  25124  spthispth  26103  wwlknred  26251  wwlkextproplem2  26270  vdgrfival  26424  nbhashuvtx1  26442  rusgranumwlks  26483  eupap1  26503  eupath2lem3  26506  frghash2spot  26590  usgreghash2spotv  26593  numclwwlk5  26639  numclwwlk6  26640  friendshipgt3  26648  nndiffz1  28936  2sqmod  28979  nexple  29399  oddpwdc  29743  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemb  29757  coinfliplem  29867  signsplypnf  29953  signslema  29965  signstfvc  29977  signstfveq0  29980  erdszelem8  30434  erdsze2lem2  30440  cvmliftlem7  30527  snmlff  30565  bcprod  30877  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  rrnequiv  32804  eldioph2lem1  36341  pell1qrge1  36452  rmxypos  36532  ltrmynn0  36533  ltrmxnn0  36534  lermxnn0  36535  jm2.24nn  36544  jm2.24  36548  jm2.19  36578  jm2.26lem3  36586  jm2.27c  36592  hbt  36719  dgraa0p  36738  binomcxplemnn0  37570  fsumnncl  38638  mccllem  38664  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnxpaek  38832  dvnmul  38833  dvnprodlem2  38837  stoweidlem17  38910  stoweidlem24  38917  wallispilem5  38962  stirlinglem15  38981  fourierdlem48  39047  fourierdlem83  39082  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  elaa2lem  39126  etransclem10  39137  etransclem19  39146  etransclem20  39147  etransclem21  39148  etransclem22  39149  etransclem23  39150  etransclem24  39151  etransclem27  39154  etransclem32  39159  etransclem35  39162  etransclem44  39171  etransclem45  39172  etransclem46  39173  etransclem47  39174  etransclem48  39175  etransc  39176  rrndistlt  39186  fmtnoge3  39980  sqrtpwpw2p  39988  fmtnosqrt  39989  flsqrt  40046  lighneallem4a  40063  pfxsuffeqwrdeq  40269  vtxdgfival  40685  vtxdfiun  40697  crctcsh  41027  wwlksnred  41098  wwlksnextproplem2  41116  rusgrnumwwlks  41177  eupth2lems  41406  eucrct2eupth  41413  frgrhash2wsp  41497  fusgreghash2wspv  41499  av-numclwwlk5  41542  av-numclwwlk6  41544  av-friendshipgt3  41552  ssnn0ssfz  41920  pgrple2abl  41940  nn0eo  42116  fllog2  42160  aacllem  42356