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

Theorem nn0red 10859
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1  |-  ( ph  ->  A  e.  NN0 )
Assertion
Ref Expression
nn0red  |-  ( ph  ->  A  e.  RR )

Proof of Theorem nn0red
StepHypRef Expression
1 nn0ssre 10805 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3487 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   RRcr 9494   NN0cn0 10801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-om 6686  df-recs 7044  df-rdg 7078  df-nn 10543  df-n0 10802
This theorem is referenced by:  nn0cnd  10860  nn0readdcl  10864  flmulnn0  11939  quoremz  11961  quoremnn0ALT  11963  modaddmodup  12029  modaddmodlo  12030  expneg  12153  expnbnd  12274  facdiv  12344  faclbnd6  12356  hashdom  12426  hashun2  12430  hashunx  12433  hashfun  12474  hashf1  12485  seqcoll2  12492  hashge2el2dif  12500  hashtpg  12502  wrdlenge2n0  12556  ccatval1  12574  ccatsymb  12579  ccatrn  12585  swrdccat3blem  12699  cshwidxmod  12753  repswcshw  12759  swrds2  12862  modfsummods  13586  climcnds  13642  geomulcvg  13664  mertenslem1  13672  efcllem  13691  eftlub  13721  ruclem10  13849  bitsfzolem  13961  bitsfzo  13962  bitsmod  13963  sadcaddlem  13984  sadaddlem  13993  sadasslem  13997  sadeq  13999  smuval2  14009  smupvallem  14010  smueqlem  14017  bezoutlem3  14055  bezoutlem4  14056  gcdeq  14067  dvdssqlem  14074  nn0seqcvgd  14076  eucalglt  14091  mulgcddvds  14122  qredeu  14125  prmdiveq  14193  odzdvds  14199  pythagtriplem3  14219  pythagtriplem6  14222  pythagtriplem7  14223  iserodd  14236  pclem  14239  pcpremul  14244  pcidlem  14272  pcgcd1  14277  pc2dvds  14279  pcz  14281  pcprmpw2  14282  fldivp1  14293  pcfaclem  14294  pcfac  14295  pcbc  14296  prmreclem2  14312  prmreclem3  14313  prmreclem4  14314  prmreclem5  14315  4sqlem11  14350  4sqlem12  14351  4sqlem14  14353  vdwlem11  14386  vdwlem12  14387  ramlb  14414  0ram  14415  ram0  14417  ramub1lem2  14422  ramcl  14424  psgnunilem2  16394  odmodnn0  16438  mndodconglem  16439  mndodcong  16440  oddvds  16445  odhash3  16470  gexdvds  16478  sylow1lem1  16492  sylow1lem5  16496  pgpfi  16499  pgpssslw  16508  efgsfo  16631  efgredlemd  16636  efgredlem  16639  efgred  16640  lt6abl  16771  telgsums  16896  pgpfaclem2  17007  srgbinomlem3  17067  psrbaglesupp  17891  psrbaglesuppOLD  17892  mplmonmul  18000  coe1tmmul2  18191  coe1tmmul2fv  18193  coe1pwmulfv  18195  gsummoncoe1  18220  zringlpirlem3  18384  zlpirlem3  18389  fvmptnn04if  19223  fvmptnn04ifc  19226  fvmptnn04ifd  19227  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  lebnumii  21339  dyadmaxlem  21879  mbfi1fseqlem3  21997  mbfi1fseqlem4  21998  mbfi1fseqlem5  21999  mdegmullem  22351  coe1mul3  22373  coe1mul4  22374  deg1sublt  22384  deg1mul2  22388  deg1tmle  22391  deg1tm  22392  ply1divmo  22409  ply1divex  22410  deg1submon1p  22426  dvdsq1p  22434  fta1glem2  22440  fta1blem  22442  plyco0  22462  plyeq0lem  22480  plypf1  22482  plyaddlem1  22483  coeeulem  22494  dgrub  22504  dgrlb  22506  dgreq  22514  coeaddlem  22518  coemullem  22519  coemulhi  22523  dgrlt  22535  dgradd2  22537  dgrmul  22539  dgrcolem2  22543  dgrco  22544  plydivlem3  22563  plydivlem4  22564  plydivex  22565  plydiveu  22566  fta1lem  22575  quotcan  22577  vieta1lem2  22579  radcnvlem1  22680  dvradcnv  22688  leibpilem1  23143  leibpi  23145  log2tlbnd  23148  birthdaylem2  23154  birthdaylem3  23155  fsumharmonic  23213  basellem3  23228  basellem5  23230  issqf  23282  ppip1le  23307  ppiltx  23323  mumullem2  23326  sgmppw  23344  ppiub  23351  chtublem  23358  chpub  23367  dchrabs  23407  bcmono  23424  bcmax  23425  bcp1ctr  23426  bclbnd  23427  bposlem5  23435  lgseisenlem1  23496  2sqlem7  23517  2sqlem8  23519  chebbnd1lem1  23526  chtppilimlem1  23530  dchrisum0re  23570  mulogsumlem  23588  selberg2lem  23607  pntrlog2bndlem4  23637  pntlemr  23659  pntlemj  23660  pnt  23671  ostth2lem3  23692  spthispth  24447  wwlknred  24595  wwlkextproplem2  24614  vdgrfival  24769  nbhashuvtx1  24787  rusgranumwlks  24828  eupap1  24848  eupath2lem3  24851  frghash2spot  24935  usgreghash2spotv  24938  numclwwlk5  24984  numclwwlk6  24985  friendshipgt3  24993  nndiffz1  27468  2sqmod  27509  nexple  27878  oddpwdc  28166  eulerpartlems  28172  eulerpartlemgc  28174  eulerpartlemb  28180  coinfliplem  28290  eluzmn  28364  signsplypnf  28380  signslema  28392  signstfvc  28404  signstfveq0  28407  dmlogdmgm  28439  erdszelem8  28515  erdsze2lem2  28521  cvmliftlem7  28609  snmlff  28647  binomfallfaclem2  29137  binomrisefac  29139  fallfacval4  29140  rrnequiv  30306  eldioph2lem1  30668  pell1qrge1  30781  rmxypos  30860  ltrmynn0  30861  ltrmxnn0  30862  lermxnn0  30863  jm2.24nn  30872  jm2.24  30876  jm2.19  30910  jm2.26lem3  30918  jm2.27c  30924  hbt  31054  dgraa0p  31074  lcmneg  31185  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  stoweidlem17  31688  stoweidlem24  31695  wallispilem5  31740  stirlinglem15  31759  fourierdlem48  31826  fourierdlem83  31861  fourierdlem103  31881  fourierdlem104  31882  sqwvfoura  31900  ssnn0ssfz  32671  pgrple2abl  32691
  Copyright terms: Public domain W3C validator