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

Theorem nn0red 12566
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 12509 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sselid 3974 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2098  cr 11139  0cn0 12505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-i2m1 11208  ax-1ne0 11209  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-nn 12246  df-n0 12506
This theorem is referenced by:  nn0cnd  12567  nn0readdcl  12571  eluzmn  12862  flmulnn0  13828  quoremz  13856  quoremnn0ALT  13858  modaddmodup  13935  modaddmodlo  13936  expneg  14070  expnbnd  14230  facdiv  14282  faclbnd6  14294  hashdom  14374  hashun2  14378  hashunx  14381  hashfun  14432  hashf1  14454  seqcoll2  14462  hashge2el2dif  14477  hashtpg  14482  wrdlenge2n0  14538  ccatsymb  14568  ccatrn  14575  ccatalpha  14579  ccat2s1fvw  14624  swrdnd  14640  swrdnd0  14643  pfxnd0  14674  pfxsuffeqwrdeq  14684  swrdccat3blem  14725  cshwidxmod  14789  repswcshw  14798  swrds2  14927  modfsummods  15775  climcnds  15833  geomulcvg  15858  mertenslem1  15866  binomfallfaclem2  16020  binomrisefac  16022  fallfacval4  16023  efcllem  16057  eftlub  16089  ruclem10  16219  oddge22np1  16329  nn0oddm1d2  16365  divalglem5  16377  bitsfzolem  16412  bitsfzo  16413  bitsmod  16414  sadcaddlem  16435  sadaddlem  16444  sadasslem  16448  sadeq  16450  smuval2  16460  smupvallem  16461  smueqlem  16468  bezoutlem3  16520  bezoutlem4  16521  gcdzeq  16531  dvdssqlem  16540  nn0seqcvgd  16544  eucalglt  16559  lcmneg  16577  mulgcddvds  16629  qredeu  16632  prmdvdsbc  16701  prmdiveq  16758  odzdvds  16767  pythagtriplem3  16790  pythagtriplem6  16793  pythagtriplem7  16794  iserodd  16807  pclem  16810  pcpremul  16815  pcidlem  16844  pcgcd1  16849  pc2dvds  16851  pcz  16853  pcprmpw2  16854  fldivp1  16869  pcfaclem  16870  pcfac  16871  pcbc  16872  prmreclem2  16889  prmreclem3  16890  prmreclem4  16891  prmreclem5  16892  4sqlem11  16927  4sqlem12  16928  4sqlem14  16930  vdwlem11  16963  vdwlem12  16964  ramlb  16991  0ram  16992  ram0  16994  ramub1lem2  16999  ramcl  17001  psgnunilem2  19462  odmodnn0  19507  mndodconglem  19508  mndodcong  19509  oddvds  19514  odhash3  19543  gexdvds  19551  sylow1lem1  19565  sylow1lem5  19569  pgpfi  19572  pgpssslw  19581  efgsfo  19706  efgredlemd  19711  efgredlem  19714  efgred  19715  lt6abl  19862  telgsums  19960  pgpfaclem2  20051  srgbinomlem3  20180  zringlpirlem3  21407  psrbaglesupp  21874  psrbaglesuppOLD  21875  psrbagcon  21880  psrbagleadd1  21886  mplmonmul  21996  psdmul  22113  coe1tmmul2  22220  coe1tmmul2fv  22222  coe1pwmulfv  22224  gsummoncoe1  22252  fvmptnn04if  22795  fvmptnn04ifc  22798  fvmptnn04ifd  22799  chfacfscmulgsum  22806  chfacfpmmulgsum  22810  lebnumii  24936  dyadmaxlem  25570  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mdegmullem  26058  coe1mul3  26079  coe1mul4  26080  deg1sublt  26090  deg1mul2  26094  deg1tmle  26098  deg1tm  26099  ply1divmo  26116  ply1divex  26117  deg1submon1p  26133  dvdsq1p  26142  fta1glem2  26148  fta1blem  26150  plyco0  26171  plyeq0lem  26189  plypf1  26191  plyaddlem1  26192  coeeulem  26203  dgrub  26213  dgrlb  26215  dgreq  26223  coeaddlem  26228  coemullem  26229  coemulhi  26233  dgrlt  26246  dgradd2  26248  dgrmul  26250  dgrcolem2  26254  dgrco  26255  plydivlem3  26275  plydivlem4  26276  plydivex  26277  plydiveu  26278  fta1lem  26287  quotcan  26289  vieta1lem2  26291  radcnvlem1  26394  dvradcnv  26402  leibpi  26919  log2tlbnd  26922  birthdaylem2  26929  birthdaylem3  26930  fsumharmonic  26989  dmlogdmgm  27001  basellem3  27060  basellem5  27062  issqf  27113  ppip1le  27138  ppiltx  27154  mumullem2  27157  sgmppw  27175  ppiub  27182  chtublem  27189  chpub  27198  dchrabs  27238  bcmono  27255  bcmax  27256  bcp1ctr  27257  bclbnd  27258  bposlem5  27266  gausslemma2dlem0h  27341  gausslemma2dlem4  27347  gausslemma2dlem6  27350  lgseisenlem1  27353  2lgsoddprmlem2  27387  2sqlem7  27402  2sqlem8  27404  2sq2  27411  2sqmod  27414  chebbnd1lem1  27447  chtppilimlem1  27451  dchrisum0re  27491  mulogsumlem  27509  selberg2lem  27528  pntrlog2bndlem4  27558  pntlemr  27580  pntlemj  27581  pnt  27592  ostth2lem3  27613  vtxdgfival  29355  vtxdfiun  29368  vtxdginducedm1fi  29430  crctcsh  29707  wwlksnred  29775  wwlksnextproplem2  29793  rusgrnumwwlks  29857  eupth2lems  30120  eucrct2eupth  30127  numclwlk1lem1  30251  numclwwlk5  30270  numclwwlk6  30272  friendshipgt3  30280  nnmulge  32602  nndiffz1  32636  fzo0opth  32655  suppssnn0  32657  pfxlsw2ccat  32760  wrdt2ind  32763  cycpmrn  32956  cyc3conja  32970  1arithidomlem1  33347  1arithidomlem2  33348  1arithidom  33349  ply1unit  33386  ply1dg3rt0irred  33391  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  ply1degltdimlem  33451  ply1degltdim  33452  minplyirredlem  33511  irredminply  33515  nexple  33759  oddpwdc  34105  eulerpartlems  34111  eulerpartlemgc  34113  eulerpartlemb  34119  coinfliplem  34229  signsplypnf  34313  signslema  34325  signstfvc  34337  signstfveq0  34340  fsum2dsub  34370  reprlt  34382  reprgt  34384  reprinfz1  34385  breprexplemc  34395  lpadmax  34445  lpadright  34447  usgrgt2cycl  34871  acycgr1v  34890  erdszelem8  34939  erdsze2lem2  34945  cvmliftlem7  35032  snmlff  35070  bcprod  35463  poimirlem3  37227  poimirlem4  37228  poimirlem6  37230  poimirlem7  37231  poimirlem10  37234  poimirlem11  37235  poimirlem12  37236  poimirlem13  37237  poimirlem15  37239  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem20  37244  poimirlem21  37245  poimirlem22  37246  poimirlem23  37247  poimirlem24  37248  poimirlem25  37249  poimirlem26  37250  poimirlem29  37253  poimirlem30  37254  poimirlem31  37255  rrnequiv  37439  lcmineqlem17  41648  lcmineqlem21  41652  3lexlogpow5ineq5  41663  aks4d1p1p4  41674  aks4d1p1p7  41677  aks4d1p3  41681  aks4d1p7d1  41685  aks6d1c1  41719  aks6d1c3  41726  aks6d1c2lem4  41730  hashnexinj  41731  aks6d1c2  41733  aks6d1c5lem1  41739  aks6d1c5lem3  41740  aks6d1c5lem2  41741  aks6d1c5  41742  2np3bcnp1  41747  2ap1caineq  41748  sticksstones6  41754  sticksstones7  41755  sticksstones22  41771  aks6d1c6lem3  41775  aks6d1c6lem4  41776  bcled  41781  bcle2d  41782  aks6d1c7lem1  41783  aks6d1c7lem2  41784  frlmvscadiccat  41884  fltnltalem  42221  eldioph2lem1  42322  pell1qrge1  42432  rmxypos  42510  ltrmynn0  42511  ltrmxnn0  42512  lermxnn0  42513  jm2.24nn  42522  jm2.24  42526  jm2.19  42556  jm2.26lem3  42564  jm2.27c  42570  hbt  42696  dgraa0p  42715  binomcxplemnn0  43928  fsumnncl  45098  mccllem  45123  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  dvnxpaek  45468  dvnmul  45469  dvnprodlem2  45473  stoweidlem17  45543  stoweidlem24  45550  wallispilem5  45595  stirlinglem15  45614  fourierdlem48  45680  fourierdlem83  45715  fourierdlem103  45735  fourierdlem104  45736  sqwvfoura  45754  elaa2lem  45759  etransclem10  45770  etransclem19  45779  etransclem20  45780  etransclem21  45781  etransclem22  45782  etransclem23  45783  etransclem24  45784  etransclem27  45787  etransclem32  45792  etransclem35  45795  etransclem44  45804  etransclem45  45805  etransclem46  45806  etransclem47  45807  etransclem48  45808  etransc  45809  rrndistlt  45816  fmtnoge3  47007  sqrtpwpw2p  47015  fmtnosqrt  47016  flsqrt  47070  lighneallem4a  47085  ssnn0ssfz  47599  pgrple2abl  47615  nn0eo  47787  fllog2  47827  itcovalt2lem2lem1  47932  aacllem  48420
  Copyright terms: Public domain W3C validator