Theorem nn0red 12277

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 10854  ℕ₀cn0 12216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-nn 11957  df-n0 12217

This theorem is referenced by:  nn0cnd  12278  nn0readdcl  12282  eluzmn  12571  flmulnn0  13528  quoremz  13556  quoremnn0ALT  13558  modaddmodup  13635  modaddmodlo  13636  expneg  13771  expnbnd  13928  facdiv  13982  faclbnd6  13994  hashdom  14075  hashun2  14079  hashunx  14082  hashfun  14133  hashf1  14152  seqcoll2  14160  hashge2el2dif  14175  hashtpg  14180  wrdlenge2n0  14236  ccatsymb  14268  ccatrn  14275  ccatalpha  14279  ccat2s1fvw  14330  ccat2s1fvwOLD  14331  swrdnd  14348  swrdnd0  14351  pfxnd0  14382  pfxsuffeqwrdeq  14392  swrdccat3blem  14433  cshwidxmod  14497  repswcshw  14506  swrds2  14634  modfsummods  15486  climcnds  15544  geomulcvg  15569  mertenslem1  15577  binomfallfaclem2  15731  binomrisefac  15733  fallfacval4  15734  efcllem  15768  eftlub  15799  ruclem10  15929  oddge22np1  16039  nn0oddm1d2  16075  divalglem5  16087  bitsfzolem  16122  bitsfzo  16123  bitsmod  16124  sadcaddlem  16145  sadaddlem  16154  sadasslem  16158  sadeq  16160  smuval2  16170  smupvallem  16171  smueqlem  16178  bezoutlem3  16230  bezoutlem4  16231  gcdzeq  16243  dvdssqlem  16252  nn0seqcvgd  16256  eucalglt  16271  lcmneg  16289  mulgcddvds  16341  qredeu  16344  prmdiveq  16468  odzdvds  16477  pythagtriplem3  16500  pythagtriplem6  16503  pythagtriplem7  16504  iserodd  16517  pclem  16520  pcpremul  16525  pcidlem  16554  pcgcd1  16559  pc2dvds  16561  pcz  16563  pcprmpw2  16564  fldivp1  16579  pcfaclem  16580  pcfac  16581  pcbc  16582  prmreclem2  16599  prmreclem3  16600  prmreclem4  16601  prmreclem5  16602  4sqlem11  16637  4sqlem12  16638  4sqlem14  16640  vdwlem11  16673  vdwlem12  16674  ramlb  16701  0ram  16702  ram0  16704  ramub1lem2  16709  ramcl  16711  psgnunilem2  19084  odmodnn0  19129  mndodconglem  19130  mndodcong  19131  oddvds  19136  odhash3  19162  gexdvds  19170  sylow1lem1  19184  sylow1lem5  19188  pgpfi  19191  pgpssslw  19200  efgsfo  19326  efgredlemd  19331  efgredlem  19334  efgred  19335  lt6abl  19477  telgsums  19575  pgpfaclem2  19666  srgbinomlem3  19759  zringlpirlem3  20667  psrbaglesupp  21108  psrbaglesuppOLD  21109  psrbagcon  21114  mplmonmul  21218  coe1tmmul2  21428  coe1tmmul2fv  21430  coe1pwmulfv  21432  gsummoncoe1  21456  fvmptnn04if  21979  fvmptnn04ifc  21982  fvmptnn04ifd  21983  chfacfscmulgsum  21990  chfacfpmmulgsum  21994  lebnumii  24110  dyadmaxlem  24742  mbfi1fseqlem3  24863  mbfi1fseqlem4  24864  mbfi1fseqlem5  24865  mdegmullem  25224  coe1mul3  25245  coe1mul4  25246  deg1sublt  25256  deg1mul2  25260  deg1tmle  25263  deg1tm  25264  ply1divmo  25281  ply1divex  25282  deg1submon1p  25298  dvdsq1p  25306  fta1glem2  25312  fta1blem  25314  plyco0  25334  plyeq0lem  25352  plypf1  25354  plyaddlem1  25355  coeeulem  25366  dgrub  25376  dgrlb  25378  dgreq  25386  coeaddlem  25391  coemullem  25392  coemulhi  25396  dgrlt  25408  dgradd2  25410  dgrmul  25412  dgrcolem2  25416  dgrco  25417  plydivlem3  25436  plydivlem4  25437  plydivex  25438  plydiveu  25439  fta1lem  25448  quotcan  25450  vieta1lem2  25452  radcnvlem1  25553  dvradcnv  25561  leibpi  26073  log2tlbnd  26076  birthdaylem2  26083  birthdaylem3  26084  fsumharmonic  26142  dmlogdmgm  26154  basellem3  26213  basellem5  26215  issqf  26266  ppip1le  26291  ppiltx  26307  mumullem2  26310  sgmppw  26326  ppiub  26333  chtublem  26340  chpub  26349  dchrabs  26389  bcmono  26406  bcmax  26407  bcp1ctr  26408  bclbnd  26409  bposlem5  26417  gausslemma2dlem0h  26492  gausslemma2dlem4  26498  gausslemma2dlem6  26501  lgseisenlem1  26504  2lgsoddprmlem2  26538  2sqlem7  26553  2sqlem8  26555  2sq2  26562  2sqmod  26565  chebbnd1lem1  26598  chtppilimlem1  26602  dchrisum0re  26642  mulogsumlem  26660  selberg2lem  26679  pntrlog2bndlem4  26709  pntlemr  26731  pntlemj  26732  pnt  26743  ostth2lem3  26764  vtxdgfival  27817  vtxdfiun  27830  vtxdginducedm1fi  27892  crctcsh  28168  wwlksnred  28236  wwlksnextproplem2  28254  rusgrnumwwlks  28318  eupth2lems  28581  eucrct2eupth  28588  numclwlk1lem1  28712  numclwwlk5  28731  numclwwlk6  28733  friendshipgt3  28741  nnmulge  31052  nndiffz1  31086  prmdvdsbc  31109  pfxlsw2ccat  31203  wrdt2ind  31204  cycpmrn  31389  cyc3conja  31403  nexple  31956  oddpwdc  32300  eulerpartlems  32306  eulerpartlemgc  32308  eulerpartlemb  32314  coinfliplem  32424  signsplypnf  32508  signslema  32520  signstfvc  32532  signstfveq0  32535  fsum2dsub  32566  reprlt  32578  reprgt  32580  reprinfz1  32581  breprexplemc  32591  lpadmax  32641  lpadright  32643  usgrgt2cycl  33071  acycgr1v  33090  erdszelem8  33139  erdsze2lem2  33145  cvmliftlem7  33232  snmlff  33270  bcprod  33683  poimirlem3  35759  poimirlem4  35760  poimirlem6  35762  poimirlem7  35763  poimirlem10  35766  poimirlem11  35767  poimirlem12  35768  poimirlem13  35769  poimirlem15  35771  poimirlem16  35772  poimirlem17  35773  poimirlem19  35775  poimirlem20  35776  poimirlem21  35777  poimirlem22  35778  poimirlem23  35779  poimirlem24  35780  poimirlem25  35781  poimirlem26  35782  poimirlem29  35785  poimirlem30  35786  poimirlem31  35787  rrnequiv  35972  lcmineqlem17  40033  lcmineqlem21  40037  3lexlogpow5ineq5  40048  aks4d1p1p4  40059  aks4d1p1p7  40062  aks4d1p3  40066  aks4d1p7d1  40070  2np3bcnp1  40080  2ap1caineq  40081  sticksstones6  40087  sticksstones7  40088  sticksstones22  40104  frlmvscadiccat  40217  fltnltalem  40479  eldioph2lem1  40562  pell1qrge1  40672  rmxypos  40749  ltrmynn0  40750  ltrmxnn0  40751  lermxnn0  40752  jm2.24nn  40761  jm2.24  40765  jm2.19  40795  jm2.26lem3  40803  jm2.27c  40809  hbt  40935  dgraa0p  40954  binomcxplemnn0  41920  fsumnncl  43067  mccllem  43092  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvnxpaek  43437  dvnmul  43438  dvnprodlem2  43442  stoweidlem17  43512  stoweidlem24  43519  wallispilem5  43564  stirlinglem15  43583  fourierdlem48  43649  fourierdlem83  43684  fourierdlem103  43704  fourierdlem104  43705  sqwvfoura  43723  elaa2lem  43728  etransclem10  43739  etransclem19  43748  etransclem20  43749  etransclem21  43750  etransclem22  43751  etransclem23  43752  etransclem24  43753  etransclem27  43756  etransclem32  43761  etransclem35  43764  etransclem44  43773  etransclem45  43774  etransclem46  43775  etransclem47  43776  etransclem48  43777  etransc  43778  rrndistlt  43785  fmtnoge3  44934  sqrtpwpw2p  44942  fmtnosqrt  44943  flsqrt  44997  lighneallem4a  45012  ssnn0ssfz  45637  pgrple2abl  45653  nn0eo  45826  fllog2  45866  itcovalt2lem2lem1  45971  aacllem  46457