Theorem nn0re 12225

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 12220	. 2 ⊢ ℕ0 ⊆ ℝ
2	1	sseli 3921	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ)

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:  nn0ge0  12241  nn0nlt0  12242  nn0le0eq0  12244  nn0p1gt0  12245  elnnnn0c  12261  nn0addge1  12262  nn0addge2  12263  nn0sub  12266  ltsubnn0  12267  nn0negleid  12268  difgtsumgt  12269  nn0n0n1ge2b  12284  nn0ge2m1nn  12285  nn0nndivcl  12287  xnn0xr  12293  nn0nepnf  12296  xnn0nemnf  12299  elznn0nn  12316  nn0lt2  12366  nn0le2is012  12367  nn0ge0div  12372  nn01to3  12663  xnn0xaddcl  12951  xnn0lem1lt  12960  xnn0lenn0nn0  12961  xnn0xadd0  12963  nn0rp0  13169  xnn0xrge0  13220  nn0fz0  13336  elfz0fzfz0  13343  fz0fzelfz0  13344  fz0fzdiffz0  13347  fzctr  13350  difelfzle  13351  difelfznle  13352  fvffz0  13356  fzoun  13405  nn0p1elfzo  13411  elfzo0le  13412  fzonmapblen  13414  fzofzim  13415  elincfzoext  13426  elfzodifsumelfzo  13434  fzonn0p1  13445  fzonn0p1p1  13447  ssfzoulel  13462  ubmelm1fzo  13464  elfznelfzo  13473  fvinim0ffz  13487  subfzo0  13490  adddivflid  13519  divfl0  13525  fldivnn0le  13533  flltdivnn0lt  13534  quoremnn0ALT  13558  modmuladdnn0  13616  addmodid  13620  modifeq2int  13634  modfzo0difsn  13644  modsumfzodifsn  13645  addmodlteq  13647  ssnn0fi  13686  fsuppmapnn0fiub0  13694  suppssfz  13695  nn0sq11  13832  bernneq  13925  bernneq3  13927  facwordi  13984  faclbnd  13985  faclbnd3  13987  faclbnd5  13993  faclbnd6  13994  facubnd  13995  facavg  13996  bcval4  14002  bcval5  14013  bcpasc  14016  hashbnd  14031  hashnnn0genn0  14038  hashnemnf  14039  hashclb  14054  hashneq0  14060  hashsdom  14077  hashunsnggt  14090  fi1uzind  14192  ccat0  14261  ccat2s1fvw  14330  ccat2s1fvwOLD  14331  swrdnd0  14351  swrdsbslen  14358  swrdspsleq  14359  pfxnd0  14382  swrdswrdlem  14398  swrdswrd  14399  swrdccatin1  14419  pfxccatin12lem2  14425  pfxccatin12lem3  14426  pfxccat3  14428  swrdccat  14429  pfxccat3a  14432  swrdccat3blem  14433  repswswrd  14478  2cshw  14507  cshweqrep  14515  cshwcsh2id  14522  2swrd2eqwrdeq  14647  nn0sqeq1  14969  isercoll  15360  o1fsum  15506  geomulcvg  15569  rerisefaccl  15708  refallfaccl  15709  rprisefaccl  15714  dvdseq  16004  oddge22np1  16039  nn0ehalf  16068  nn0o1gt2  16071  nn0o  16073  nn0oddm1d2  16075  bitsfi  16125  bitsinv1  16130  gcdn0gt0  16206  nn0gcdid0  16209  absmulgcd  16238  nn0seqcvgd  16256  algcvgblem  16263  algcvga  16265  lcmgcdnn  16297  lcmfun  16331  lcmfass  16332  prmfac1  16407  prmndvdsfaclt  16411  nonsq  16444  hashgcdlem  16470  odzdvds  16477  iserodd  16517  pcprendvds  16522  pcdvdsb  16551  pcidlem  16554  dvdsprmpweqle  16568  difsqpwdvds  16569  pcfaclem  16580  prmunb  16596  ramtcl2  16693  ramubcl  16700  ram0  16704  ramub1lem1  16708  cshwshashlem2  16779  smndex1iidm  18521  sylow1lem1  19184  pgpssslw  19200  efgsfo  19326  efgred  19335  telgsums  19575  prmirredlem  20675  prmirred  20677  psrbagconOLD  21115  gsumbagdiaglemOLD  21122  gsumbagdiaglem  21125  psrridm  21154  coe1tmmul2  21428  gsummoncoe1  21456  mp2pm2mplem4  21939  fvmptnn04ifb  21981  chfacfisf  21984  chfacfisfcpmat  21985  chfacffsupp  21986  chfacfscmul0  21988  chfacfpmmul0  21992  dyaddisj  24741  mdegle0  25223  deg1nn0clb  25236  deg1ge  25244  deg1tmle  25263  ply1divex  25282  plyco0  25334  coeeulem  25366  coeaddlem  25391  coe1termlem  25400  dgreq0  25407  dgrlt  25408  plydivex  25438  aannenlem1  25469  taylfvallem1  25497  tayl0  25502  radcnvlem1  25553  radcnvlem2  25554  dvradcnv  25561  leibpi  26073  log2tlbnd  26076  birthdaylem3  26084  zetacvg  26145  basellem2  26212  basellem3  26213  chpp1  26285  bcmono  26406  bcmax  26407  lgsdinn0  26474  2lgslem1c  26522  2sq2  26562  2sqreulem1  26575  2sqreultlem  26576  dchrisumlem1  26618  ostth2lem2  26763  nbusgrvtxm1  27727  upgrewlkle2  27954  pthdlem1  28113  crctcshwlkn0lem4  28157  crctcshwlkn0  28165  crctcsh  28168  wwlksm1edg  28225  wwlksnred  28236  wwlksnredwwlkn  28239  wwlksnredwwlkn0  28240  wwlksnextwrd  28241  wwlksnextfun  28242  wwlksnextinj  28243  wwlksnextproplem1  28253  wwlksnextproplem2  28254  wwlksnextproplem3  28255  clwlkclwwlklem2a1  28335  clwlkclwwlklem2a2  28336  clwlkclwwlklem2fv1  28338  clwlkclwwlklem2fv2  28339  clwlkclwwlklem2a4  28340  clwlkclwwlklem2a  28341  clwlkclwwlklem2  28343  clwlkclwwlk  28345  clwlkclwwlk2  28346  clwlkclwwlkf  28351  clwwisshclwwslem  28357  clwwlkel  28389  wwlksext2clwwlk  28400  clwlknf1oclwwlknlem1  28424  clwwlknonex2lem2  28451  eupth2lems  28581  eupth2  28582  eucrctshift  28586  numclwwlk7  28734  frgrreggt1  28736  frgrreg  28737  frgrogt3nreg  28740  friendship  28742  nn0xmulclb  31073  dpcl  31144  wrdt2ind  31204  hasheuni  32032  eulerpartlems  32306  hgt750lem  32610  0nn0m1nnn0  33050  derangen  33113  faclimlem1  33688  poimirlem28  35784  rrntotbnd  35973  sticksstones22  40104  factwoffsmonot  40143  gcdnn0id  40309  nacsfix  40514  eldioph2lem1  40562  irrapxlem4  40627  pell14qrgt0  40661  pell1qrgaplem  40675  pellqrexplicit  40679  rmxycomplete  40719  jm2.17a  40762  jm2.17b  40763  rmygeid  40766  jm2.22  40797  rmxdiophlem  40817  hbtlem5  40933  hbt  40935  fperiodmullem  42796  dvnxpaek  43437  stoweidlem17  43512  wallispilem3  43562  stirlinglem5  43573  stirlinglem7  43575  fourierdlem16  43618  fourierdlem21  43623  fourierdlem22  43624  fourierdlem83  43684  fourierdlem112  43713  elaa2lem  43728  etransclem23  43752  zm1nn  44746  nn0resubcl  44752  fz0addge0  44763  elfzlble  44764  subsubelfzo0  44770  2ffzoeq  44772  iccpartigtl  44827  lswn0  44848  sqrtpwpw2p  44942  fmtnodvds  44948  goldbachth  44951  odz2prm2pw  44967  flsqrt  44997  nn0e  45101  nn0sumltlt  45638  ply1mulgsumlem2  45680  nn0eo  45826  flnn0div2ge  45831  fllog2  45866  dignn0fr  45899  digexp  45905  dig2nn0  45909  0dig2nn0e  45910  dig2bits  45912  itcovalt2lem2lem1  45971