Theorem nn0red 11618

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

Step	Hyp	Ref	Expression
1		nn0ssre 11563	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sseldi 3796	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2156  ℝcr 10220  ℕ₀cn0 11559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-i2m1 10289  ax-1ne0 10290  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-ov 6877  df-om 7296  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-nn 11306  df-n0 11560

This theorem is referenced by:  nn0cnd  11619  nn0readdcl  11623  eluzmn  11911  flmulnn0  12852  quoremz  12878  quoremnn0ALT  12880  modaddmodup  12957  modaddmodlo  12958  expneg  13091  expnbnd  13216  facdiv  13294  faclbnd6  13306  hashdom  13386  hashun2  13390  hashunx  13393  hashfun  13441  hashf1  13458  seqcoll2  13466  hashge2el2dif  13479  hashtpg  13484  wrdlenge2n0  13553  ccatsymb  13579  ccatrn  13586  ccatalpha  13590  ccat2s1fvw  13638  swrdnd  13656  swrdccat3blem  13719  cshwidxmod  13773  repswcshw  13782  swrds2  13909  modfsummods  14747  climcnds  14805  geomulcvg  14829  mertenslem1  14837  binomfallfaclem2  14991  binomrisefac  14993  fallfacval4  14994  efcllem  15028  eftlub  15059  ruclem10  15188  oddge22np1  15293  nn0oddm1d2  15321  bitsfzolem  15375  bitsfzo  15376  bitsmod  15377  sadcaddlem  15398  sadaddlem  15407  sadasslem  15411  sadeq  15413  smuval2  15423  smupvallem  15424  smueqlem  15431  bezoutlem3  15477  bezoutlem4  15478  gcdzeq  15490  dvdssqlem  15498  nn0seqcvgd  15502  eucalglt  15517  lcmneg  15535  mulgcddvds  15587  qredeu  15590  prmdiveq  15708  odzdvds  15717  pythagtriplem3  15740  pythagtriplem6  15743  pythagtriplem7  15744  iserodd  15757  pclem  15760  pcpremul  15765  pcidlem  15793  pcgcd1  15798  pc2dvds  15800  pcz  15802  pcprmpw2  15803  fldivp1  15818  pcfaclem  15819  pcfac  15820  pcbc  15821  prmreclem2  15838  prmreclem3  15839  prmreclem4  15840  prmreclem5  15841  4sqlem11  15876  4sqlem12  15877  4sqlem14  15879  vdwlem11  15912  vdwlem12  15913  ramlb  15940  0ram  15941  ram0  15943  ramub1lem2  15948  ramcl  15950  psgnunilem2  18116  odmodnn0  18160  mndodconglem  18161  mndodcong  18162  oddvds  18167  odhash3  18192  gexdvds  18200  sylow1lem1  18214  sylow1lem5  18218  pgpfi  18221  pgpssslw  18230  efgsfo  18353  efgredlemd  18358  efgredlem  18361  efgred  18362  lt6abl  18497  telgsums  18592  pgpfaclem2  18683  srgbinomlem3  18744  psrbaglesupp  19577  mplmonmul  19673  coe1tmmul2  19854  coe1tmmul2fv  19856  coe1pwmulfv  19858  gsummoncoe1  19882  zringlpirlem3  20042  fvmptnn04if  20867  fvmptnn04ifc  20870  fvmptnn04ifd  20871  chfacfscmulgsum  20878  chfacfpmmulgsum  20882  lebnumii  22978  dyadmaxlem  23578  mbfi1fseqlem3  23698  mbfi1fseqlem4  23699  mbfi1fseqlem5  23700  mdegmullem  24052  coe1mul3  24073  coe1mul4  24074  deg1sublt  24084  deg1mul2  24088  deg1tmle  24091  deg1tm  24092  ply1divmo  24109  ply1divex  24110  deg1submon1p  24126  dvdsq1p  24134  fta1glem2  24140  fta1blem  24142  plyco0  24162  plyeq0lem  24180  plypf1  24182  plyaddlem1  24183  coeeulem  24194  dgrub  24204  dgrlb  24206  dgreq  24214  coeaddlem  24219  coemullem  24220  coemulhi  24224  dgrlt  24236  dgradd2  24238  dgrmul  24240  dgrcolem2  24244  dgrco  24245  plydivlem3  24264  plydivlem4  24265  plydivex  24266  plydiveu  24267  fta1lem  24276  quotcan  24278  vieta1lem2  24280  radcnvlem1  24381  dvradcnv  24389  leibpilem1  24881  leibpi  24883  log2tlbnd  24886  birthdaylem2  24893  birthdaylem3  24894  fsumharmonic  24952  dmlogdmgm  24964  basellem3  25023  basellem5  25025  issqf  25076  ppip1le  25101  ppiltx  25117  mumullem2  25120  sgmppw  25136  ppiub  25143  chtublem  25150  chpub  25159  dchrabs  25199  bcmono  25216  bcmax  25217  bcp1ctr  25218  bclbnd  25219  bposlem5  25227  gausslemma2dlem0h  25302  gausslemma2dlem4  25308  gausslemma2dlem6  25311  lgseisenlem1  25314  2lgsoddprmlem2  25348  2sqlem7  25363  2sqlem8  25365  chebbnd1lem1  25372  chtppilimlem1  25376  dchrisum0re  25416  mulogsumlem  25434  selberg2lem  25453  pntrlog2bndlem4  25483  pntlemr  25505  pntlemj  25506  pnt  25517  ostth2lem3  25538  vtxdgfival  26593  vtxdfiun  26606  vtxdginducedm1fi  26668  crctcsh  26945  wwlksnred  27029  wwlksnextproplem2  27048  rusgrnumwwlks  27116  eupth2lems  27411  eucrct2eupth  27418  numclwlk1lem1  27549  numclwwlk5  27576  numclwwlk6  27578  friendshipgt3  27586  nnmulge  29842  nndiffz1  29875  2sqmod  29973  nexple  30396  oddpwdc  30741  eulerpartlems  30747  eulerpartlemgc  30749  eulerpartlemb  30755  coinfliplem  30865  signsplypnf  30952  signslema  30964  signstfvc  30976  signstfveq0  30979  fsum2dsub  31010  reprlt  31022  reprgt  31024  reprinfz1  31025  breprexplemc  31035  erdszelem8  31503  erdsze2lem2  31509  cvmliftlem7  31596  snmlff  31634  bcprod  31946  poimirlem3  33725  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem10  33732  poimirlem11  33733  poimirlem12  33734  poimirlem13  33735  poimirlem15  33737  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem20  33742  poimirlem21  33743  poimirlem22  33744  poimirlem23  33745  poimirlem24  33746  poimirlem25  33747  poimirlem26  33748  poimirlem29  33751  poimirlem30  33752  poimirlem31  33753  rrnequiv  33945  eldioph2lem1  37825  pell1qrge1  37936  rmxypos  38015  ltrmynn0  38016  ltrmxnn0  38017  lermxnn0  38018  jm2.24nn  38027  jm2.24  38031  jm2.19  38061  jm2.26lem3  38069  jm2.27c  38075  hbt  38201  dgraa0p  38220  binomcxplemnn0  39048  fsumnncl  40283  mccllem  40309  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnxpaek  40637  dvnmul  40638  dvnprodlem2  40642  stoweidlem17  40713  stoweidlem24  40720  wallispilem5  40765  stirlinglem15  40784  fourierdlem48  40850  fourierdlem83  40885  fourierdlem103  40905  fourierdlem104  40906  sqwvfoura  40924  elaa2lem  40929  etransclem10  40940  etransclem19  40949  etransclem20  40950  etransclem21  40951  etransclem22  40952  etransclem23  40953  etransclem24  40954  etransclem27  40957  etransclem32  40962  etransclem35  40965  etransclem44  40974  etransclem45  40975  etransclem46  40976  etransclem47  40977  etransclem48  40978  etransc  40979  rrndistlt  40989  pfxsuffeqwrdeq  41981  fmtnoge3  42017  sqrtpwpw2p  42025  fmtnosqrt  42026  flsqrt  42083  lighneallem4a  42100  ssnn0ssfz  42695  pgrple2abl  42714  nn0eo  42890  fllog2  42930  aacllem  43118