MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0re Structured version   Unicode version

Theorem nn0re 10222
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
StepHypRef Expression
1 nn0ssre 10217 . 2  |-  NN0  C_  RR
21sseli 3336 1  |-  ( A  e.  NN0  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RRcr 8981   NN0cn0 10213
This theorem is referenced by:  nn0ge0  10239  nn0nlt0  10240  nn0le0eq0  10242  elnnnn0c  10257  nn0addge1  10258  nn0addge2  10259  nn0sub  10262  nn0n0n1ge2b  10273  elznn0nn  10287  nn0lt10b  10328  nn0fz0  11106  fzctr  11109  fzossrbm1  11156  elfznelfzo  11184  injresinjlem  11191  quoremnn0  11229  quoremnn0ALT  11230  bernneq  11497  bernneq3  11499  facwordi  11572  faclbnd  11573  faclbnd3  11575  faclbnd5  11581  faclbnd6  11582  facubnd  11583  facavg  11584  bcval4  11590  bcval5  11601  bcpasc  11604  hashbnd  11616  hashnnn0genn0  11619  hashnemnf  11620  hashclb  11633  hashsdom  11647  brfi1uzind  11707  isercoll  12453  o1fsum  12584  geomulcvg  12645  dvdseq  12889  divalglem5  12909  bitsfi  12941  bitsinv1  12946  gcdn0gt0  13014  nn0gcdid0  13017  absmulgcd  13039  nn0seqcvgd  13053  algcvgblem  13060  algcvga  13062  prmfac1  13110  nonsq  13143  odzdvds  13173  iserodd  13201  pcprendvds  13206  pcdvdsb  13234  pcidlem  13237  pcfaclem  13259  prmunb  13274  ramtcl2  13371  ramubcl  13378  ram0  13382  ramub1lem1  13386  sylow1lem1  15224  pgpssslw  15240  efgsfo  15363  efgred  15372  psrbagcon  16428  gsumbagdiaglem  16432  psrridm  16460  coe1tmmul2  16660  prmirredlem  16765  prmirred  16767  dyaddisj  19480  mdegle0  19992  deg1nn0clb  20005  deg1ge  20013  deg1tmle  20032  ply1divex  20051  plyco0  20103  coeeulem  20135  coeaddlem  20159  coe1termlem  20168  dgreq0  20175  dgrlt  20176  plydivex  20206  aannenlem1  20237  taylfvallem1  20265  tayl0  20270  radcnvlem1  20321  radcnvlem2  20322  dvradcnv  20329  leibpi  20774  log2tlbnd  20777  birthdaylem3  20784  basellem2  20856  basellem3  20857  chpp1  20930  bcmono  21053  bcmax  21054  lgsdinn0  21116  dchrisumlem1  21175  ostth2lem2  21320  wlkonwlk  21527  cyclnspth  21610  nvnencycllem  21622  vdgrf  21661  vdgrfif  21662  eupath2  21694  hasheuni  24467  zetacvg  24791  derangen  24850  rerisefaccl  25325  refallfaccl  25326  rprisefaccl  25331  faclimlem1  25354  faclimlem3  25356  iprodfac  25358  rrntotbnd  26536  nacsfix  26757  eldioph2lem1  26809  irrapxlem4  26879  pell14qrgt0  26913  pell1qrgaplem  26927  pellqrexplicit  26931  rmxycomplete  26971  jm2.17a  27016  jm2.17b  27017  rmygeid  27020  jm2.22  27057  rmxdiophlem  27077  hbtlem5  27300  hbt  27302  hashgcdlem  27484  stoweidlem17  27733  wallispilem3  27783  stirlinglem5  27794  stirlinglem7  27796  lesubnn0  28081  ltsubnn0  28082  nn0resubcl  28084  elfzelfzadd  28094  elfz0fzfz0  28098  fz0fzelfz0  28102  fz0fzdiffz0  28103  fz0addge0  28104  fzonmapblen  28117  subsubelfzo0  28118  nn0nndivcl  28119  nn0ge0div  28120  fldivnn0le  28124  flltdivnn0lt  28125  modifeq2int  28139  wrdsymb0  28147  swrdnd  28154  swrdvalodmlem1  28159  swrdvalodm2  28160  swrd0swrd  28163  swrdswrdlem  28164  swrdswrd  28165  swrdccatin1  28171  swrdccatin12lem3  28178  swrdccatin12lem4  28179  swrdccat3  28181  swrdccat  28182  swrdccat3blem  28184  cshwoor  28203  cshwlen  28207  cshwidx  28208  cshwidxmod  28209  cshwidx0  28210  2cshw1lem1  28214  2cshw1lem2  28215  2cshw1lem3  28216  2cshw2lem1  28218  2cshw2lem2  28219  2cshw2lem3  28220  2cshwmod  28223  2cshwid  28224  lswrdn0  28226  cshweqrep  28237  cshw1  28238  cshwssizelem2  28244  cshwssizelem4a  28246  dpcl  28451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-i2m1 9050  ax-1ne0 9051  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-recs 6625  df-rdg 6660  df-nn 9993  df-n0 10214
  Copyright terms: Public domain W3C validator