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

Theorem nn0red 11195
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 11139 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3561 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975  cr 9787  0cn0 11135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-i2m1 9856  ax-1ne0 9857  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-ov 6526  df-om 6931  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-nn 10864  df-n0 11136
This theorem is referenced by:  nn0cnd  11196  nn0readdcl  11200  eluzmn  11522  flmulnn0  12441  quoremz  12467  quoremnn0ALT  12469  modaddmodup  12546  modaddmodlo  12547  expneg  12681  expnbnd  12806  facdiv  12887  faclbnd6  12899  hashdom  12977  hashun2  12981  hashunx  12984  hashfun  13032  hashf1  13046  seqcoll2  13054  hashge2el2dif  13063  hashtpg  13067  wrdlenge2n0  13138  ccatsymb  13161  ccatrn  13167  ccatalpha  13170  ccat2s1fvw  13209  swrdnd  13226  swrdccat3blem  13288  cshwidxmod  13342  repswcshw  13351  swrds2  13475  modfsummods  14308  climcnds  14364  geomulcvg  14388  mertenslem1  14397  binomfallfaclem2  14552  binomrisefac  14554  fallfacval4  14555  efcllem  14589  eftlub  14620  ruclem10  14749  oddge22np1  14853  nn0oddm1d2  14881  bitsfzolem  14936  bitsfzo  14937  bitsmod  14938  sadcaddlem  14959  sadaddlem  14968  sadasslem  14972  sadeq  14974  smuval2  14984  smupvallem  14985  smueqlem  14992  bezoutlem3  15038  bezoutlem4  15039  gcdzeq  15051  dvdssqlem  15059  nn0seqcvgd  15063  eucalglt  15078  lcmneg  15096  mulgcddvds  15149  qredeu  15152  prmdiveq  15271  odzdvds  15280  pythagtriplem3  15303  pythagtriplem6  15306  pythagtriplem7  15307  iserodd  15320  pclem  15323  pcpremul  15328  pcidlem  15356  pcgcd1  15361  pc2dvds  15363  pcz  15365  pcprmpw2  15366  fldivp1  15381  pcfaclem  15382  pcfac  15383  pcbc  15384  prmreclem2  15401  prmreclem3  15402  prmreclem4  15403  prmreclem5  15404  4sqlem11  15439  4sqlem12  15440  4sqlem14  15442  vdwlem11  15475  vdwlem12  15476  ramlb  15503  0ram  15504  ram0  15506  ramub1lem2  15511  ramcl  15513  psgnunilem2  17680  odmodnn0  17724  mndodconglem  17725  mndodcong  17726  oddvds  17731  odhash3  17756  gexdvds  17764  sylow1lem1  17778  sylow1lem5  17782  pgpfi  17785  pgpssslw  17794  efgsfo  17917  efgredlemd  17922  efgredlem  17925  efgred  17926  lt6abl  18061  telgsums  18155  pgpfaclem2  18246  srgbinomlem3  18307  psrbaglesupp  19131  mplmonmul  19227  coe1tmmul2  19409  coe1tmmul2fv  19411  coe1pwmulfv  19413  gsummoncoe1  19437  zringlpirlem3  19595  fvmptnn04if  20411  fvmptnn04ifc  20414  fvmptnn04ifd  20415  chfacfscmulgsum  20422  chfacfpmmulgsum  20426  lebnumii  22500  dyadmaxlem  23084  mbfi1fseqlem3  23203  mbfi1fseqlem4  23204  mbfi1fseqlem5  23205  mdegmullem  23555  coe1mul3  23576  coe1mul4  23577  deg1sublt  23587  deg1mul2  23591  deg1tmle  23594  deg1tm  23595  ply1divmo  23612  ply1divex  23613  deg1submon1p  23629  dvdsq1p  23637  fta1glem2  23643  fta1blem  23645  plyco0  23665  plyeq0lem  23683  plypf1  23685  plyaddlem1  23686  coeeulem  23697  dgrub  23707  dgrlb  23709  dgreq  23717  coeaddlem  23722  coemullem  23723  coemulhi  23727  dgrlt  23739  dgradd2  23741  dgrmul  23743  dgrcolem2  23747  dgrco  23748  plydivlem3  23767  plydivlem4  23768  plydivex  23769  plydiveu  23770  fta1lem  23779  quotcan  23781  vieta1lem2  23783  radcnvlem1  23884  dvradcnv  23892  leibpilem1  24380  leibpi  24382  log2tlbnd  24385  birthdaylem2  24392  birthdaylem3  24393  fsumharmonic  24451  dmlogdmgm  24463  basellem3  24522  basellem5  24524  issqf  24575  ppip1le  24600  ppiltx  24616  mumullem2  24619  sgmppw  24635  ppiub  24642  chtublem  24649  chpub  24658  dchrabs  24698  bcmono  24715  bcmax  24716  bcp1ctr  24717  bclbnd  24718  bposlem5  24726  gausslemma2dlem0h  24801  gausslemma2dlem4  24807  gausslemma2dlem6  24810  lgseisenlem1  24813  2lgsoddprmlem2  24847  2sqlem7  24862  2sqlem8  24864  chebbnd1lem1  24871  chtppilimlem1  24875  dchrisum0re  24915  mulogsumlem  24933  selberg2lem  24952  pntrlog2bndlem4  24982  pntlemr  25004  pntlemj  25005  pnt  25016  ostth2lem3  25037  spthispth  25865  wwlknred  26013  wwlkextproplem2  26032  vdgrfival  26186  nbhashuvtx1  26204  rusgranumwlks  26245  eupap1  26265  eupath2lem3  26268  frghash2spot  26352  usgreghash2spotv  26355  numclwwlk5  26401  numclwwlk6  26402  friendshipgt3  26410  nndiffz1  28738  2sqmod  28781  nexple  29201  oddpwdc  29545  eulerpartlems  29551  eulerpartlemgc  29553  eulerpartlemb  29559  coinfliplem  29669  signsplypnf  29755  signslema  29767  signstfvc  29779  signstfveq0  29782  erdszelem8  30236  erdsze2lem2  30242  cvmliftlem7  30329  snmlff  30367  bcprod  30679  poimirlem3  32381  poimirlem4  32382  poimirlem6  32384  poimirlem7  32385  poimirlem10  32388  poimirlem11  32389  poimirlem12  32390  poimirlem13  32391  poimirlem15  32393  poimirlem16  32394  poimirlem17  32395  poimirlem19  32397  poimirlem20  32398  poimirlem21  32399  poimirlem22  32400  poimirlem23  32401  poimirlem24  32402  poimirlem25  32403  poimirlem26  32404  poimirlem29  32407  poimirlem30  32408  poimirlem31  32409  rrnequiv  32603  eldioph2lem1  36140  pell1qrge1  36251  rmxypos  36331  ltrmynn0  36332  ltrmxnn0  36333  lermxnn0  36334  jm2.24nn  36343  jm2.24  36347  jm2.19  36377  jm2.26lem3  36385  jm2.27c  36391  hbt  36518  dgraa0p  36537  binomcxplemnn0  37369  fsumnncl  38438  mccllem  38464  ioodvbdlimc1lem2  38622  ioodvbdlimc2lem  38624  dvnxpaek  38632  dvnmul  38633  dvnprodlem2  38637  stoweidlem17  38710  stoweidlem24  38717  wallispilem5  38762  stirlinglem15  38781  fourierdlem48  38847  fourierdlem83  38882  fourierdlem103  38902  fourierdlem104  38903  sqwvfoura  38921  elaa2lem  38926  etransclem10  38937  etransclem19  38946  etransclem20  38947  etransclem21  38948  etransclem22  38949  etransclem23  38950  etransclem24  38951  etransclem27  38954  etransclem32  38959  etransclem35  38962  etransclem44  38971  etransclem45  38972  etransclem46  38973  etransclem47  38974  etransclem48  38975  etransc  38976  rrndistlt  38986  fmtnoge3  39781  sqrtpwpw2p  39789  fmtnosqrt  39790  flsqrt  39847  lighneallem4a  39864  pfxsuffeqwrdeq  40070  vtxdgfival  40683  vtxdfiun  40695  crctcsh  41025  wwlksnred  41096  wwlksnextproplem2  41114  rusgrnumwwlks  41175  eupth2lems  41404  eucrct2eupth  41411  frgrhash2wsp  41495  fusgreghash2wspv  41497  av-numclwwlk5  41540  av-numclwwlk6  41542  av-friendshipgt3  41550  ssnn0ssfz  41918  pgrple2abl  41938  nn0eo  42114  fllog2  42158  aacllem  42315
  Copyright terms: Public domain W3C validator