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

Theorem nn0re 10186
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 10181 . 2  |-  NN0  C_  RR
21sseli 3304 1  |-  ( A  e.  NN0  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   RRcr 8945   NN0cn0 10177
This theorem is referenced by:  nn0ge0  10203  nn0nlt0  10204  nn0le0eq0  10206  elnnnn0c  10221  nn0addge1  10222  nn0addge2  10223  nn0sub  10226  nn0n0n1ge2b  10237  elznn0nn  10251  nn0lt10b  10292  fzctr  11072  fzossrbm1  11119  elfznelfzo  11147  injresinjlem  11154  quoremnn0  11192  quoremnn0ALT  11193  bernneq  11460  bernneq3  11462  facwordi  11535  faclbnd  11536  faclbnd3  11538  faclbnd5  11544  faclbnd6  11545  facubnd  11546  facavg  11547  bcval4  11553  bcval5  11564  bcpasc  11567  hashbnd  11579  hashnnn0genn0  11582  hashnemnf  11583  hashclb  11596  hashsdom  11610  brfi1uzind  11670  isercoll  12416  o1fsum  12547  geomulcvg  12608  dvdseq  12852  divalglem5  12872  bitsfi  12904  bitsinv1  12909  gcdn0gt0  12977  nn0gcdid0  12980  absmulgcd  13002  nn0seqcvgd  13016  algcvgblem  13023  algcvga  13025  prmfac1  13073  nonsq  13106  odzdvds  13136  iserodd  13164  pcprendvds  13169  pcdvdsb  13197  pcidlem  13200  pcfaclem  13222  prmunb  13237  ramtcl2  13334  ramubcl  13341  ram0  13345  ramub1lem1  13349  sylow1lem1  15187  pgpssslw  15203  efgsfo  15326  efgred  15335  psrbagcon  16391  gsumbagdiaglem  16395  psrridm  16423  coe1tmmul2  16623  prmirredlem  16728  prmirred  16730  dyaddisj  19441  mdegle0  19953  deg1nn0clb  19966  deg1ge  19974  deg1tmle  19993  ply1divex  20012  plyco0  20064  coeeulem  20096  coeaddlem  20120  coe1termlem  20129  dgreq0  20136  dgrlt  20137  plydivex  20167  aannenlem1  20198  taylfvallem1  20226  tayl0  20231  radcnvlem1  20282  radcnvlem2  20283  dvradcnv  20290  leibpi  20735  log2tlbnd  20738  birthdaylem3  20745  basellem2  20817  basellem3  20818  chpp1  20891  bcmono  21014  bcmax  21015  lgsdinn0  21077  dchrisumlem1  21136  ostth2lem2  21281  wlkonwlk  21488  cyclnspth  21571  nvnencycllem  21583  vdgrf  21622  vdgrfif  21623  eupath2  21655  hasheuni  24428  zetacvg  24752  derangen  24811  rerisefaccl  25285  refallfaccl  25286  rprisefaccl  25291  faclimlem1  25310  faclimlem3  25312  iprodfac  25314  rrntotbnd  26435  nacsfix  26656  eldioph2lem1  26708  irrapxlem4  26778  pell14qrgt0  26812  pell1qrgaplem  26826  pellqrexplicit  26830  rmxycomplete  26870  jm2.17a  26915  jm2.17b  26916  rmygeid  26919  jm2.22  26956  rmxdiophlem  26976  hbtlem5  27200  hbt  27202  hashgcdlem  27384  stoweidlem17  27633  wallispilem3  27683  stirlinglem5  27694  stirlinglem7  27696  lesubnn0  27972  ltsubnn0  27973  nn0resubcl  27975  nn0fz0  27979  elfzelfzadd  27982  swrdnd  28001  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3b  28031  dpcl  28228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-recs 6592  df-rdg 6627  df-nn 9957  df-n0 10178
  Copyright terms: Public domain W3C validator