Theorem nn0re 12540

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11126  ℕ₀cn0 12531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-nn 12261  df-n0 12532

This theorem is used by:  nn0ge0  12556  nn0nlt0  12557  nn0le0eq0  12559  nn0p1gt0  12560  elnnnn0c  12576  nn0addge1  12577  nn0addge2  12578  nn0sub  12581  ltsubnn0  12582  nn0negleid  12583  difgtsumgt  12584  nn0le2x  12585  nn0n0n1ge2b  12600  nn0ge2m1nn  12601  nn0nndivcl  12603  xnn0xr  12609  nn0nepnf  12612  xnn0nemnf  12615  elznn0nn  12632  0nn0m1nnn0  12678  nn0lt2  12687  nn0le2is012  12688  nn0ge0div  12693  nn01to3  12993  xnn0xaddcl  13290  xnn0lem1lt  13299  xnn0lenn0nn0  13300  xnn0xadd0  13302  nn0rp0  13511  xnn0xrge0  13562  nn0fz0  13683  elfz0fzfz0  13691  fz0fzelfz0  13692  fz0fzdiffz0  13695  fzctr  13698  difelfzle  13699  difelfznle  13700  fvffz0  13704  fzoun  13755  nn0p1elfzo  13761  elfzo0le  13762  fzonmapblen  13767  fzofzim  13768  elincfzoext  13782  elfzodifsumelfzo  13790  fzonn0p1  13801  fzonn0p1p1  13803  ssfzoulel  13819  ubmelm1fzo  13822  elfznelfzo  13832  fvinim0ffz  13848  subfzo0  13852  adddivflid  13882  divfl0  13888  fldivnn0le  13896  flltdivnn0lt  13897  quoremnn0ALT  13921  modmuladdnn0  13982  addmodid  13986  modifeq2int  14000  modfzo0difsn  14010  modsumfzodifsn  14011  addmodlteq  14013  ssnn0fi  14052  fsuppmapnn0fiub0  14060  suppssfz  14061  nn0sq11  14199  bernneq  14296  bernneq3  14298  facwordi  14356  faclbnd  14357  faclbnd3  14359  faclbnd5  14365  faclbnd6  14366  facubnd  14367  facavg  14368  bcval4  14374  bcval5  14385  bcpasc  14388  hashbnd  14403  hashnnn0genn0  14410  hashnemnf  14411  hashclb  14425  hashneq0  14431  hashsdom  14448  hashunsnggt  14461  fi1uzind  14575  ccat0  14644  ccat2s1fvw  14709  swrdnd0  14730  swrdsbslen  14737  swrdspsleq  14738  pfxnd0  14761  swrdswrdlem  14776  swrdswrd  14777  swrdccatin1  14797  pfxccatin12lem2  14803  pfxccatin12lem3  14804  pfxccat3  14806  swrdccat  14807  pfxccat3a  14810  swrdccat3blem  14811  repswswrd  14858  2cshw  14887  cshweqrep  14895  cshwcsh2id  14902  2swrd2eqwrdeq  15029  nn0sqeq1  15366  nn0absid  15520  isercoll  15758  o1fsum  15903  geomulcvg  15968  rerisefaccl  16107  refallfaccl  16108  rprisefaccl  16113  dvdseq  16407  oddge22np1  16442  nn0ehalf  16471  nn0o1gt2  16474  nn0o  16476  nn0oddm1d2  16478  bitsfi  16530  bitsinv1  16535  gcdn0gt0  16611  nn0gcdid0  16614  absmulgcd  16642  nn0seqcvgd  16663  algcvgblem  16670  algcvga  16672  lcmgcdnn  16704  lcmfun  16738  lcmfass  16739  prmfac1  16814  prmndvdsfaclt  16819  nonsq  16853  hashgcdlem  16882  odzdvds  16890  iserodd  16930  pcprendvds  16935  pcdvdsb  16964  pcidlem  16967  dvdsprmpweqle  16981  difsqpwdvds  16982  pcfaclem  16993  prmunb  17009  ramtcl2  17106  ramubcl  17113  ram0  17117  ramub1lem1  17121  cshwshashlem2  17191  smndex1iidm  19013  sylow1lem1  19728  pgpssslw  19744  efgsfo  19869  efgred  19878  telgsums  20123  prmirredlem  21688  prmirred  21690  gsumbagdiaglem  22149  psrridm  22180  psdmul  22397  coe1tmmul2  22505  gsummoncoe1  22536  mp2pm2mplem4  23037  fvmptnn04ifb  23079  chfacfisf  23082  chfacfisfcpmat  23083  chfacffsupp  23084  chfacfscmul0  23086  chfacfpmmul0  23090  dyaddisj  25827  mdegle0  26305  deg1nn0clb  26318  deg1ge  26326  deg1tmle  26346  ply1divex  26365  plyco0  26420  coeeulem  26453  coeaddlem  26478  coe1termlem  26487  dgreq0  26494  dgrlt  26495  plydivex  26530  aannenlem1  26567  taylfvallem1  26596  tayl0  26601  radcnvlem1  26652  radcnvlem2  26653  dvradcnv  26660  leibpi  27182  log2tlbnd  27185  birthdaylem3  27193  zetacvg  27254  basellem2  27321  basellem3  27322  chpp1  27394  bcmono  27516  bcmax  27517  lgsdinn0  27584  2lgslem1c  27632  2sq2  27672  2sqreulem1  27685  2sqreultlem  27686  dchrisumlem1  27728  ostth2lem2  27873  nbusgrvtxm1  29842  upgrewlkle2  30069  pthdlem1  30234  crctcshwlkn0lem4  30284  crctcshwlkn0  30292  crctcsh  30295  wwlksm1edg  30352  wwlksnred  30363  wwlksnredwwlkn  30366  wwlksnredwwlkn0  30367  wwlksnextwrd  30368  wwlksnextfun  30369  wwlksnextinj  30370  wwlksnextproplem1  30380  wwlksnextproplem2  30381  wwlksnextproplem3  30382  clwlkclwwlklem2a1  30465  clwlkclwwlklem2a2  30466  clwlkclwwlklem2fv1  30468  clwlkclwwlklem2fv2  30469  clwlkclwwlklem2a4  30470  clwlkclwwlklem2a  30471  clwlkclwwlklem2  30473  clwlkclwwlk  30475  clwlkclwwlk2  30476  clwlkclwwlkf  30481  clwwisshclwwslem  30487  clwwlkel  30519  wwlksext2clwwlk  30530  clwlknf1oclwwlknlem1  30554  clwwlknonex2lem2  30581  eupth2lems  30721  eupth2  30722  eucrctshift  30726  numclwwlk7  30874  frgrreggt1  30876  frgrreg  30877  frgrogt3nreg  30880  friendship  30882  nn0mnfxrd  33225  nn0xmulclb  33245  dpcl  33339  wrdt2ind  33398  hasheuni  34598  eulerpartlems  34874  hgt750lem  35162  derangen  35754  faclimlem1  36325  poimirlem28  38400  rrntotbnd  38589  sticksstones22  43037  gcdnn0id  43207  nn0addcom  43353  zaddcomlem  43354  nn0mulcom  43357  nacsfix  43560  eldioph2lem1  43608  irrapxlem4  43669  pell14qrgt0  43703  pell1qrgaplem  43717  pellqrexplicit  43721  rmxycomplete  43761  jm2.17a  43804  jm2.17b  43805  rmygeid  43808  jm2.22  43839  rmxdiophlem  43859  hbtlem5  43972  hbt  43974  fperiodmullem  46139  dvnxpaek  46773  stoweidlem17  46848  wallispilem3  46898  stirlinglem5  46909  stirlinglem7  46911  fourierdlem16  46954  fourierdlem21  46959  fourierdlem22  46960  fourierdlem83  47020  fourierdlem112  47049  elaa2lem  47064  etransclem23  47088  zm1nn  48193  nn0resubcl  48199  fz0addge0  48210  elfzlble  48211  subsubelfzo0  48218  2ffzoeq  48219  addmodne  48241  submodlt  48247  iccpartigtl  48326  lswn0  48347  sqrtpwpw2p  48444  fmtnodvds  48450  goldbachth  48453  odz2prm2pw  48469  flsqrt  48499  nn0e  48616  nn0sumltlt  49283  ply1mulgsumlem2  49320  nn0eo  49461  flnn0div2ge  49466  fllog2  49501  dignn0fr  49534  digexp  49540  dig2nn0  49544  0dig2nn0e  49545  dig2bits  49547  itcovalt2lem2lem1  49606