Theorem nn0red 11703

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 11646	. 2 ⊢ ℕ0 ⊆ ℝ
2		nn0red.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sseldi 3818	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 10271  ℕ₀cn0 11642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-i2m1 10340  ax-1ne0 10341  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-nn 11375  df-n0 11643

This theorem is referenced by:  nn0cnd  11704  nn0readdcl  11708  eluzmn  11999  flmulnn0  12947  quoremz  12973  quoremnn0ALT  12975  modaddmodup  13052  modaddmodlo  13053  expneg  13186  expnbnd  13312  facdiv  13392  faclbnd6  13404  hashdom  13483  hashun2  13487  hashunx  13490  hashfun  13538  hashf1  13555  seqcoll2  13563  hashge2el2dif  13576  hashtpg  13581  wrdlenge2n0  13642  ccatsymb  13672  ccatrn  13679  ccatalpha  13683  ccat2s1fvw  13728  swrdnd  13749  swrdnd0  13752  pfxnd0  13797  pfxsuffeqwrdeq  13807  swrdccat3blem  13871  cshwidxmod  13954  repswcshw  13963  swrds2  14091  modfsummods  14929  climcnds  14987  geomulcvg  15011  mertenslem1  15019  binomfallfaclem2  15173  binomrisefac  15175  fallfacval4  15176  efcllem  15210  eftlub  15241  ruclem10  15372  oddge22np1  15477  nn0oddm1d2  15515  divalglem5  15527  bitsfzolem  15562  bitsfzo  15563  bitsmod  15564  sadcaddlem  15585  sadaddlem  15594  sadasslem  15598  sadeq  15600  smuval2  15610  smupvallem  15611  smueqlem  15618  bezoutlem3  15664  bezoutlem4  15665  gcdzeq  15677  dvdssqlem  15685  nn0seqcvgd  15689  eucalglt  15704  lcmneg  15722  mulgcddvds  15774  qredeu  15777  prmdiveq  15895  odzdvds  15904  pythagtriplem3  15927  pythagtriplem6  15930  pythagtriplem7  15931  iserodd  15944  pclem  15947  pcpremul  15952  pcidlem  15980  pcgcd1  15985  pc2dvds  15987  pcz  15989  pcprmpw2  15990  fldivp1  16005  pcfaclem  16006  pcfac  16007  pcbc  16008  prmreclem2  16025  prmreclem3  16026  prmreclem4  16027  prmreclem5  16028  4sqlem11  16063  4sqlem12  16064  4sqlem14  16066  vdwlem11  16099  vdwlem12  16100  ramlb  16127  0ram  16128  ram0  16130  ramub1lem2  16135  ramcl  16137  psgnunilem2  18299  odmodnn0  18343  mndodconglem  18344  mndodcong  18345  oddvds  18350  odhash3  18375  gexdvds  18383  sylow1lem1  18397  sylow1lem5  18401  pgpfi  18404  pgpssslw  18413  efgsfo  18537  efgredlemd  18542  efgredlem  18545  efgredlemOLD  18546  efgred  18547  lt6abl  18682  telgsums  18777  pgpfaclem2  18868  srgbinomlem3  18929  psrbaglesupp  19765  mplmonmul  19861  coe1tmmul2  20042  coe1tmmul2fv  20044  coe1pwmulfv  20046  gsummoncoe1  20070  zringlpirlem3  20230  fvmptnn04if  21061  fvmptnn04ifc  21064  fvmptnn04ifd  21065  chfacfscmulgsum  21072  chfacfpmmulgsum  21076  lebnumii  23173  dyadmaxlem  23801  mbfi1fseqlem3  23921  mbfi1fseqlem4  23922  mbfi1fseqlem5  23923  mdegmullem  24275  coe1mul3  24296  coe1mul4  24297  deg1sublt  24307  deg1mul2  24311  deg1tmle  24314  deg1tm  24315  ply1divmo  24332  ply1divex  24333  deg1submon1p  24349  dvdsq1p  24357  fta1glem2  24363  fta1blem  24365  plyco0  24385  plyeq0lem  24403  plypf1  24405  plyaddlem1  24406  coeeulem  24417  dgrub  24427  dgrlb  24429  dgreq  24437  coeaddlem  24442  coemullem  24443  coemulhi  24447  dgrlt  24459  dgradd2  24461  dgrmul  24463  dgrcolem2  24467  dgrco  24468  plydivlem3  24487  plydivlem4  24488  plydivex  24489  plydiveu  24490  fta1lem  24499  quotcan  24501  vieta1lem2  24503  radcnvlem1  24604  dvradcnv  24612  leibpilem1OLD  25119  leibpi  25121  log2tlbnd  25124  birthdaylem2  25131  birthdaylem3  25132  fsumharmonic  25190  dmlogdmgm  25202  basellem3  25261  basellem5  25263  issqf  25314  ppip1le  25339  ppiltx  25355  mumullem2  25358  sgmppw  25374  ppiub  25381  chtublem  25388  chpub  25397  dchrabs  25437  bcmono  25454  bcmax  25455  bcp1ctr  25456  bclbnd  25457  bposlem5  25465  gausslemma2dlem0h  25540  gausslemma2dlem4  25546  gausslemma2dlem6  25549  lgseisenlem1  25552  2lgsoddprmlem2  25586  2sqlem7  25601  2sqlem8  25603  chebbnd1lem1  25610  chtppilimlem1  25614  dchrisum0re  25654  mulogsumlem  25672  selberg2lem  25691  pntrlog2bndlem4  25721  pntlemr  25743  pntlemj  25744  pnt  25755  ostth2lem3  25776  vtxdgfival  26817  vtxdfiun  26830  vtxdginducedm1fi  26892  crctcsh  27173  wwlksnred  27252  wwlksnredOLD  27253  wwlksnextproplem2  27285  wwlksnextproplem2OLD  27286  rusgrnumwwlks  27354  rusgrnumwwlksOLD  27355  eupth2lems  27642  eucrct2eupthOLD  27650  eucrct2eupth  27651  numclwlk1lem1  27797  numclwwlk5  27820  numclwwlk6  27822  friendshipgt3  27830  nnmulge  30080  nndiffz1  30112  2sqmod  30210  nexple  30669  oddpwdc  31014  eulerpartlems  31020  eulerpartlemgc  31022  eulerpartlemb  31028  coinfliplem  31139  signsplypnf  31227  signslema  31239  signstfvc  31252  signstfveq0  31255  signstfveq0OLD  31256  fsum2dsub  31287  reprlt  31299  reprgt  31301  reprinfz1  31302  breprexplemc  31312  erdszelem8  31779  erdsze2lem2  31785  cvmliftlem7  31872  snmlff  31910  bcprod  32218  poimirlem3  34022  poimirlem4  34023  poimirlem6  34025  poimirlem7  34026  poimirlem10  34029  poimirlem11  34030  poimirlem12  34031  poimirlem13  34032  poimirlem15  34034  poimirlem16  34035  poimirlem17  34036  poimirlem19  34038  poimirlem20  34039  poimirlem21  34040  poimirlem22  34041  poimirlem23  34042  poimirlem24  34043  poimirlem25  34044  poimirlem26  34045  poimirlem29  34048  poimirlem30  34049  poimirlem31  34050  rrnequiv  34242  eldioph2lem1  38265  pell1qrge1  38376  rmxypos  38455  ltrmynn0  38456  ltrmxnn0  38457  lermxnn0  38458  jm2.24nn  38467  jm2.24  38471  jm2.19  38501  jm2.26lem3  38509  jm2.27c  38515  hbt  38641  dgraa0p  38660  binomcxplemnn0  39486  fsumnncl  40693  mccllem  40719  ioodvbdlimc1lem2  41057  ioodvbdlimc2lem  41059  dvnxpaek  41067  dvnmul  41068  dvnprodlem2  41072  stoweidlem17  41143  stoweidlem24  41150  wallispilem5  41195  stirlinglem15  41214  fourierdlem48  41280  fourierdlem83  41315  fourierdlem103  41335  fourierdlem104  41336  sqwvfoura  41354  elaa2lem  41359  etransclem10  41370  etransclem19  41379  etransclem20  41380  etransclem21  41381  etransclem22  41382  etransclem23  41383  etransclem24  41384  etransclem27  41387  etransclem32  41392  etransclem35  41395  etransclem44  41404  etransclem45  41405  etransclem46  41406  etransclem47  41407  etransclem48  41408  etransc  41409  rrndistlt  41416  fmtnoge3  42445  sqrtpwpw2p  42453  fmtnosqrt  42454  flsqrt  42511  lighneallem4a  42528  ssnn0ssfz  43124  pgrple2abl  43143  nn0eo  43319  fllog2  43359  aacllem  43635