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

Theorem nn0red 11312
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0red (𝜑𝐴 ∈ ℝ)

Proof of Theorem nn0red
StepHypRef Expression
1 nn0ssre 11256 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3586 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cr 9895  0cn0 11252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-i2m1 9964  ax-1ne0 9965  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-ov 6618  df-om 7028  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-nn 10981  df-n0 11253
This theorem is referenced by:  nn0cnd  11313  nn0readdcl  11317  eluzmn  11654  flmulnn0  12584  quoremz  12610  quoremnn0ALT  12612  modaddmodup  12689  modaddmodlo  12690  expneg  12824  expnbnd  12949  facdiv  13030  faclbnd6  13042  hashdom  13124  hashun2  13128  hashunx  13131  hashfun  13180  hashf1  13195  seqcoll2  13203  hashge2el2dif  13216  hashtpg  13221  wrdlenge2n0  13296  ccatsymb  13321  ccatrn  13327  ccatalpha  13330  ccat2s1fvw  13369  swrdnd  13386  swrdccat3blem  13448  cshwidxmod  13502  repswcshw  13511  swrds2  13635  modfsummods  14471  climcnds  14527  geomulcvg  14551  mertenslem1  14560  binomfallfaclem2  14715  binomrisefac  14717  fallfacval4  14718  efcllem  14752  eftlub  14783  ruclem10  14912  oddge22np1  15016  nn0oddm1d2  15044  bitsfzolem  15099  bitsfzo  15100  bitsmod  15101  sadcaddlem  15122  sadaddlem  15131  sadasslem  15135  sadeq  15137  smuval2  15147  smupvallem  15148  smueqlem  15155  bezoutlem3  15201  bezoutlem4  15202  gcdzeq  15214  dvdssqlem  15222  nn0seqcvgd  15226  eucalglt  15241  lcmneg  15259  mulgcddvds  15312  qredeu  15315  prmdiveq  15434  odzdvds  15443  pythagtriplem3  15466  pythagtriplem6  15469  pythagtriplem7  15470  iserodd  15483  pclem  15486  pcpremul  15491  pcidlem  15519  pcgcd1  15524  pc2dvds  15526  pcz  15528  pcprmpw2  15529  fldivp1  15544  pcfaclem  15545  pcfac  15546  pcbc  15547  prmreclem2  15564  prmreclem3  15565  prmreclem4  15566  prmreclem5  15567  4sqlem11  15602  4sqlem12  15603  4sqlem14  15605  vdwlem11  15638  vdwlem12  15639  ramlb  15666  0ram  15667  ram0  15669  ramub1lem2  15674  ramcl  15676  psgnunilem2  17855  odmodnn0  17899  mndodconglem  17900  mndodcong  17901  oddvds  17906  odhash3  17931  gexdvds  17939  sylow1lem1  17953  sylow1lem5  17957  pgpfi  17960  pgpssslw  17969  efgsfo  18092  efgredlemd  18097  efgredlem  18100  efgred  18101  lt6abl  18236  telgsums  18330  pgpfaclem2  18421  srgbinomlem3  18482  psrbaglesupp  19308  mplmonmul  19404  coe1tmmul2  19586  coe1tmmul2fv  19588  coe1pwmulfv  19590  gsummoncoe1  19614  zringlpirlem3  19774  fvmptnn04if  20594  fvmptnn04ifc  20597  fvmptnn04ifd  20598  chfacfscmulgsum  20605  chfacfpmmulgsum  20609  lebnumii  22705  dyadmaxlem  23305  mbfi1fseqlem3  23424  mbfi1fseqlem4  23425  mbfi1fseqlem5  23426  mdegmullem  23776  coe1mul3  23797  coe1mul4  23798  deg1sublt  23808  deg1mul2  23812  deg1tmle  23815  deg1tm  23816  ply1divmo  23833  ply1divex  23834  deg1submon1p  23850  dvdsq1p  23858  fta1glem2  23864  fta1blem  23866  plyco0  23886  plyeq0lem  23904  plypf1  23906  plyaddlem1  23907  coeeulem  23918  dgrub  23928  dgrlb  23930  dgreq  23938  coeaddlem  23943  coemullem  23944  coemulhi  23948  dgrlt  23960  dgradd2  23962  dgrmul  23964  dgrcolem2  23968  dgrco  23969  plydivlem3  23988  plydivlem4  23989  plydivex  23990  plydiveu  23991  fta1lem  24000  quotcan  24002  vieta1lem2  24004  radcnvlem1  24105  dvradcnv  24113  leibpilem1  24601  leibpi  24603  log2tlbnd  24606  birthdaylem2  24613  birthdaylem3  24614  fsumharmonic  24672  dmlogdmgm  24684  basellem3  24743  basellem5  24745  issqf  24796  ppip1le  24821  ppiltx  24837  mumullem2  24840  sgmppw  24856  ppiub  24863  chtublem  24870  chpub  24879  dchrabs  24919  bcmono  24936  bcmax  24937  bcp1ctr  24938  bclbnd  24939  bposlem5  24947  gausslemma2dlem0h  25022  gausslemma2dlem4  25028  gausslemma2dlem6  25031  lgseisenlem1  25034  2lgsoddprmlem2  25068  2sqlem7  25083  2sqlem8  25085  chebbnd1lem1  25092  chtppilimlem1  25096  dchrisum0re  25136  mulogsumlem  25154  selberg2lem  25173  pntrlog2bndlem4  25203  pntlemr  25225  pntlemj  25226  pnt  25237  ostth2lem3  25258  vtxdgfival  26286  vtxdfiun  26298  crctcsh  26619  wwlksnred  26690  wwlksnextproplem2  26708  rusgrnumwwlks  26770  eupth2lems  26998  eucrct2eupth  27005  frgrhash2wsp  27089  fusgreghash2wspv  27091  numclwwlk5  27134  numclwwlk6  27136  friendshipgt3  27144  nndiffz1  29431  2sqmod  29475  nexple  29895  oddpwdc  30239  eulerpartlems  30245  eulerpartlemgc  30247  eulerpartlemb  30253  coinfliplem  30363  signsplypnf  30449  signslema  30461  signstfvc  30473  signstfveq0  30476  erdszelem8  30941  erdsze2lem2  30947  cvmliftlem7  31034  snmlff  31072  bcprod  31385  poimirlem3  33083  poimirlem4  33084  poimirlem6  33086  poimirlem7  33087  poimirlem10  33090  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem15  33095  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem21  33101  poimirlem22  33102  poimirlem23  33103  poimirlem24  33104  poimirlem25  33105  poimirlem26  33106  poimirlem29  33109  poimirlem30  33110  poimirlem31  33111  rrnequiv  33305  eldioph2lem1  36842  pell1qrge1  36953  rmxypos  37033  ltrmynn0  37034  ltrmxnn0  37035  lermxnn0  37036  jm2.24nn  37045  jm2.24  37049  jm2.19  37079  jm2.26lem3  37087  jm2.27c  37093  hbt  37220  dgraa0p  37239  binomcxplemnn0  38069  fsumnncl  39239  mccllem  39265  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnxpaek  39494  dvnmul  39495  dvnprodlem2  39499  stoweidlem17  39571  stoweidlem24  39578  wallispilem5  39623  stirlinglem15  39642  fourierdlem48  39708  fourierdlem83  39743  fourierdlem103  39763  fourierdlem104  39764  sqwvfoura  39782  elaa2lem  39787  etransclem10  39798  etransclem19  39807  etransclem20  39808  etransclem21  39809  etransclem22  39810  etransclem23  39811  etransclem24  39812  etransclem27  39815  etransclem32  39820  etransclem35  39823  etransclem44  39832  etransclem45  39833  etransclem46  39834  etransclem47  39835  etransclem48  39836  etransc  39837  rrndistlt  39847  pfxsuffeqwrdeq  40735  fmtnoge3  40771  sqrtpwpw2p  40779  fmtnosqrt  40780  flsqrt  40837  lighneallem4a  40854  ssnn0ssfz  41445  pgrple2abl  41464  nn0eo  41640  fllog2  41684  aacllem  41880
  Copyright terms: Public domain W3C validator