Theorem nn0re 12390

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11005  ℕ₀cn0 12381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-n0 12382

This theorem is referenced by:  nn0ge0  12406  nn0nlt0  12407  nn0le0eq0  12409  nn0p1gt0  12410  elnnnn0c  12426  nn0addge1  12427  nn0addge2  12428  nn0sub  12431  ltsubnn0  12432  nn0negleid  12433  difgtsumgt  12434  nn0le2x  12435  nn0n0n1ge2b  12450  nn0ge2m1nn  12451  nn0nndivcl  12453  xnn0xr  12459  nn0nepnf  12462  xnn0nemnf  12465  elznn0nn  12482  nn0lt2  12536  nn0le2is012  12537  nn0ge0div  12542  nn01to3  12839  xnn0xaddcl  13134  xnn0lem1lt  13143  xnn0lenn0nn0  13144  xnn0xadd0  13146  nn0rp0  13355  xnn0xrge0  13406  nn0fz0  13525  elfz0fzfz0  13533  fz0fzelfz0  13534  fz0fzdiffz0  13537  fzctr  13540  difelfzle  13541  difelfznle  13542  fvffz0  13546  fzoun  13596  nn0p1elfzo  13602  elfzo0le  13603  fzonmapblen  13608  fzofzim  13609  elincfzoext  13623  elfzodifsumelfzo  13631  fzonn0p1  13642  fzonn0p1p1  13644  ssfzoulel  13660  ubmelm1fzo  13663  elfznelfzo  13673  fvinim0ffz  13689  subfzo0  13692  adddivflid  13722  divfl0  13728  fldivnn0le  13736  flltdivnn0lt  13737  quoremnn0ALT  13761  modmuladdnn0  13822  addmodid  13826  modifeq2int  13840  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  ssnn0fi  13892  fsuppmapnn0fiub0  13900  suppssfz  13901  nn0sq11  14039  bernneq  14136  bernneq3  14138  facwordi  14196  faclbnd  14197  faclbnd3  14199  faclbnd5  14205  faclbnd6  14206  facubnd  14207  facavg  14208  bcval4  14214  bcval5  14225  bcpasc  14228  hashbnd  14243  hashnnn0genn0  14250  hashnemnf  14251  hashclb  14265  hashneq0  14271  hashsdom  14288  hashunsnggt  14301  fi1uzind  14414  ccat0  14483  ccat2s1fvw  14546  swrdnd0  14565  swrdsbslen  14572  swrdspsleq  14573  pfxnd0  14596  swrdswrdlem  14611  swrdswrd  14612  swrdccatin1  14632  pfxccatin12lem2  14638  pfxccatin12lem3  14639  pfxccat3  14641  swrdccat  14642  pfxccat3a  14645  swrdccat3blem  14646  repswswrd  14691  2cshw  14720  cshweqrep  14728  cshwcsh2id  14735  2swrd2eqwrdeq  14860  nn0sqeq1  15183  nn0absid  15337  isercoll  15575  o1fsum  15720  geomulcvg  15783  rerisefaccl  15924  refallfaccl  15925  rprisefaccl  15930  dvdseq  16225  oddge22np1  16260  nn0ehalf  16289  nn0o1gt2  16292  nn0o  16294  nn0oddm1d2  16296  bitsfi  16348  bitsinv1  16353  gcdn0gt0  16429  nn0gcdid0  16432  absmulgcd  16460  nn0seqcvgd  16481  algcvgblem  16488  algcvga  16490  lcmgcdnn  16522  lcmfun  16556  lcmfass  16557  prmfac1  16631  prmndvdsfaclt  16636  nonsq  16670  hashgcdlem  16699  odzdvds  16707  iserodd  16747  pcprendvds  16752  pcdvdsb  16781  pcidlem  16784  dvdsprmpweqle  16798  difsqpwdvds  16799  pcfaclem  16810  prmunb  16826  ramtcl2  16923  ramubcl  16930  ram0  16934  ramub1lem1  16938  cshwshashlem2  17008  smndex1iidm  18809  sylow1lem1  19510  pgpssslw  19526  efgsfo  19651  efgred  19660  telgsums  19905  prmirredlem  21409  prmirred  21411  gsumbagdiaglem  21867  psrridm  21900  psdmul  22081  coe1tmmul2  22190  gsummoncoe1  22223  mp2pm2mplem4  22724  fvmptnn04ifb  22766  chfacfisf  22769  chfacfisfcpmat  22770  chfacffsupp  22771  chfacfscmul0  22773  chfacfpmmul0  22777  dyaddisj  25524  mdegle0  26009  deg1nn0clb  26022  deg1ge  26030  deg1tmle  26050  ply1divex  26069  plyco0  26124  coeeulem  26156  coeaddlem  26181  coe1termlem  26190  dgreq0  26198  dgrlt  26199  plydivex  26232  aannenlem1  26263  taylfvallem1  26291  tayl0  26296  radcnvlem1  26349  radcnvlem2  26350  dvradcnv  26357  leibpi  26879  log2tlbnd  26882  birthdaylem3  26890  zetacvg  26952  basellem2  27019  basellem3  27020  chpp1  27092  bcmono  27215  bcmax  27216  lgsdinn0  27283  2lgslem1c  27331  2sq2  27371  2sqreulem1  27384  2sqreultlem  27385  dchrisumlem1  27427  ostth2lem2  27572  nbusgrvtxm1  29357  upgrewlkle2  29585  pthdlem1  29744  crctcshwlkn0lem4  29791  crctcshwlkn0  29799  crctcsh  29802  wwlksm1edg  29859  wwlksnred  29870  wwlksnredwwlkn  29873  wwlksnredwwlkn0  29874  wwlksnextwrd  29875  wwlksnextfun  29876  wwlksnextinj  29877  wwlksnextproplem1  29887  wwlksnextproplem2  29888  wwlksnextproplem3  29889  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a2  29973  clwlkclwwlklem2fv1  29975  clwlkclwwlklem2fv2  29976  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwlkclwwlk  29982  clwlkclwwlk2  29983  clwlkclwwlkf  29988  clwwisshclwwslem  29994  clwwlkel  30026  wwlksext2clwwlk  30037  clwlknf1oclwwlknlem1  30061  clwwlknonex2lem2  30088  eupth2lems  30218  eupth2  30219  eucrctshift  30223  numclwwlk7  30371  frgrreggt1  30373  frgrreg  30374  frgrogt3nreg  30377  friendship  30379  nn0xmulclb  32754  dpcl  32871  wrdt2ind  32934  hasheuni  34098  eulerpartlems  34373  hgt750lem  34664  0nn0m1nnn0  35157  derangen  35216  faclimlem1  35787  poimirlem28  37698  rrntotbnd  37886  sticksstones22  42271  gcdnn0id  42432  nn0addcom  42565  zaddcomlem  42566  nn0mulcom  42569  nacsfix  42815  eldioph2lem1  42863  irrapxlem4  42928  pell14qrgt0  42962  pell1qrgaplem  42976  pellqrexplicit  42980  rmxycomplete  43020  jm2.17a  43063  jm2.17b  43064  rmygeid  43067  jm2.22  43098  rmxdiophlem  43118  hbtlem5  43231  hbt  43233  fperiodmullem  45414  dvnxpaek  46050  stoweidlem17  46125  wallispilem3  46175  stirlinglem5  46186  stirlinglem7  46188  fourierdlem16  46231  fourierdlem21  46236  fourierdlem22  46237  fourierdlem83  46297  fourierdlem112  46326  elaa2lem  46341  etransclem23  46365  zm1nn  47412  nn0resubcl  47418  fz0addge0  47429  elfzlble  47430  subsubelfzo0  47436  2ffzoeq  47437  addmodne  47454  submodlt  47460  iccpartigtl  47533  lswn0  47554  sqrtpwpw2p  47648  fmtnodvds  47654  goldbachth  47657  odz2prm2pw  47673  flsqrt  47703  nn0e  47807  nn0sumltlt  48460  ply1mulgsumlem2  48498  nn0eo  48639  flnn0div2ge  48644  fllog2  48679  dignn0fr  48712  digexp  48718  dig2nn0  48722  0dig2nn0e  48723  dig2bits  48725  itcovalt2lem2lem1  48784