Theorem nn0red 12499

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-n0 12438

This theorem is referenced by:  nn0cnd  12500  nn0readdcl  12504  eluzmn  12795  flmulnn0  13786  quoremz  13814  quoremnn0ALT  13816  modaddmodup  13896  modaddmodlo  13897  expneg  14031  expnbnd  14194  facdiv  14249  faclbnd6  14261  hashdom  14341  hashun2  14345  hashunx  14348  hashfun  14399  hashf1  14419  seqcoll2  14427  hashge2el2dif  14442  hashtpg  14447  wrdlenge2n0  14514  ccatdmss  14544  ccatsymb  14545  ccatrn  14552  ccatalpha  14556  ccat2s1fvw  14601  swrdnd  14617  swrdnd0  14620  pfxnd0  14651  pfxsuffeqwrdeq  14660  swrdccat3blem  14701  cshwidxmod  14765  repswcshw  14774  swrds2  14902  modfsummods  15756  climcnds  15816  geomulcvg  15841  mertenslem1  15849  binomfallfaclem2  16005  binomrisefac  16007  fallfacval4  16008  efcllem  16042  eftlub  16076  ruclem10  16206  oddge22np1  16318  nn0oddm1d2  16354  divalglem5  16366  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  sadcaddlem  16426  sadaddlem  16435  sadasslem  16439  sadeq  16441  smuval2  16451  smupvallem  16452  smueqlem  16459  bezoutlem3  16510  bezoutlem4  16511  gcdzeq  16521  dvdssqlem  16535  nn0seqcvgd  16539  eucalglt  16554  lcmneg  16572  mulgcddvds  16624  qredeu  16627  prmdvdsbc  16696  prmdiveq  16756  odzdvds  16766  pythagtriplem3  16789  pythagtriplem6  16792  pythagtriplem7  16793  iserodd  16806  pclem  16809  pcpremul  16814  pcidlem  16843  pcgcd1  16848  pc2dvds  16850  pcz  16852  pcprmpw2  16853  fldivp1  16868  pcfaclem  16869  pcfac  16870  pcbc  16871  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  vdwlem11  16962  vdwlem12  16963  ramlb  16990  0ram  16991  ram0  16993  ramub1lem2  16998  ramcl  17000  psgnunilem2  19470  odmodnn0  19515  mndodconglem  19516  mndodcong  19517  oddvds  19522  odhash3  19551  gexdvds  19559  sylow1lem1  19573  sylow1lem5  19577  pgpfi  19580  pgpssslw  19589  efgsfo  19714  efgredlemd  19719  efgredlem  19722  efgred  19723  lt6abl  19870  telgsums  19968  pgpfaclem2  20059  srgbinomlem3  20209  zringlpirlem3  21444  psrbaglesupp  21902  psrbagcon  21905  psrbagleadd1  21908  mplmonmul  22014  psdmul  22132  coe1tmmul2  22241  coe1tmmul2fv  22243  coe1pwmulfv  22245  gsummoncoe1  22273  fvmptnn04if  22814  fvmptnn04ifc  22817  fvmptnn04ifd  22818  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  lebnumii  24933  dyadmaxlem  25564  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mdegmullem  26043  coe1mul3  26064  coe1mul4  26065  deg1sublt  26075  deg1mul2  26079  deg1tmle  26083  deg1tm  26084  ply1divmo  26101  ply1divex  26102  deg1submon1p  26118  dvdsq1p  26128  fta1glem2  26134  fta1blem  26136  plyco0  26157  plyeq0lem  26175  plypf1  26177  plyaddlem1  26178  coeeulem  26189  dgrub  26199  dgrlb  26201  dgreq  26209  coeaddlem  26214  coemullem  26215  coemulhi  26219  dgrlt  26231  dgradd2  26233  dgrmul  26235  dgrcolem2  26239  dgrco  26240  plydivlem3  26261  plydivlem4  26262  plydivex  26263  plydiveu  26264  fta1lem  26273  quotcan  26275  vieta1lem2  26277  radcnvlem1  26378  dvradcnv  26386  leibpi  26906  log2tlbnd  26909  birthdaylem2  26916  birthdaylem3  26917  fsumharmonic  26975  dmlogdmgm  26987  basellem3  27046  basellem5  27048  issqf  27099  ppip1le  27124  ppiltx  27140  mumullem2  27143  sgmppw  27160  ppiub  27167  chtublem  27174  chpub  27183  dchrabs  27223  bcmono  27240  bcmax  27241  bcp1ctr  27242  bclbnd  27243  bposlem5  27251  gausslemma2dlem0h  27326  gausslemma2dlem4  27332  gausslemma2dlem6  27335  lgseisenlem1  27338  2lgsoddprmlem2  27372  2sqlem7  27387  2sqlem8  27389  2sq2  27396  2sqmod  27399  chebbnd1lem1  27432  chtppilimlem1  27436  dchrisum0re  27476  mulogsumlem  27494  selberg2lem  27513  pntrlog2bndlem4  27543  pntlemr  27565  pntlemj  27566  pnt  27577  ostth2lem3  27598  vtxdgfival  29538  vtxdfiun  29551  vtxdginducedm1fi  29613  crctcsh  29892  wwlksnred  29960  wwlksnextproplem2  29978  rusgrnumwwlks  30045  eupth2lems  30308  eucrct2eupth  30315  numclwlk1lem1  30439  numclwwlk5  30458  numclwwlk6  30460  friendshipgt3  30468  nnmulge  32812  nndiffz1  32859  fzo0opth  32876  suppssnn0  32878  pfxlsw2ccat  33010  wrdt2ind  33013  gsumwrd2dccatlem  33138  cycpmrn  33204  cyc3conja  33218  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  ply1unit  33635  ply1dg3rt0irred  33644  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  psrmonmul  33694  esplyfval2  33709  esplyfval3  33716  exsslsb  33741  ply1degltdimlem  33766  ply1degltdim  33767  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  extdgfialglem1  33836  minplyirredlem  33854  irredminply  33860  nn0constr  33905  iconstr  33910  cos9thpiminplylem1  33926  oddpwdc  34498  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemb  34512  coinfliplem  34623  signsplypnf  34694  signslema  34706  signstfvc  34718  signstfveq0  34721  fsum2dsub  34751  reprlt  34763  reprgt  34765  reprinfz1  34766  breprexplemc  34776  lpadmax  34826  lpadright  34828  usgrgt2cycl  35312  acycgr1v  35331  erdszelem8  35380  erdsze2lem2  35386  cvmliftlem7  35473  snmlff  35511  bcprod  35920  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  rrnequiv  38156  lcmineqlem17  42484  lcmineqlem21  42488  3lexlogpow5ineq5  42499  aks4d1p1p4  42510  aks4d1p1p7  42513  aks4d1p3  42517  aks4d1p7d1  42521  aks6d1c1  42555  aks6d1c3  42562  aks6d1c2lem4  42566  hashnexinj  42567  aks6d1c2  42569  aks6d1c5lem1  42575  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c5  42578  2np3bcnp1  42583  2ap1caineq  42584  sticksstones6  42590  sticksstones7  42591  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c6lem4  42612  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  unitscyglem1  42634  unitscyglem4  42637  aks5lem8  42640  frlmvscadiccat  42951  fltnltalem  43095  eldioph2lem1  43192  pell1qrge1  43298  rmxypos  43375  ltrmynn0  43376  ltrmxnn0  43377  lermxnn0  43378  jm2.24nn  43387  jm2.24  43391  jm2.19  43421  jm2.26lem3  43429  jm2.27c  43435  hbt  43558  dgraa0p  43577  binomcxplemnn0  44776  fsumnncl  46002  mccllem  46027  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnmul  46371  dvnprodlem2  46375  stoweidlem17  46445  stoweidlem24  46452  wallispilem5  46497  stirlinglem15  46516  fourierdlem48  46582  fourierdlem83  46617  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  elaa2lem  46661  etransclem10  46672  etransclem19  46681  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem27  46689  etransclem32  46694  etransclem35  46697  etransclem44  46706  etransclem45  46707  etransclem46  46708  etransclem47  46709  etransclem48  46710  etransc  46711  rrndistlt  46718  chnsubseqwl  47309  chnsubseq  47310  fmtnoge3  47993  sqrtpwpw2p  48001  fmtnosqrt  48002  flsqrt  48056  lighneallem4a  48071  ssnn0ssfz  48825  pgrple2abl  48841  nn0eo  49004  fllog2  49044  itcovalt2lem2lem1  49149  aacllem  50276