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

Theorem nn0red 11390
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 11334 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3634 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cr 9973  0cn0 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-nn 11059  df-n0 11331
This theorem is referenced by:  nn0cnd  11391  nn0readdcl  11395  eluzmn  11732  flmulnn0  12668  quoremz  12694  quoremnn0ALT  12696  modaddmodup  12773  modaddmodlo  12774  expneg  12908  expnbnd  13033  facdiv  13114  faclbnd6  13126  hashdom  13206  hashun2  13210  hashunx  13213  hashfun  13262  hashf1  13279  seqcoll2  13287  hashge2el2dif  13300  hashtpg  13305  wrdlenge2n0  13374  ccatsymb  13400  ccatrn  13407  ccatalpha  13411  ccat2s1fvw  13460  swrdnd  13478  swrdccat3blem  13541  cshwidxmod  13595  repswcshw  13604  swrds2  13731  modfsummods  14569  climcnds  14627  geomulcvg  14651  mertenslem1  14660  binomfallfaclem2  14815  binomrisefac  14817  fallfacval4  14818  efcllem  14852  eftlub  14883  ruclem10  15012  oddge22np1  15120  nn0oddm1d2  15148  bitsfzolem  15203  bitsfzo  15204  bitsmod  15205  sadcaddlem  15226  sadaddlem  15235  sadasslem  15239  sadeq  15241  smuval2  15251  smupvallem  15252  smueqlem  15259  bezoutlem3  15305  bezoutlem4  15306  gcdzeq  15318  dvdssqlem  15326  nn0seqcvgd  15330  eucalglt  15345  lcmneg  15363  mulgcddvds  15416  qredeu  15419  prmdiveq  15538  odzdvds  15547  pythagtriplem3  15570  pythagtriplem6  15573  pythagtriplem7  15574  iserodd  15587  pclem  15590  pcpremul  15595  pcidlem  15623  pcgcd1  15628  pc2dvds  15630  pcz  15632  pcprmpw2  15633  fldivp1  15648  pcfaclem  15649  pcfac  15650  pcbc  15651  prmreclem2  15668  prmreclem3  15669  prmreclem4  15670  prmreclem5  15671  4sqlem11  15706  4sqlem12  15707  4sqlem14  15709  vdwlem11  15742  vdwlem12  15743  ramlb  15770  0ram  15771  ram0  15773  ramub1lem2  15778  ramcl  15780  psgnunilem2  17961  odmodnn0  18005  mndodconglem  18006  mndodcong  18007  oddvds  18012  odhash3  18037  gexdvds  18045  sylow1lem1  18059  sylow1lem5  18063  pgpfi  18066  pgpssslw  18075  efgsfo  18198  efgredlemd  18203  efgredlem  18206  efgred  18207  lt6abl  18342  telgsums  18436  pgpfaclem2  18527  srgbinomlem3  18588  psrbaglesupp  19416  mplmonmul  19512  coe1tmmul2  19694  coe1tmmul2fv  19696  coe1pwmulfv  19698  gsummoncoe1  19722  zringlpirlem3  19882  fvmptnn04if  20702  fvmptnn04ifc  20705  fvmptnn04ifd  20706  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  lebnumii  22812  dyadmaxlem  23411  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mdegmullem  23883  coe1mul3  23904  coe1mul4  23905  deg1sublt  23915  deg1mul2  23919  deg1tmle  23922  deg1tm  23923  ply1divmo  23940  ply1divex  23941  deg1submon1p  23957  dvdsq1p  23965  fta1glem2  23971  fta1blem  23973  plyco0  23993  plyeq0lem  24011  plypf1  24013  plyaddlem1  24014  coeeulem  24025  dgrub  24035  dgrlb  24037  dgreq  24045  coeaddlem  24050  coemullem  24051  coemulhi  24055  dgrlt  24067  dgradd2  24069  dgrmul  24071  dgrcolem2  24075  dgrco  24076  plydivlem3  24095  plydivlem4  24096  plydivex  24097  plydiveu  24098  fta1lem  24107  quotcan  24109  vieta1lem2  24111  radcnvlem1  24212  dvradcnv  24220  leibpilem1  24712  leibpi  24714  log2tlbnd  24717  birthdaylem2  24724  birthdaylem3  24725  fsumharmonic  24783  dmlogdmgm  24795  basellem3  24854  basellem5  24856  issqf  24907  ppip1le  24932  ppiltx  24948  mumullem2  24951  sgmppw  24967  ppiub  24974  chtublem  24981  chpub  24990  dchrabs  25030  bcmono  25047  bcmax  25048  bcp1ctr  25049  bclbnd  25050  bposlem5  25058  gausslemma2dlem0h  25133  gausslemma2dlem4  25139  gausslemma2dlem6  25142  lgseisenlem1  25145  2lgsoddprmlem2  25179  2sqlem7  25194  2sqlem8  25196  chebbnd1lem1  25203  chtppilimlem1  25207  dchrisum0re  25247  mulogsumlem  25265  selberg2lem  25284  pntrlog2bndlem4  25314  pntlemr  25336  pntlemj  25337  pnt  25348  ostth2lem3  25369  vtxdgfival  26421  vtxdfiun  26434  vtxdginducedm1fi  26496  crctcsh  26772  wwlksnred  26855  wwlksnextproplem2  26873  rusgrnumwwlks  26941  eupth2lems  27216  eucrct2eupth  27223  numclwwlk5  27375  numclwwlk6  27377  friendshipgt3  27385  nnmulge  29643  nndiffz1  29676  2sqmod  29776  nexple  30199  oddpwdc  30544  eulerpartlems  30550  eulerpartlemgc  30552  eulerpartlemb  30558  coinfliplem  30668  signsplypnf  30755  signslema  30767  signstfvc  30779  signstfveq0  30782  fsum2dsub  30813  reprlt  30825  reprgt  30827  reprinfz1  30828  breprexplemc  30838  erdszelem8  31306  erdsze2lem2  31312  cvmliftlem7  31399  snmlff  31437  bcprod  31750  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  rrnequiv  33764  eldioph2lem1  37640  pell1qrge1  37751  rmxypos  37831  ltrmynn0  37832  ltrmxnn0  37833  lermxnn0  37834  jm2.24nn  37843  jm2.24  37847  jm2.19  37877  jm2.26lem3  37885  jm2.27c  37891  hbt  38017  dgraa0p  38036  binomcxplemnn0  38865  fsumnncl  40121  mccllem  40147  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnxpaek  40475  dvnmul  40476  dvnprodlem2  40480  stoweidlem17  40552  stoweidlem24  40559  wallispilem5  40604  stirlinglem15  40623  fourierdlem48  40689  fourierdlem83  40724  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  elaa2lem  40768  etransclem10  40779  etransclem19  40788  etransclem20  40789  etransclem21  40790  etransclem22  40791  etransclem23  40792  etransclem24  40793  etransclem27  40796  etransclem32  40801  etransclem35  40804  etransclem44  40813  etransclem45  40814  etransclem46  40815  etransclem47  40816  etransclem48  40817  etransc  40818  rrndistlt  40828  pfxsuffeqwrdeq  41731  fmtnoge3  41767  sqrtpwpw2p  41775  fmtnosqrt  41776  flsqrt  41833  lighneallem4a  41850  ssnn0ssfz  42452  pgrple2abl  42471  nn0eo  42647  fllog2  42687  aacllem  42875
  Copyright terms: Public domain W3C validator