Theorem nn0re 11301

Description: A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0re	|- ( A e. NN0 -> A e. RR )

Proof of Theorem nn0re

Step	Hyp	Ref	Expression
1		nn0ssre 11296	. 2 |- NN0 C_ RR
2	1	sseli 3599	1 |- ( A e. NN0 -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1990   RRcr 9935   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021  df-n0 11293

This theorem is referenced by:  nn0ge0  11318  nn0nlt0  11319  nn0le0eq0  11321  nn0p1gt0  11322  elnnnn0c  11338  nn0addge1  11339  nn0addge2  11340  nn0sub  11343  ltsubnn0  11344  nn0negleid  11345  difgtsumgt  11346  nn0n0n1ge2b  11359  nn0ge2m1nn  11360  nn0nndivcl  11362  xnn0xr  11368  nn0nepnf  11371  xnn0nemnf  11374  elznn0nn  11391  nn0lt2  11440  nn0le2is012  11441  nn0ge0div  11446  nn01to3  11781  xnn0xaddcl  12066  xnn0lenn0nn0  12075  xnn0xadd0  12077  nn0rp0  12279  xnn0xrge0  12325  nn0fz0  12437  elfz0fzfz0  12444  fz0fzelfz0  12445  fz0fzdiffz0  12448  fzctr  12451  difelfzle  12452  difelfznle  12453  fvffz0  12457  nn0p1elfzo  12510  elfzo0le  12511  fzonmapblen  12513  fzofzim  12514  elincfzoext  12525  elfzodifsumelfzo  12533  fzonn0p1  12544  fzonn0p1p1  12546  elfzom1p1elfzo  12547  ssfzoulel  12562  ubmelm1fzo  12564  elfznelfzo  12573  fvinim0ffz  12587  subfzo0  12590  adddivflid  12619  divfl0  12625  fldivnn0le  12633  flltdivnn0lt  12634  quoremnn0ALT  12656  modmuladdnn0  12714  addmodid  12718  modifeq2int  12732  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  ssnn0fi  12784  fsuppmapnn0fiub0  12793  suppssfz  12794  bernneq  12990  bernneq3  12992  facwordi  13076  faclbnd  13077  faclbnd3  13079  faclbnd5  13085  faclbnd6  13086  facubnd  13087  facavg  13088  bcval4  13094  bcval5  13105  bcpasc  13108  hashbnd  13123  hashnnn0genn0  13131  hashnemnf  13132  hashclb  13149  hashneq0  13155  hashsdom  13170  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdsbslen  13448  swrdspsleq  13449  2swrdeqwrdeq  13453  swrdswrdlem  13459  swrdswrd  13460  swrdccatin1  13483  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat  13493  swrdccat3blem  13495  swrdccatid  13497  repswswrd  13531  2cshw  13559  cshweqrep  13567  cshwcsh2id  13574  2swrd2eqwrdeq  13696  isercoll  14398  o1fsum  14545  geomulcvg  14607  rerisefaccl  14748  refallfaccl  14749  rprisefaccl  14754  dvdseq  15036  oddge22np1  15073  nn0ehalf  15095  nn0o1gt2  15097  nn0o  15099  nn0oddm1d2  15101  divalglem5  15120  bitsfi  15159  bitsinv1  15164  gcdn0gt0  15239  nn0gcdid0  15242  absmulgcd  15266  nn0seqcvgd  15283  algcvgblem  15290  algcvga  15292  lcmgcdnn  15324  lcmfun  15358  lcmfass  15359  prmfac1  15431  prmndvdsfaclt  15435  nonsq  15467  hashgcdlem  15493  odzdvds  15500  iserodd  15540  pcprendvds  15545  pcdvdsb  15573  pcidlem  15576  dvdsprmpweqle  15590  difsqpwdvds  15591  pcfaclem  15602  prmunb  15618  ramtcl2  15715  ramubcl  15722  ram0  15726  ramub1lem1  15730  cshwshashlem2  15803  sylow1lem1  18013  pgpssslw  18029  efgsfo  18152  efgred  18161  telgsums  18390  psrbagcon  19371  gsumbagdiaglem  19375  psrridm  19404  coe1tmmul2  19646  gsummoncoe1  19674  prmirredlem  19841  prmirred  19843  mp2pm2mplem4  20614  fvmptnn04ifb  20656  chfacfisf  20659  chfacfisfcpmat  20660  chfacffsupp  20661  chfacfscmul0  20663  chfacfpmmul0  20667  dyaddisj  23364  mdegle0  23837  deg1nn0clb  23850  deg1ge  23858  deg1tmle  23877  ply1divex  23896  plyco0  23948  coeeulem  23980  coeaddlem  24005  coe1termlem  24014  dgreq0  24021  dgrlt  24022  plydivex  24052  aannenlem1  24083  taylfvallem1  24111  tayl0  24116  radcnvlem1  24167  radcnvlem2  24168  dvradcnv  24175  leibpi  24669  log2tlbnd  24672  birthdaylem3  24680  zetacvg  24741  basellem2  24808  basellem3  24809  chpp1  24881  bcmono  25002  bcmax  25003  lgsdinn0  25070  2lgslem1c  25118  dchrisumlem1  25178  ostth2lem2  25323  nbusgrvtxm1  26281  upgrewlkle2  26502  pthdlem1  26662  crctcshwlkn0lem4  26705  crctcshwlkn0  26713  crctcsh  26716  wwlksm1edg  26767  wwlksnred  26787  wwlksnredwwlkn  26790  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextproplem2  26805  wwlksnextproplem3  26806  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a2  26894  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwlkclwwlk  26903  clwlkclwwlk2  26904  clwwlksel  26914  wwlksext2clwwlk  26924  clwwisshclwwslem  26927  clwlksf1clwwlklem1  26965  eupth2lems  27098  eupth2  27099  eucrctshift  27103  numclwwlkovf2exlem2  27212  numclwwlk7  27249  frgrreggt1  27251  frgrreg  27252  frgrogt3nreg  27255  friendship  27257  nn0sqeq1  29513  dpcl  29598  hasheuni  30147  eulerpartlems  30422  hgt750lem  30729  derangen  31154  faclimlem1  31629  poimirlem28  33437  rrntotbnd  33635  nacsfix  37275  eldioph2lem1  37323  irrapxlem4  37389  pell14qrgt0  37423  pell1qrgaplem  37437  pellqrexplicit  37441  rmxycomplete  37482  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  jm2.22  37562  rmxdiophlem  37582  hbtlem5  37698  hbt  37700  fperiodmullem  39517  dvnxpaek  40157  stoweidlem17  40234  wallispilem3  40284  stirlinglem5  40295  stirlinglem7  40297  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem83  40406  fourierdlem112  40435  elaa2lem  40450  etransclem23  40474  zm1nn  41316  nn0resubcl  41317  fz0addge0  41329  elfzlble  41330  subsubelfzo0  41336  2ffzoeq  41338  iccpartigtl  41359  lswn0  41380  pfx2  41412  pfxccatin12lem2  41424  pfxccat3  41426  pfxccat3a  41429  sqrtpwpw2p  41450  fmtnodvds  41456  goldbachth  41459  odz2prm2pw  41475  flsqrt  41508  nn0e  41608  nn0sumltlt  42128  ply1mulgsumlem2  42175  nn0eo  42322  flnn0div2ge  42327  fllog2  42362  dignn0fr  42395  digexp  42401  dig2nn0  42405  0dig2nn0e  42406  dig2bits  42408