Theorem nn0red 12563

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11128  ℕ₀cn0 12501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-i2m1 11197  ax-1ne0 11198  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12241  df-n0 12502

This theorem is referenced by:  nn0cnd  12564  nn0readdcl  12568  eluzmn  12859  flmulnn0  13844  quoremz  13872  quoremnn0ALT  13874  modaddmodup  13952  modaddmodlo  13953  expneg  14087  expnbnd  14250  facdiv  14305  faclbnd6  14317  hashdom  14397  hashun2  14401  hashunx  14404  hashfun  14455  hashf1  14475  seqcoll2  14483  hashge2el2dif  14498  hashtpg  14503  wrdlenge2n0  14570  ccatsymb  14600  ccatrn  14607  ccatalpha  14611  ccat2s1fvw  14656  swrdnd  14672  swrdnd0  14675  pfxnd0  14706  pfxsuffeqwrdeq  14716  swrdccat3blem  14757  cshwidxmod  14821  repswcshw  14830  swrds2  14959  modfsummods  15809  climcnds  15867  geomulcvg  15892  mertenslem1  15900  binomfallfaclem2  16056  binomrisefac  16058  fallfacval4  16059  efcllem  16093  eftlub  16127  ruclem10  16257  oddge22np1  16368  nn0oddm1d2  16404  divalglem5  16416  bitsfzolem  16453  bitsfzo  16454  bitsmod  16455  sadcaddlem  16476  sadaddlem  16485  sadasslem  16489  sadeq  16491  smuval2  16501  smupvallem  16502  smueqlem  16509  bezoutlem3  16560  bezoutlem4  16561  gcdzeq  16571  dvdssqlem  16585  nn0seqcvgd  16589  eucalglt  16604  lcmneg  16622  mulgcddvds  16674  qredeu  16677  prmdvdsbc  16745  prmdiveq  16805  odzdvds  16815  pythagtriplem3  16838  pythagtriplem6  16841  pythagtriplem7  16842  iserodd  16855  pclem  16858  pcpremul  16863  pcidlem  16892  pcgcd1  16897  pc2dvds  16899  pcz  16901  pcprmpw2  16902  fldivp1  16917  pcfaclem  16918  pcfac  16919  pcbc  16920  prmreclem2  16937  prmreclem3  16938  prmreclem4  16939  prmreclem5  16940  4sqlem11  16975  4sqlem12  16976  4sqlem14  16978  vdwlem11  17011  vdwlem12  17012  ramlb  17039  0ram  17040  ram0  17042  ramub1lem2  17047  ramcl  17049  psgnunilem2  19476  odmodnn0  19521  mndodconglem  19522  mndodcong  19523  oddvds  19528  odhash3  19557  gexdvds  19565  sylow1lem1  19579  sylow1lem5  19583  pgpfi  19586  pgpssslw  19595  efgsfo  19720  efgredlemd  19725  efgredlem  19728  efgred  19729  lt6abl  19876  telgsums  19974  pgpfaclem2  20065  srgbinomlem3  20188  zringlpirlem3  21425  psrbaglesupp  21882  psrbagcon  21885  psrbagleadd1  21888  mplmonmul  21994  psdmul  22104  coe1tmmul2  22213  coe1tmmul2fv  22215  coe1pwmulfv  22217  gsummoncoe1  22246  fvmptnn04if  22787  fvmptnn04ifc  22790  fvmptnn04ifd  22791  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  lebnumii  24916  dyadmaxlem  25550  mbfi1fseqlem3  25670  mbfi1fseqlem4  25671  mbfi1fseqlem5  25672  mdegmullem  26035  coe1mul3  26056  coe1mul4  26057  deg1sublt  26067  deg1mul2  26071  deg1tmle  26075  deg1tm  26076  ply1divmo  26093  ply1divex  26094  deg1submon1p  26110  dvdsq1p  26120  fta1glem2  26126  fta1blem  26128  plyco0  26149  plyeq0lem  26167  plypf1  26169  plyaddlem1  26170  coeeulem  26181  dgrub  26191  dgrlb  26193  dgreq  26201  coeaddlem  26206  coemullem  26207  coemulhi  26211  dgrlt  26224  dgradd2  26226  dgrmul  26228  dgrcolem2  26232  dgrco  26233  plydivlem3  26255  plydivlem4  26256  plydivex  26257  plydiveu  26258  fta1lem  26267  quotcan  26269  vieta1lem2  26271  radcnvlem1  26374  dvradcnv  26382  leibpi  26904  log2tlbnd  26907  birthdaylem2  26914  birthdaylem3  26915  fsumharmonic  26974  dmlogdmgm  26986  basellem3  27045  basellem5  27047  issqf  27098  ppip1le  27123  ppiltx  27139  mumullem2  27142  sgmppw  27160  ppiub  27167  chtublem  27174  chpub  27183  dchrabs  27223  bcmono  27240  bcmax  27241  bcp1ctr  27242  bclbnd  27243  bposlem5  27251  gausslemma2dlem0h  27326  gausslemma2dlem4  27332  gausslemma2dlem6  27335  lgseisenlem1  27338  2lgsoddprmlem2  27372  2sqlem7  27387  2sqlem8  27389  2sq2  27396  2sqmod  27399  chebbnd1lem1  27432  chtppilimlem1  27436  dchrisum0re  27476  mulogsumlem  27494  selberg2lem  27513  pntrlog2bndlem4  27543  pntlemr  27565  pntlemj  27566  pnt  27577  ostth2lem3  27598  vtxdgfival  29449  vtxdfiun  29462  vtxdginducedm1fi  29524  crctcsh  29806  wwlksnred  29874  wwlksnextproplem2  29892  rusgrnumwwlks  29956  eupth2lems  30219  eucrct2eupth  30226  numclwlk1lem1  30350  numclwwlk5  30369  numclwwlk6  30371  friendshipgt3  30379  nnmulge  32716  nndiffz1  32763  fzo0opth  32782  suppssnn0  32784  ccatdmss  32925  pfxlsw2ccat  32926  wrdt2ind  32929  gsumwrd2dccatlem  33060  cycpmrn  33154  cyc3conja  33168  1arithidomlem1  33550  1arithidomlem2  33551  1arithidom  33552  ply1unit  33588  ply1dg3rt0irred  33595  ply1degltel  33604  ply1degleel  33605  ply1degltlss  33606  exsslsb  33636  ply1degltdimlem  33662  ply1degltdim  33663  fldextrspundgdvdslem  33721  fldextrspundgdvds  33722  minplyirredlem  33744  irredminply  33750  nn0constr  33795  iconstr  33800  cos9thpiminplylem1  33816  oddpwdc  34386  eulerpartlems  34392  eulerpartlemgc  34394  eulerpartlemb  34400  coinfliplem  34511  signsplypnf  34582  signslema  34594  signstfvc  34606  signstfveq0  34609  fsum2dsub  34639  reprlt  34651  reprgt  34653  reprinfz1  34654  breprexplemc  34664  lpadmax  34714  lpadright  34716  usgrgt2cycl  35152  acycgr1v  35171  erdszelem8  35220  erdsze2lem2  35226  cvmliftlem7  35313  snmlff  35351  bcprod  35755  poimirlem3  37647  poimirlem4  37648  poimirlem6  37650  poimirlem7  37651  poimirlem10  37654  poimirlem11  37655  poimirlem12  37656  poimirlem13  37657  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem23  37667  poimirlem24  37668  poimirlem25  37669  poimirlem26  37670  poimirlem29  37673  poimirlem30  37674  poimirlem31  37675  rrnequiv  37859  lcmineqlem17  42058  lcmineqlem21  42062  3lexlogpow5ineq5  42073  aks4d1p1p4  42084  aks4d1p1p7  42087  aks4d1p3  42091  aks4d1p7d1  42095  aks6d1c1  42129  aks6d1c3  42136  aks6d1c2lem4  42140  hashnexinj  42141  aks6d1c2  42143  aks6d1c5lem1  42149  aks6d1c5lem3  42150  aks6d1c5lem2  42151  aks6d1c5  42152  2np3bcnp1  42157  2ap1caineq  42158  sticksstones6  42164  sticksstones7  42165  sticksstones22  42181  aks6d1c6lem3  42185  aks6d1c6lem4  42186  bcled  42191  bcle2d  42192  aks6d1c7lem1  42193  aks6d1c7lem2  42194  unitscyglem1  42208  unitscyglem4  42211  aks5lem8  42214  frlmvscadiccat  42529  fltnltalem  42685  eldioph2lem1  42783  pell1qrge1  42893  rmxypos  42971  ltrmynn0  42972  ltrmxnn0  42973  lermxnn0  42974  jm2.24nn  42983  jm2.24  42987  jm2.19  43017  jm2.26lem3  43025  jm2.27c  43031  hbt  43154  dgraa0p  43173  binomcxplemnn0  44373  fsumnncl  45601  mccllem  45626  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  dvnxpaek  45971  dvnmul  45972  dvnprodlem2  45976  stoweidlem17  46046  stoweidlem24  46053  wallispilem5  46098  stirlinglem15  46117  fourierdlem48  46183  fourierdlem83  46218  fourierdlem103  46238  fourierdlem104  46239  sqwvfoura  46257  elaa2lem  46262  etransclem10  46273  etransclem19  46282  etransclem20  46283  etransclem21  46284  etransclem22  46285  etransclem23  46286  etransclem24  46287  etransclem27  46290  etransclem32  46295  etransclem35  46298  etransclem44  46307  etransclem45  46308  etransclem46  46309  etransclem47  46310  etransclem48  46311  etransc  46312  rrndistlt  46319  fmtnoge3  47544  sqrtpwpw2p  47552  fmtnosqrt  47553  flsqrt  47607  lighneallem4a  47622  ssnn0ssfz  48324  pgrple2abl  48340  nn0eo  48508  fllog2  48548  itcovalt2lem2lem1  48653  aacllem  49665