Theorem nn0re 12528

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11114  ℕ₀cn0 12519

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-i2m1 11183  ax-1ne0 11184  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12249  df-n0 12520

This theorem is used by:  nn0ge0  12544  nn0nlt0  12545  nn0le0eq0  12547  nn0p1gt0  12548  elnnnn0c  12564  nn0addge1  12565  nn0addge2  12566  nn0sub  12569  ltsubnn0  12570  nn0negleid  12571  difgtsumgt  12572  nn0le2x  12573  nn0n0n1ge2b  12588  nn0ge2m1nn  12589  nn0nndivcl  12591  xnn0xr  12597  nn0nepnf  12600  xnn0nemnf  12603  elznn0nn  12620  0nn0m1nnn0  12666  nn0lt2  12675  nn0le2is012  12676  nn0ge0div  12681  nn01to3  12981  xnn0xaddcl  13277  xnn0lem1lt  13286  xnn0lenn0nn0  13287  xnn0xadd0  13289  nn0rp0  13498  xnn0xrge0  13549  nn0fz0  13670  elfz0fzfz0  13678  fz0fzelfz0  13679  fz0fzdiffz0  13682  fzctr  13685  difelfzle  13686  difelfznle  13687  fvffz0  13691  fzoun  13742  nn0p1elfzo  13748  elfzo0le  13749  fzonmapblen  13754  fzofzim  13755  elincfzoext  13769  elfzodifsumelfzo  13777  fzonn0p1  13788  fzonn0p1p1  13790  ssfzoulel  13806  ubmelm1fzo  13809  elfznelfzo  13819  fvinim0ffz  13835  subfzo0  13839  adddivflid  13869  divfl0  13875  fldivnn0le  13883  flltdivnn0lt  13884  quoremnn0ALT  13908  modmuladdnn0  13969  addmodid  13973  modifeq2int  13987  modfzo0difsn  13997  modsumfzodifsn  13998  addmodlteq  14000  ssnn0fi  14039  fsuppmapnn0fiub0  14047  suppssfz  14048  nn0sq11  14186  bernneq  14283  bernneq3  14285  facwordi  14343  faclbnd  14344  faclbnd3  14346  faclbnd5  14352  faclbnd6  14353  facubnd  14354  facavg  14355  bcval4  14361  bcval5  14372  bcpasc  14375  hashbnd  14390  hashnnn0genn0  14397  hashnemnf  14398  hashclb  14412  hashneq0  14418  hashsdom  14435  hashunsnggt  14448  fi1uzind  14562  ccat0  14631  ccat2s1fvw  14696  swrdnd0  14717  swrdsbslen  14724  swrdspsleq  14725  pfxnd0  14748  swrdswrdlem  14763  swrdswrd  14764  swrdccatin1  14784  pfxccatin12lem2  14790  pfxccatin12lem3  14791  pfxccat3  14793  swrdccat  14794  pfxccat3a  14797  swrdccat3blem  14798  repswswrd  14845  2cshw  14874  cshweqrep  14882  cshwcsh2id  14889  2swrd2eqwrdeq  15014  nn0sqeq1  15351  nn0absid  15505  isercoll  15743  o1fsum  15888  geomulcvg  15953  rerisefaccl  16094  refallfaccl  16095  rprisefaccl  16100  dvdseq  16394  oddge22np1  16429  nn0ehalf  16458  nn0o1gt2  16461  nn0o  16463  nn0oddm1d2  16465  bitsfi  16517  bitsinv1  16522  gcdn0gt0  16598  nn0gcdid0  16601  absmulgcd  16629  nn0seqcvgd  16650  algcvgblem  16657  algcvga  16659  lcmgcdnn  16691  lcmfun  16725  lcmfass  16726  prmfac1  16801  prmndvdsfaclt  16806  nonsq  16840  hashgcdlem  16869  odzdvds  16877  iserodd  16917  pcprendvds  16922  pcdvdsb  16951  pcidlem  16954  dvdsprmpweqle  16968  difsqpwdvds  16969  pcfaclem  16980  prmunb  16996  ramtcl2  17093  ramubcl  17100  ram0  17104  ramub1lem1  17108  cshwshashlem2  17178  smndex1iidm  18997  sylow1lem1  19712  pgpssslw  19728  efgsfo  19853  efgred  19862  telgsums  20107  prmirredlem  21672  prmirred  21674  gsumbagdiaglem  22131  psrridm  22162  psdmul  22379  coe1tmmul2  22487  gsummoncoe1  22518  mp2pm2mplem4  23016  fvmptnn04ifb  23058  chfacfisf  23061  chfacfisfcpmat  23062  chfacffsupp  23063  chfacfscmul0  23065  chfacfpmmul0  23069  dyaddisj  25806  mdegle0  26285  deg1nn0clb  26298  deg1ge  26306  deg1tmle  26326  ply1divex  26345  plyco0  26400  coeeulem  26432  coeaddlem  26457  coe1termlem  26466  dgreq0  26473  dgrlt  26474  plydivex  26509  aannenlem1  26542  taylfvallem1  26571  tayl0  26576  radcnvlem1  26627  radcnvlem2  26628  dvradcnv  26635  leibpi  27158  log2tlbnd  27161  birthdaylem3  27169  zetacvg  27230  basellem2  27297  basellem3  27298  chpp1  27370  bcmono  27492  bcmax  27493  lgsdinn0  27560  2lgslem1c  27608  2sq2  27648  2sqreulem1  27661  2sqreultlem  27662  dchrisumlem1  27704  ostth2lem2  27849  nbusgrvtxm1  29787  upgrewlkle2  30014  pthdlem1  30179  crctcshwlkn0lem4  30229  crctcshwlkn0  30237  crctcsh  30240  wwlksm1edg  30297  wwlksnred  30308  wwlksnredwwlkn  30311  wwlksnredwwlkn0  30312  wwlksnextwrd  30313  wwlksnextfun  30314  wwlksnextinj  30315  wwlksnextproplem1  30325  wwlksnextproplem2  30326  wwlksnextproplem3  30327  clwlkclwwlklem2a1  30410  clwlkclwwlklem2a2  30411  clwlkclwwlklem2fv1  30413  clwlkclwwlklem2fv2  30414  clwlkclwwlklem2a4  30415  clwlkclwwlklem2a  30416  clwlkclwwlklem2  30418  clwlkclwwlk  30420  clwlkclwwlk2  30421  clwlkclwwlkf  30426  clwwisshclwwslem  30432  clwwlkel  30464  wwlksext2clwwlk  30475  clwlknf1oclwwlknlem1  30499  clwwlknonex2lem2  30526  eupth2lems  30660  eupth2  30661  eucrctshift  30665  numclwwlk7  30813  frgrreggt1  30815  frgrreg  30816  frgrogt3nreg  30819  friendship  30821  nn0mnfxrd  33166  nn0xmulclb  33186  dpcl  33280  wrdt2ind  33339  hasheuni  34539  eulerpartlems  34815  hgt750lem  35103  derangen  35701  faclimlem1  36272  poimirlem28  38356  rrntotbnd  38545  sticksstones22  42993  gcdnn0id  43148  nn0addcom  43294  zaddcomlem  43295  nn0mulcom  43298  nacsfix  43501  eldioph2lem1  43549  irrapxlem4  43610  pell14qrgt0  43644  pell1qrgaplem  43658  pellqrexplicit  43662  rmxycomplete  43702  jm2.17a  43745  jm2.17b  43746  rmygeid  43749  jm2.22  43780  rmxdiophlem  43800  hbtlem5  43913  hbt  43915  fperiodmullem  46080  dvnxpaek  46714  stoweidlem17  46789  wallispilem3  46839  stirlinglem5  46850  stirlinglem7  46852  fourierdlem16  46895  fourierdlem21  46900  fourierdlem22  46901  fourierdlem83  46961  fourierdlem112  46990  elaa2lem  47005  etransclem23  47029  zm1nn  48097  nn0resubcl  48103  fz0addge0  48114  elfzlble  48115  subsubelfzo0  48122  2ffzoeq  48123  addmodne  48145  submodlt  48151  iccpartigtl  48230  lswn0  48251  sqrtpwpw2p  48348  fmtnodvds  48354  goldbachth  48357  odz2prm2pw  48373  flsqrt  48403  nn0e  48520  nn0sumltlt  49187  ply1mulgsumlem2  49224  nn0eo  49365  flnn0div2ge  49370  fllog2  49405  dignn0fr  49438  digexp  49444  dig2nn0  49448  0dig2nn0e  49449  dig2bits  49451  itcovalt2lem2lem1  49510