Theorem nn0re 12655

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11238  ℕ₀cn0 12646

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376  df-n0 12647

This theorem is used by:  nn0ge0  12671  nn0nlt0  12672  nn0le0eq0  12674  nn0p1gt0  12675  elnnnn0c  12691  nn0addge1  12692  nn0addge2  12693  nn0sub  12696  ltsubnn0  12697  nn0negleid  12698  difgtsumgt  12699  nn0le2x  12700  nn0n0n1ge2b  12715  nn0ge2m1nn  12716  nn0nndivcl  12718  xnn0xr  12724  nn0nepnf  12727  xnn0nemnf  12730  elznn0nn  12747  0nn0m1nnn0  12793  nn0lt2  12802  nn0le2is012  12803  nn0ge0div  12808  nn01to3  13108  xnn0xaddcl  13405  xnn0lem1lt  13414  xnn0lenn0nn0  13415  xnn0xadd0  13417  nn0rp0  13626  xnn0xrge0  13677  nn0fz0  13799  elfz0fzfz0  13807  fz0fzelfz0  13808  fz0fzdiffz0  13811  difelfzle  13815  difelfznle  13816  fvffz0  13820  fzoun  13871  nn0p1elfzo  13877  elfzo0le  13878  fzonmapblen  13883  fzofzim  13884  elincfzoext  13898  elfzodifsumelfzo  13906  fzonn0p1  13917  fzonn0p1p1  13919  ssfzoulel  13935  ubmelm1fzo  13938  elfznelfzo  13948  fvinim0ffz  13964  subfzo0  13968  adddivflid  13998  divfl0  14004  fldivnn0le  14012  flltdivnn0lt  14013  quoremnn0ALT  14037  modmuladdnn0  14098  addmodid  14102  modifeq2int  14116  modfzo0difsn  14126  modsumfzodifsn  14127  addmodlteq  14129  ssnn0fi  14168  fsuppmapnn0fiub0  14176  suppssfz  14177  nn0sq11  14315  bernneq  14414  bernneq3  14416  facwordi  14474  faclbnd  14475  faclbnd3  14477  faclbnd5  14483  faclbnd6  14484  facubnd  14485  facavg  14486  bcval4  14492  bcval5  14503  bcpasc  14506  hashbnd  14521  hashnnn0genn0  14528  hashnemnf  14529  hashclb  14543  hashneq0  14549  hashsdom  14566  hashunsnggt  14579  fi1uzind  14693  ccat0  14762  ccat2s1fvw  14828  swrdnd0  14849  swrdsbslen  14856  swrdspsleq  14857  pfxnd0  14880  swrdswrdlem  14895  swrdswrd  14896  swrdccatin1  14916  pfxccatin12lem2  14922  pfxccatin12lem3  14923  pfxccat3  14925  swrdccat  14926  pfxccat3a  14929  swrdccat3blem  14930  repswswrd  14977  2cshw  15006  cshweqrep  15014  cshwcsh2id  15021  2swrd2eqwrdeq  15149  nn0sqeq1  15486  nn0absid  15641  isercoll  15879  o1fsum  16024  geomulcvg  16089  rerisefaccl  16228  refallfaccl  16229  rprisefaccl  16234  dvdseq  16528  oddge22np1  16563  nn0ehalf  16592  nn0o1gt2  16595  nn0o  16597  nn0oddm1d2  16599  bitsfi  16651  bitsinv1  16656  gcdn0gt0  16734  nn0gcdid0  16737  gcdnn0id  16744  absmulgcd  16766  nn0seqcvgd  16789  algcvgblem  16796  algcvga  16798  lcmgcdnn  16830  lcmfun  16864  lcmfass  16865  prmfac1  16940  prmndvdsfaclt  16945  nonsq  16979  hashgcdlem  17009  odzdvds  17017  iserodd  17057  pcprendvds  17062  pcdvdsb  17091  pcidlem  17094  dvdsprmpweqle  17108  difsqpwdvds  17109  pcfaclem  17120  prmunb  17136  ramtcl2  17233  ramubcl  17240  ram0  17244  ramub1lem1  17248  cshwshashlem2  17318  smndex1iidm  19147  sylow1lem1  19863  pgpssslw  19879  efgsfo  20004  efgred  20013  telgsums  20258  prmirredlem  21833  prmirred  21835  gsumbagdiaglem  22294  psrridm  22325  psdmul  22542  coe1tmmul2  22650  gsummoncoe1  22681  mp2pm2mplem4  23182  fvmptnn04ifb  23224  chfacfisf  23227  chfacfisfcpmat  23228  chfacffsupp  23229  chfacfscmul0  23231  chfacfpmmul0  23235  dyaddisj  25972  mdegle0  26450  deg1nn0clb  26463  deg1ge  26471  deg1tmle  26491  ply1divex  26510  plyco0  26565  coeeulem  26598  coeaddlem  26623  coe1termlem  26632  dgreq0  26639  dgrlt  26640  plydivex  26673  aannenlem1  26712  taylfvallem1  26741  tayl0  26746  radcnvlem1  26797  radcnvlem2  26798  dvradcnv  26805  leibpi  27327  log2tlbnd  27330  birthdaylem3  27338  zetacvg  27399  basellem2  27466  basellem3  27467  chpp1  27539  bcmono  27661  bcmax  27662  lgsdinn0  27729  2lgslem1c  27777  2sq2  27817  2sqreulem1  27830  2sqreultlem  27831  dchrisumlem1  27873  ostth2lem2  28018  nbusgrvtxm1  30017  upgrewlkle2  30244  pthdlem1  30409  crctcshwlkn0lem4  30459  crctcshwlkn0  30467  crctcsh  30470  wwlksm1edg  30527  wwlksnred  30538  wwlksnredwwlkn  30541  wwlksnredwwlkn0  30542  wwlksnextwrd  30543  wwlksnextfun  30544  wwlksnextinj  30545  wwlksnextproplem1  30555  wwlksnextproplem2  30556  wwlksnextproplem3  30557  clwlkclwwlklem2a1  30640  clwlkclwwlklem2a2  30641  clwlkclwwlklem2fv1  30643  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwlkclwwlk  30650  clwlkclwwlk2  30651  clwlkclwwlkf  30656  clwwisshclwwslem  30662  clwwlkel  30694  wwlksext2clwwlk  30705  clwlknf1oclwwlknlem1  30729  clwwlknonex2lem2  30756  eupth2lems  30896  eupth2  30897  eucrctshift  30901  numclwwlk7  31049  frgrreggt1  31051  frgrreg  31052  frgrogt3nreg  31055  friendship  31057  nn0mnfxrd  33439  nn0xmulclb  33459  dpcl  33553  wrdt2ind  33612  hasheuni  34828  eulerpartlems  35103  hgt750lem  35391  derangen  36145  faclimlem1  36723  poimirlem28  38834  rrntotbnd  39036  sticksstones22  43484  nn0addcom  43792  zaddcomlem  43793  nn0mulcom  43796  nacsfix  43989  eldioph2lem1  44037  irrapxlem4  44098  pell14qrgt0  44132  pell1qrgaplem  44146  pellqrexplicit  44150  rmxycomplete  44190  jm2.17a  44233  jm2.17b  44234  rmygeid  44237  jm2.22  44268  rmxdiophlem  44288  hbtlem5  44395  hbt  44397  fperiodmullem  46592  dvnxpaek  47225  stoweidlem17  47300  wallispilem3  47350  stirlinglem5  47361  stirlinglem7  47363  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem83  47472  fourierdlem112  47501  elaa2lem  47516  etransclem23  47540  zm1nn  48645  nn0resubcl  48651  fz0addge0  48662  elfzlble  48663  subsubelfzo0  48670  2ffzoeq  48671  addmodne  48693  submodlt  48699  iccpartigtl  48778  lswn0  48799  sqrtpwpw2p  48896  fmtnodvds  48902  goldbachth  48905  odz2prm2pw  48921  flsqrt  48951  nn0e  49068  nn0sumltlt  49793  ply1mulgsumlem2  49830  nn0eo  49971  flnn0div2ge  49976  fllog2  50011  dignn0fr  50044  digexp  50050  dig2nn0  50054  0dig2nn0e  50055  dig2bits  50057  itcovalt2lem2lem1  50116