Theorem nn0re 12538

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

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

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 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-i2m1 11193  ax-1ne0 11194  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198

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 12259  df-n0 12530

This theorem is used by:  nn0ge0  12554  nn0nlt0  12555  nn0le0eq0  12557  nn0p1gt0  12558  elnnnn0c  12574  nn0addge1  12575  nn0addge2  12576  nn0sub  12579  ltsubnn0  12580  nn0negleid  12581  difgtsumgt  12582  nn0le2x  12583  nn0n0n1ge2b  12598  nn0ge2m1nn  12599  nn0nndivcl  12601  xnn0xr  12607  nn0nepnf  12610  xnn0nemnf  12613  elznn0nn  12630  0nn0m1nnn0  12676  nn0lt2  12685  nn0le2is012  12686  nn0ge0div  12691  nn01to3  12991  xnn0xaddcl  13288  xnn0lem1lt  13297  xnn0lenn0nn0  13298  xnn0xadd0  13300  nn0rp0  13509  xnn0xrge0  13560  nn0fz0  13681  elfz0fzfz0  13689  fz0fzelfz0  13690  fz0fzdiffz0  13693  fzctr  13696  difelfzle  13697  difelfznle  13698  fvffz0  13702  fzoun  13753  nn0p1elfzo  13759  elfzo0le  13760  fzonmapblen  13765  fzofzim  13766  elincfzoext  13780  elfzodifsumelfzo  13788  fzonn0p1  13799  fzonn0p1p1  13801  ssfzoulel  13817  ubmelm1fzo  13820  elfznelfzo  13830  fvinim0ffz  13846  subfzo0  13850  adddivflid  13880  divfl0  13886  fldivnn0le  13894  flltdivnn0lt  13895  quoremnn0ALT  13919  modmuladdnn0  13980  addmodid  13984  modifeq2int  13998  modfzo0difsn  14008  modsumfzodifsn  14009  addmodlteq  14011  ssnn0fi  14050  fsuppmapnn0fiub0  14058  suppssfz  14059  nn0sq11  14197  bernneq  14294  bernneq3  14296  facwordi  14354  faclbnd  14355  faclbnd3  14357  faclbnd5  14363  faclbnd6  14364  facubnd  14365  facavg  14366  bcval4  14372  bcval5  14383  bcpasc  14386  hashbnd  14401  hashnnn0genn0  14408  hashnemnf  14409  hashclb  14423  hashneq0  14429  hashsdom  14446  hashunsnggt  14459  fi1uzind  14573  ccat0  14642  ccat2s1fvw  14707  swrdnd0  14728  swrdsbslen  14735  swrdspsleq  14736  pfxnd0  14759  swrdswrdlem  14774  swrdswrd  14775  swrdccatin1  14795  pfxccatin12lem2  14801  pfxccatin12lem3  14802  pfxccat3  14804  swrdccat  14805  pfxccat3a  14808  swrdccat3blem  14809  repswswrd  14856  2cshw  14885  cshweqrep  14893  cshwcsh2id  14900  2swrd2eqwrdeq  15027  nn0sqeq1  15364  nn0absid  15518  isercoll  15756  o1fsum  15901  geomulcvg  15966  rerisefaccl  16105  refallfaccl  16106  rprisefaccl  16111  dvdseq  16405  oddge22np1  16440  nn0ehalf  16469  nn0o1gt2  16472  nn0o  16474  nn0oddm1d2  16476  bitsfi  16528  bitsinv1  16533  gcdn0gt0  16609  nn0gcdid0  16612  absmulgcd  16640  nn0seqcvgd  16661  algcvgblem  16668  algcvga  16670  lcmgcdnn  16702  lcmfun  16736  lcmfass  16737  prmfac1  16812  prmndvdsfaclt  16817  nonsq  16851  hashgcdlem  16880  odzdvds  16888  iserodd  16928  pcprendvds  16933  pcdvdsb  16962  pcidlem  16965  dvdsprmpweqle  16979  difsqpwdvds  16980  pcfaclem  16991  prmunb  17007  ramtcl2  17104  ramubcl  17111  ram0  17115  ramub1lem1  17119  cshwshashlem2  17189  smndex1iidm  19011  sylow1lem1  19726  pgpssslw  19742  efgsfo  19867  efgred  19876  telgsums  20121  prmirredlem  21686  prmirred  21688  gsumbagdiaglem  22147  psrridm  22178  psdmul  22395  coe1tmmul2  22503  gsummoncoe1  22534  mp2pm2mplem4  23035  fvmptnn04ifb  23077  chfacfisf  23080  chfacfisfcpmat  23081  chfacffsupp  23082  chfacfscmul0  23084  chfacfpmmul0  23088  dyaddisj  25825  mdegle0  26303  deg1nn0clb  26316  deg1ge  26324  deg1tmle  26344  ply1divex  26363  plyco0  26418  coeeulem  26451  coeaddlem  26476  coe1termlem  26485  dgreq0  26492  dgrlt  26493  plydivex  26528  aannenlem1  26565  taylfvallem1  26594  tayl0  26599  radcnvlem1  26650  radcnvlem2  26651  dvradcnv  26658  leibpi  27180  log2tlbnd  27183  birthdaylem3  27191  zetacvg  27252  basellem2  27319  basellem3  27320  chpp1  27392  bcmono  27514  bcmax  27515  lgsdinn0  27582  2lgslem1c  27630  2sq2  27670  2sqreulem1  27683  2sqreultlem  27684  dchrisumlem1  27726  ostth2lem2  27871  nbusgrvtxm1  29840  upgrewlkle2  30067  pthdlem1  30232  crctcshwlkn0lem4  30282  crctcshwlkn0  30290  crctcsh  30293  wwlksm1edg  30350  wwlksnred  30361  wwlksnredwwlkn  30364  wwlksnredwwlkn0  30365  wwlksnextwrd  30366  wwlksnextfun  30367  wwlksnextinj  30368  wwlksnextproplem1  30378  wwlksnextproplem2  30379  wwlksnextproplem3  30380  clwlkclwwlklem2a1  30463  clwlkclwwlklem2a2  30464  clwlkclwwlklem2fv1  30466  clwlkclwwlklem2fv2  30467  clwlkclwwlklem2a4  30468  clwlkclwwlklem2a  30469  clwlkclwwlklem2  30471  clwlkclwwlk  30473  clwlkclwwlk2  30474  clwlkclwwlkf  30479  clwwisshclwwslem  30485  clwwlkel  30517  wwlksext2clwwlk  30528  clwlknf1oclwwlknlem1  30552  clwwlknonex2lem2  30579  eupth2lems  30719  eupth2  30720  eucrctshift  30724  numclwwlk7  30872  frgrreggt1  30874  frgrreg  30875  frgrogt3nreg  30878  friendship  30880  nn0mnfxrd  33223  nn0xmulclb  33243  dpcl  33337  wrdt2ind  33396  hasheuni  34596  eulerpartlems  34872  hgt750lem  35160  derangen  35752  faclimlem1  36323  poimirlem28  38398  rrntotbnd  38587  sticksstones22  43035  gcdnn0id  43205  nn0addcom  43351  zaddcomlem  43352  nn0mulcom  43355  nacsfix  43558  eldioph2lem1  43606  irrapxlem4  43667  pell14qrgt0  43701  pell1qrgaplem  43715  pellqrexplicit  43719  rmxycomplete  43759  jm2.17a  43802  jm2.17b  43803  rmygeid  43806  jm2.22  43837  rmxdiophlem  43857  hbtlem5  43970  hbt  43972  fperiodmullem  46137  dvnxpaek  46771  stoweidlem17  46846  wallispilem3  46896  stirlinglem5  46907  stirlinglem7  46909  fourierdlem16  46952  fourierdlem21  46957  fourierdlem22  46958  fourierdlem83  47018  fourierdlem112  47047  elaa2lem  47062  etransclem23  47086  zm1nn  48191  nn0resubcl  48197  fz0addge0  48208  elfzlble  48209  subsubelfzo0  48216  2ffzoeq  48217  addmodne  48239  submodlt  48245  iccpartigtl  48324  lswn0  48345  sqrtpwpw2p  48442  fmtnodvds  48448  goldbachth  48451  odz2prm2pw  48467  flsqrt  48497  nn0e  48614  nn0sumltlt  49281  ply1mulgsumlem2  49318  nn0eo  49459  flnn0div2ge  49464  fllog2  49499  dignn0fr  49532  digexp  49538  dig2nn0  49542  0dig2nn0e  49543  dig2bits  49545  itcovalt2lem2lem1  49604