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

Theorem nn0red 11934
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 11879 . 2 0 ⊆ ℝ
2 nn0red.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3941 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  cr 10513  0cn0 11875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-i2m1 10582  ax-1ne0 10583  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7133  df-om 7556  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-nn 11616  df-n0 11876
This theorem is referenced by:  nn0cnd  11935  nn0readdcl  11939  eluzmn  12228  flmulnn0  13180  quoremz  13206  quoremnn0ALT  13208  modaddmodup  13285  modaddmodlo  13286  expneg  13421  expnbnd  13577  facdiv  13631  faclbnd6  13643  hashdom  13724  hashun2  13728  hashunx  13731  hashfun  13782  hashf1  13799  seqcoll2  13807  hashge2el2dif  13822  hashtpg  13827  wrdlenge2n0  13883  ccatsymb  13915  ccatrn  13922  ccatalpha  13926  ccat2s1fvw  13977  ccat2s1fvwOLD  13978  swrdnd  13995  swrdnd0  13998  pfxnd0  14029  pfxsuffeqwrdeq  14039  swrdccat3blem  14080  cshwidxmod  14144  repswcshw  14153  swrds2  14281  modfsummods  15127  climcnds  15185  geomulcvg  15211  mertenslem1  15219  binomfallfaclem2  15373  binomrisefac  15375  fallfacval4  15376  efcllem  15410  eftlub  15441  ruclem10  15571  oddge22np1  15677  nn0oddm1d2  15713  divalglem5  15725  bitsfzolem  15760  bitsfzo  15761  bitsmod  15762  sadcaddlem  15783  sadaddlem  15792  sadasslem  15796  sadeq  15798  smuval2  15808  smupvallem  15809  smueqlem  15816  bezoutlem3  15866  bezoutlem4  15867  gcdzeq  15879  dvdssqlem  15887  nn0seqcvgd  15891  eucalglt  15906  lcmneg  15924  mulgcddvds  15976  qredeu  15979  prmdiveq  16100  odzdvds  16109  pythagtriplem3  16132  pythagtriplem6  16135  pythagtriplem7  16136  iserodd  16149  pclem  16152  pcpremul  16157  pcidlem  16185  pcgcd1  16190  pc2dvds  16192  pcz  16194  pcprmpw2  16195  fldivp1  16210  pcfaclem  16211  pcfac  16212  pcbc  16213  prmreclem2  16230  prmreclem3  16231  prmreclem4  16232  prmreclem5  16233  4sqlem11  16268  4sqlem12  16269  4sqlem14  16271  vdwlem11  16304  vdwlem12  16305  ramlb  16332  0ram  16333  ram0  16335  ramub1lem2  16340  ramcl  16342  psgnunilem2  18602  odmodnn0  18647  mndodconglem  18648  mndodcong  18649  oddvds  18654  odhash3  18680  gexdvds  18688  sylow1lem1  18702  sylow1lem5  18706  pgpfi  18709  pgpssslw  18718  efgsfo  18844  efgredlemd  18849  efgredlem  18852  efgred  18853  lt6abl  18994  telgsums  19092  pgpfaclem2  19183  srgbinomlem3  19271  psrbaglesupp  20124  mplmonmul  20221  coe1tmmul2  20420  coe1tmmul2fv  20422  coe1pwmulfv  20424  gsummoncoe1  20448  zringlpirlem3  20609  fvmptnn04if  21433  fvmptnn04ifc  21436  fvmptnn04ifd  21437  chfacfscmulgsum  21444  chfacfpmmulgsum  21448  lebnumii  23550  dyadmaxlem  24180  mbfi1fseqlem3  24300  mbfi1fseqlem4  24301  mbfi1fseqlem5  24302  mdegmullem  24658  coe1mul3  24679  coe1mul4  24680  deg1sublt  24690  deg1mul2  24694  deg1tmle  24697  deg1tm  24698  ply1divmo  24715  ply1divex  24716  deg1submon1p  24732  dvdsq1p  24740  fta1glem2  24746  fta1blem  24748  plyco0  24768  plyeq0lem  24786  plypf1  24788  plyaddlem1  24789  coeeulem  24800  dgrub  24810  dgrlb  24812  dgreq  24820  coeaddlem  24825  coemullem  24826  coemulhi  24830  dgrlt  24842  dgradd2  24844  dgrmul  24846  dgrcolem2  24850  dgrco  24851  plydivlem3  24870  plydivlem4  24871  plydivex  24872  plydiveu  24873  fta1lem  24882  quotcan  24884  vieta1lem2  24886  radcnvlem1  24987  dvradcnv  24995  leibpi  25507  log2tlbnd  25510  birthdaylem2  25517  birthdaylem3  25518  fsumharmonic  25576  dmlogdmgm  25588  basellem3  25647  basellem5  25649  issqf  25700  ppip1le  25725  ppiltx  25741  mumullem2  25744  sgmppw  25760  ppiub  25767  chtublem  25774  chpub  25783  dchrabs  25823  bcmono  25840  bcmax  25841  bcp1ctr  25842  bclbnd  25843  bposlem5  25851  gausslemma2dlem0h  25926  gausslemma2dlem4  25932  gausslemma2dlem6  25935  lgseisenlem1  25938  2lgsoddprmlem2  25972  2sqlem7  25987  2sqlem8  25989  2sq2  25996  2sqmod  25999  chebbnd1lem1  26032  chtppilimlem1  26036  dchrisum0re  26076  mulogsumlem  26094  selberg2lem  26113  pntrlog2bndlem4  26143  pntlemr  26165  pntlemj  26166  pnt  26177  ostth2lem3  26198  vtxdgfival  27238  vtxdfiun  27251  vtxdginducedm1fi  27313  crctcsh  27589  wwlksnred  27657  wwlksnextproplem2  27675  rusgrnumwwlks  27739  eupth2lems  28002  eucrct2eupth  28009  numclwlk1lem1  28133  numclwwlk5  28152  numclwwlk6  28154  friendshipgt3  28162  nnmulge  30461  nndiffz1  30496  prmdvdsbc  30519  pfxlsw2ccat  30613  wrdt2ind  30614  cycpmrn  30793  cyc3conja  30807  nexple  31276  oddpwdc  31620  eulerpartlems  31626  eulerpartlemgc  31628  eulerpartlemb  31634  coinfliplem  31744  signsplypnf  31828  signslema  31840  signstfvc  31852  signstfveq0  31855  fsum2dsub  31886  reprlt  31898  reprgt  31900  reprinfz1  31901  breprexplemc  31911  lpadmax  31961  lpadright  31963  usgrgt2cycl  32385  acycgr1v  32404  erdszelem8  32453  erdsze2lem2  32459  cvmliftlem7  32546  snmlff  32584  bcprod  32978  poimirlem3  34942  poimirlem4  34943  poimirlem6  34945  poimirlem7  34946  poimirlem10  34949  poimirlem11  34950  poimirlem12  34951  poimirlem13  34952  poimirlem15  34954  poimirlem16  34955  poimirlem17  34956  poimirlem19  34958  poimirlem20  34959  poimirlem21  34960  poimirlem22  34961  poimirlem23  34962  poimirlem24  34963  poimirlem25  34964  poimirlem26  34965  poimirlem29  34968  poimirlem30  34969  poimirlem31  34970  rrnequiv  35155  lcmineqlem17  39208  lcmineqlem21  39212  frlmvscadiccat  39271  fltnltalem  39425  eldioph2lem1  39508  pell1qrge1  39618  rmxypos  39695  ltrmynn0  39696  ltrmxnn0  39697  lermxnn0  39698  jm2.24nn  39707  jm2.24  39711  jm2.19  39741  jm2.26lem3  39749  jm2.27c  39755  hbt  39881  dgraa0p  39900  binomcxplemnn0  40864  fsumnncl  42032  mccllem  42058  ioodvbdlimc1lem2  42393  ioodvbdlimc2lem  42395  dvnxpaek  42403  dvnmul  42404  dvnprodlem2  42408  stoweidlem17  42478  stoweidlem24  42485  wallispilem5  42530  stirlinglem15  42549  fourierdlem48  42615  fourierdlem83  42650  fourierdlem103  42670  fourierdlem104  42671  sqwvfoura  42689  elaa2lem  42694  etransclem10  42705  etransclem19  42714  etransclem20  42715  etransclem21  42716  etransclem22  42717  etransclem23  42718  etransclem24  42719  etransclem27  42722  etransclem32  42727  etransclem35  42730  etransclem44  42739  etransclem45  42740  etransclem46  42741  etransclem47  42742  etransclem48  42743  etransc  42744  rrndistlt  42751  fmtnoge3  43866  sqrtpwpw2p  43874  fmtnosqrt  43875  flsqrt  43929  lighneallem4a  43945  ssnn0ssfz  44569  pgrple2abl  44585  nn0eo  44760  fllog2  44800  itcovalt2lem2lem1  44894  aacllem  45136
  Copyright terms: Public domain W3C validator