Theorem nn0re 11900

Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0re	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Proof of Theorem nn0re

Step	Hyp	Ref	Expression
1		nn0ssre 11895	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3962	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2110  ℝcr 10530  ℕ₀cn0 11891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-nn 11633  df-n0 11892

This theorem is referenced by:  nn0ge0  11916  nn0nlt0  11917  nn0le0eq0  11919  nn0p1gt0  11920  elnnnn0c  11936  nn0addge1  11937  nn0addge2  11938  nn0sub  11941  ltsubnn0  11942  nn0negleid  11943  difgtsumgt  11944  nn0n0n1ge2b  11957  nn0ge2m1nn  11958  nn0nndivcl  11960  xnn0xr  11966  nn0nepnf  11969  xnn0nemnf  11972  elznn0nn  11989  nn0lt2  12039  nn0le2is012  12040  nn0ge0div  12045  nn01to3  12335  xnn0xaddcl  12622  xnn0lem1lt  12631  xnn0lenn0nn0  12632  xnn0xadd0  12634  nn0rp0  12837  xnn0xrge0  12885  nn0fz0  12999  elfz0fzfz0  13006  fz0fzelfz0  13007  fz0fzdiffz0  13010  fzctr  13013  difelfzle  13014  difelfznle  13015  fvffz0  13019  fzoun  13068  nn0p1elfzo  13074  elfzo0le  13075  fzonmapblen  13077  fzofzim  13078  elincfzoext  13089  elfzodifsumelfzo  13097  fzonn0p1  13108  fzonn0p1p1  13110  ssfzoulel  13125  ubmelm1fzo  13127  elfznelfzo  13136  fvinim0ffz  13150  subfzo0  13153  adddivflid  13182  divfl0  13188  fldivnn0le  13196  flltdivnn0lt  13197  quoremnn0ALT  13219  modmuladdnn0  13277  addmodid  13281  modifeq2int  13295  modfzo0difsn  13305  modsumfzodifsn  13306  addmodlteq  13308  ssnn0fi  13347  fsuppmapnn0fiub0  13355  suppssfz  13356  nn0sq11  13491  bernneq  13584  bernneq3  13586  facwordi  13643  faclbnd  13644  faclbnd3  13646  faclbnd5  13652  faclbnd6  13653  facubnd  13654  facavg  13655  bcval4  13661  bcval5  13672  bcpasc  13675  hashbnd  13690  hashnnn0genn0  13697  hashnemnf  13698  hashclb  13713  hashneq0  13719  hashsdom  13736  hashunsnggt  13749  fi1uzind  13849  brfi1indALT  13852  ccat0  13923  ccat2s1fvw  13992  ccat2s1fvwOLD  13993  swrdnd0  14013  swrdsbslen  14020  swrdspsleq  14021  pfxnd0  14044  swrdswrdlem  14060  swrdswrd  14061  swrdccatin1  14081  pfxccatin12lem2  14087  pfxccatin12lem3  14088  pfxccat3  14090  swrdccat  14091  pfxccat3a  14094  swrdccat3blem  14095  repswswrd  14140  2cshw  14169  cshweqrep  14177  cshwcsh2id  14184  2swrd2eqwrdeq  14309  nn0sqeq1  14630  isercoll  15018  o1fsum  15162  geomulcvg  15226  rerisefaccl  15365  refallfaccl  15366  rprisefaccl  15371  dvdseq  15658  oddge22np1  15692  nn0ehalf  15723  nn0o1gt2  15726  nn0o  15728  nn0oddm1d2  15730  bitsfi  15780  bitsinv1  15785  gcdn0gt0  15860  nn0gcdid0  15863  absmulgcd  15891  nn0seqcvgd  15908  algcvgblem  15915  algcvga  15917  lcmgcdnn  15949  lcmfun  15983  lcmfass  15984  prmfac1  16057  prmndvdsfaclt  16061  nonsq  16093  hashgcdlem  16119  odzdvds  16126  iserodd  16166  pcprendvds  16171  pcdvdsb  16199  pcidlem  16202  dvdsprmpweqle  16216  difsqpwdvds  16217  pcfaclem  16228  prmunb  16244  ramtcl2  16341  ramubcl  16348  ram0  16352  ramub1lem1  16356  cshwshashlem2  16424  smndex1iidm  18060  sylow1lem1  18717  pgpssslw  18733  efgsfo  18859  efgred  18868  telgsums  19107  psrbagcon  20145  gsumbagdiaglem  20149  psrridm  20178  coe1tmmul2  20438  gsummoncoe1  20466  prmirredlem  20634  prmirred  20636  mp2pm2mplem4  21411  fvmptnn04ifb  21453  chfacfisf  21456  chfacfisfcpmat  21457  chfacffsupp  21458  chfacfscmul0  21460  chfacfpmmul0  21464  dyaddisj  24191  mdegle0  24665  deg1nn0clb  24678  deg1ge  24686  deg1tmle  24705  ply1divex  24724  plyco0  24776  coeeulem  24808  coeaddlem  24833  coe1termlem  24842  dgreq0  24849  dgrlt  24850  plydivex  24880  aannenlem1  24911  taylfvallem1  24939  tayl0  24944  radcnvlem1  24995  radcnvlem2  24996  dvradcnv  25003  leibpi  25514  log2tlbnd  25517  birthdaylem3  25525  zetacvg  25586  basellem2  25653  basellem3  25654  chpp1  25726  bcmono  25847  bcmax  25848  lgsdinn0  25915  2lgslem1c  25963  2sq2  26003  2sqreulem1  26016  2sqreultlem  26017  dchrisumlem1  26059  ostth2lem2  26204  nbusgrvtxm1  27155  upgrewlkle2  27382  pthdlem1  27541  crctcshwlkn0lem4  27585  crctcshwlkn0  27593  crctcsh  27596  wwlksm1edg  27653  wwlksnred  27664  wwlksnredwwlkn  27667  wwlksnredwwlkn0  27668  wwlksnextwrd  27669  wwlksnextfun  27670  wwlksnextinj  27671  wwlksnextproplem1  27682  wwlksnextproplem2  27683  wwlksnextproplem3  27684  clwlkclwwlklem2a1  27764  clwlkclwwlklem2a2  27765  clwlkclwwlklem2fv1  27767  clwlkclwwlklem2fv2  27768  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwlkclwwlklem2  27772  clwlkclwwlk  27774  clwlkclwwlk2  27775  clwlkclwwlkf  27780  clwwisshclwwslem  27786  clwwlkel  27819  wwlksext2clwwlk  27830  clwlknf1oclwwlknlem1  27854  clwwlknonex2lem2  27881  eupth2lems  28011  eupth2  28012  eucrctshift  28016  numclwwlk7  28164  frgrreggt1  28166  frgrreg  28167  frgrogt3nreg  28170  friendship  28172  nn0xmulclb  30490  dpcl  30562  wrdt2ind  30622  hasheuni  31339  eulerpartlems  31613  hgt750lem  31917  0nn0m1nnn0  32346  derangen  32414  faclimlem1  32970  poimirlem28  34914  rrntotbnd  35108  nacsfix  39302  eldioph2lem1  39350  irrapxlem4  39415  pell14qrgt0  39449  pell1qrgaplem  39463  pellqrexplicit  39467  rmxycomplete  39507  jm2.17a  39550  jm2.17b  39551  rmygeid  39554  jm2.22  39585  rmxdiophlem  39605  hbtlem5  39721  hbt  39723  fperiodmullem  41563  dvnxpaek  42220  stoweidlem17  42296  wallispilem3  42346  stirlinglem5  42357  stirlinglem7  42359  fourierdlem16  42402  fourierdlem21  42407  fourierdlem22  42408  fourierdlem83  42468  fourierdlem112  42497  elaa2lem  42512  etransclem23  42536  zm1nn  43496  nn0resubcl  43502  fz0addge0  43513  elfzlble  43514  subsubelfzo0  43520  2ffzoeq  43522  iccpartigtl  43577  lswn0  43598  sqrtpwpw2p  43694  fmtnodvds  43700  goldbachth  43703  odz2prm2pw  43719  flsqrt  43750  nn0e  43856  nn0sumltlt  44392  ply1mulgsumlem2  44435  nn0eo  44582  flnn0div2ge  44587  fllog2  44622  dignn0fr  44655  digexp  44661  dig2nn0  44665  0dig2nn0e  44666  dig2bits  44668