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

Theorem nn0red 10915
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 10862 . 2  |-  NN0  C_  RR
2 nn0red.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3459 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   RRcr 9527   NN0cn0 10858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-i2m1 9596  ax-1ne0 9597  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-om 6698  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-nn 10599  df-n0 10859
This theorem is referenced by:  nn0cnd  10916  nn0readdcl  10920  flmulnn0  12046  quoremz  12068  quoremnn0ALT  12070  modaddmodup  12139  modaddmodlo  12140  expneg  12266  expnbnd  12387  facdiv  12458  faclbnd6  12470  hashdom  12544  hashun2  12548  hashunx  12551  hashfun  12593  hashf1  12604  seqcoll2  12611  hashge2el2dif  12619  hashtpg  12621  wrdlenge2n0  12679  ccatsymb  12703  ccatrn  12709  ccat2s1fvw  12745  swrdnd  12762  swrdccat3blem  12825  cshwidxmod  12879  repswcshw  12885  swrds2  12988  modfsummods  13820  climcnds  13876  geomulcvg  13899  mertenslem1  13907  binomfallfaclem2  14060  binomrisefac  14062  fallfacval4  14063  efcllem  14099  eftlub  14130  ruclem10  14258  bitsfzolem  14371  bitsfzo  14372  bitsmod  14373  sadcaddlem  14394  sadaddlem  14403  sadasslem  14407  sadeq  14409  smuval2  14419  smupvallem  14420  smueqlem  14427  bezoutlem3  14468  bezoutlem4  14469  gcdeq  14480  dvdssqlem  14487  nn0seqcvgd  14489  eucalglt  14504  lcmneg  14528  mulgcddvds  14621  qredeu  14624  prmdiveq  14694  odzdvds  14700  odzdvdsOLD  14706  pythagtriplem3  14728  pythagtriplem6  14731  pythagtriplem7  14732  iserodd  14745  pclem  14748  pcpremul  14753  pcidlem  14781  pcgcd1  14786  pc2dvds  14788  pcz  14790  pcprmpw2  14791  fldivp1  14802  pcfaclem  14803  pcfac  14804  pcbc  14805  prmreclem2  14821  prmreclem3  14822  prmreclem4  14823  prmreclem5  14824  4sqlem11  14859  4sqlem12  14860  4sqlem14OLD  14862  4sqlem14  14868  vdwlem11  14901  vdwlem12  14902  ramlb  14937  0ram  14938  ram0  14940  ramub1lem2  14945  ramcl  14947  psgnunilem2  17088  odmodnn0  17134  mndodconglem  17135  mndodcong  17136  oddvds  17141  odhash3  17166  gexdvds  17176  sylow1lem1  17191  sylow1lem5  17195  pgpfi  17198  pgpssslw  17207  efgsfo  17330  efgredlemd  17335  efgredlem  17338  efgred  17339  lt6abl  17470  telgsums  17564  pgpfaclem2  17656  srgbinomlem3  17716  psrbaglesupp  18533  mplmonmul  18629  coe1tmmul2  18810  coe1tmmul2fv  18812  coe1pwmulfv  18814  gsummoncoe1  18839  zringlpirlem3  18995  fvmptnn04if  19810  fvmptnn04ifc  19813  fvmptnn04ifd  19814  chfacfscmulgsum  19821  chfacfpmmulgsum  19825  lebnumii  21916  dyadmaxlem  22462  mbfi1fseqlem3  22582  mbfi1fseqlem4  22583  mbfi1fseqlem5  22584  mdegmullem  22934  coe1mul3  22955  coe1mul4  22956  deg1sublt  22966  deg1mul2  22970  deg1tmle  22973  deg1tm  22974  ply1divmo  22993  ply1divex  22994  deg1submon1p  23010  dvdsq1p  23018  fta1glem2  23024  fta1blem  23026  plyco0  23053  plyeq0lem  23071  plypf1  23073  plyaddlem1  23074  coeeulem  23085  dgrub  23095  dgrlb  23097  dgreq  23105  coeaddlem  23110  coemullem  23111  coemulhi  23115  dgrlt  23127  dgradd2  23129  dgrmul  23131  dgrcolem2  23135  dgrco  23136  plydivlem3  23155  plydivlem4  23156  plydivex  23157  plydiveu  23158  fta1lem  23167  quotcan  23169  vieta1lem2  23171  radcnvlem1  23272  dvradcnv  23280  leibpilem1  23770  leibpi  23772  log2tlbnd  23775  birthdaylem2  23782  birthdaylem3  23783  fsumharmonic  23841  dmlogdmgm  23853  basellem3  23911  basellem5  23913  issqf  23965  ppip1le  23990  ppiltx  24006  mumullem2  24009  sgmppw  24027  ppiub  24034  chtublem  24041  chpub  24050  dchrabs  24090  bcmono  24107  bcmax  24108  bcp1ctr  24109  bclbnd  24110  bposlem5  24118  lgseisenlem1  24179  2sqlem7  24200  2sqlem8  24202  chebbnd1lem1  24209  chtppilimlem1  24213  dchrisum0re  24253  mulogsumlem  24271  selberg2lem  24290  pntrlog2bndlem4  24320  pntlemr  24342  pntlemj  24343  pnt  24354  ostth2lem3  24375  spthispth  25189  wwlknred  25337  wwlkextproplem2  25356  vdgrfival  25511  nbhashuvtx1  25529  rusgranumwlks  25570  eupap1  25590  eupath2lem3  25593  frghash2spot  25677  usgreghash2spotv  25680  numclwwlk5  25726  numclwwlk6  25727  friendshipgt3  25735  nndiffz1  28243  2sqmod  28288  nexple  28711  oddpwdc  29054  eulerpartlems  29060  eulerpartlemgc  29062  eulerpartlemb  29068  coinfliplem  29178  eluzmn  29252  signsplypnf  29268  signslema  29280  signstfvc  29292  signstfveq0  29295  erdszelem8  29750  erdsze2lem2  29756  cvmliftlem7  29843  snmlff  29881  bcprod  30202  poimirlem3  31691  poimirlem4  31692  poimirlem6  31694  poimirlem7  31695  poimirlem10  31698  poimirlem11  31699  poimirlem12  31700  poimirlem13  31701  poimirlem15  31703  poimirlem16  31704  poimirlem17  31705  poimirlem19  31707  poimirlem20  31708  poimirlem21  31709  poimirlem22  31710  poimirlem23  31711  poimirlem24  31712  poimirlem25  31713  poimirlem26  31714  poimirlem29  31717  poimirlem30  31718  poimirlem31  31719  rrnequiv  31915  eldioph2lem1  35355  pell1qrge1  35470  rmxypos  35551  ltrmynn0  35552  ltrmxnn0  35553  lermxnn0  35554  jm2.24nn  35563  jm2.24  35567  jm2.19  35602  jm2.26lem3  35610  jm2.27c  35616  hbt  35743  dgraa0p  35762  binomcxplemnn0  36383  fsumnncl  37273  mccllem  37297  ioodvbdlimc1lem2  37424  ioodvbdlimc2lem  37426  dvnxpaek  37434  dvnmul  37435  dvnprodlem2  37439  stoweidlem17  37494  stoweidlem24  37501  wallispilem5  37548  stirlinglem15  37567  fourierdlem48  37634  fourierdlem83  37669  fourierdlem103  37689  fourierdlem104  37690  sqwvfoura  37708  elaa2lem  37713  etransclem10  37724  etransclem19  37733  etransclem20  37734  etransclem21  37735  etransclem22  37736  etransclem23  37737  etransclem24  37738  etransclem27  37741  etransclem32  37746  etransclem35  37749  etransclem44  37758  etransclem45  37759  etransclem46  37760  etransclem47  37761  etransclem48  37762  etransc  37763  gcdzeq  38240  pfxsuffeqwrdeq  38394  ssnn0ssfz  38947  pgrple2abl  38967  nn0eo  39153  fllog2  39197  aacllem  39358
  Copyright terms: Public domain W3C validator