Theorem nn0red 12672

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11203  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-i2m1 11272  ax-1ne0 11273  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-nn 12340  df-n0 12611

This theorem is used by:  nn0cnd  12673  nn0readdcl  12677  eluzmn  12976  flmulnn0  13971  quoremz  13999  quoremnn0ALT  14001  modaddmodup  14081  modaddmodlo  14082  expneg  14216  expnbnd  14380  facdiv  14435  faclbnd6  14447  hashdom  14527  hashun2  14531  hashunx  14534  hashfun  14586  hashf1  14606  seqcoll2  14614  hashge2el2dif  14629  hashtpg  14634  wrdlenge2n0  14701  ccatdmss  14731  ccatsymb  14732  ccatrn  14739  ccatalpha  14744  ccat2s1fvw  14791  swrdnd  14809  swrdnd0  14812  pfxnd0  14843  pfxsuffeqwrdeq  14852  swrdccat3blem  14893  cshwidxmod  14959  repswcshw  14968  swrds2  15097  modfsummods  15966  climcnds  16026  geomulcvg  16051  mertenslem1  16059  binomfallfaclem2  16212  binomrisefac  16214  fallfacval4  16215  efcllem  16249  eftlub  16283  ruclem10  16413  oddge22np1  16525  nn0oddm1d2  16561  divalglem5  16573  bitsfzolem  16610  bitsfzo  16611  bitsmod  16612  sadcaddlem  16633  sadaddlem  16642  sadasslem  16646  sadeq  16648  smuval2  16658  smupvallem  16659  smueqlem  16666  bezoutlem3  16720  bezoutlem4  16721  gcdzeq  16731  nn0seqcvgd  16751  eucalglt  16766  lcmneg  16784  mulgcddvds  16836  qredeu  16839  prmdvdsbc  16908  prmdiveq  16969  odzdvds  16979  pythagtriplem3  17002  pythagtriplem6  17005  pythagtriplem7  17006  iserodd  17019  pclem  17022  pcpremul  17027  pcidlem  17056  pcgcd1  17061  pc2dvds  17063  pcz  17065  pcprmpw2  17066  fldivp1  17081  pcfaclem  17082  pcfac  17083  pcbc  17084  prmreclem2  17101  prmreclem3  17102  prmreclem4  17103  prmreclem5  17104  4sqlem11  17139  4sqlem12  17140  4sqlem14  17142  vdwlem11  17175  vdwlem12  17176  ramlb  17203  0ram  17204  ram0  17206  ramub1lem2  17211  ramcl  17213  psgnunilem2  19715  odmodnn0  19760  mndodconglem  19761  mndodcong  19762  oddvds  19767  odhash3  19796  gexdvds  19804  sylow1lem1  19818  sylow1lem5  19822  pgpfi  19825  pgpssslw  19834  efgsfo  19959  efgredlemd  19964  efgredlem  19967  efgred  19968  lt6abl  20115  telgsums  20213  pgpfaclem2  20304  srgbinomlem3  20460  zringlpirlem3  21776  psrbaglesupp  22236  psrbagcon  22239  psrbagleadd1  22242  mplmonmul  22351  psdmul  22493  coe1tmmul2  22601  coe1tmmul2fv  22603  coe1pwmulfv  22605  gsummoncoe1  22632  fvmptnn04if  23173  fvmptnn04ifc  23176  fvmptnn04ifd  23177  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  lebnumii  25293  dyadmaxlem  25924  mbfi1fseqlem3  26044  mbfi1fseqlem4  26045  mbfi1fseqlem5  26046  mdegmullem  26402  coe1mul3  26423  coe1mul4  26424  deg1sublt  26434  deg1mul2  26438  deg1tmle  26442  deg1tm  26443  ply1divmo  26460  ply1divex  26461  deg1submon1p  26477  dvdsq1p  26487  fta1glem2  26493  fta1blem  26495  plyco0  26516  plyeq0lem  26535  plypf1  26537  plyaddlem1  26538  coeeulem  26549  dgrub  26559  dgrlb  26561  dgreq  26569  coeaddlem  26574  coemullem  26575  coemulhi  26579  dgrlt  26591  dgradd2  26593  dgrmul  26595  dgrcolem2  26599  dgrco  26600  plydivlem3  26622  plydivlem4  26623  plydivex  26624  plydiveu  26625  fta1lem  26634  quotcan  26638  vieta1lem2  26640  radcnvlem1  26746  dvradcnv  26754  leibpi  27276  log2tlbnd  27279  birthdaylem2  27286  birthdaylem3  27287  fsumharmonic  27345  dmlogdmgm  27357  basellem3  27416  basellem5  27418  issqf  27469  ppip1le  27494  ppiltx  27510  mumullem2  27513  sgmppw  27530  ppiub  27537  chtublem  27544  chpub  27553  dchrabs  27593  bcmono  27610  bcmax  27611  bcp1ctr  27612  bclbnd  27613  bposlem5  27621  gausslemma2dlem0h  27696  gausslemma2dlem4  27702  gausslemma2dlem6  27705  lgseisenlem1  27708  2lgsoddprmlem2  27742  2sqlem7  27757  2sqlem8  27759  2sq2  27766  2sqmod  27769  chebbnd1lem1  27802  chtppilimlem1  27806  dchrisum0re  27846  mulogsumlem  27864  selberg2lem  27883  pntrlog2bndlem4  27913  pntlemr  27935  pntlemj  27936  pnt  27947  ostth2lem3  27968  vtxdgfival  30056  vtxdfiun  30069  vtxdginducedm1fi  30131  crctcsh  30419  wwlksnred  30487  wwlksnextproplem2  30505  rusgrnumwwlks  30572  eupth2lems  30845  eucrct2eupth  30852  numclwlk1lem1  30976  numclwwlk5  30995  numclwwlk6  30997  friendshipgt3  31005  nnmulge  33378  nndiffz1  33425  fzo0opth  33442  suppssnn0  33444  pfxlsw2ccat  33560  wrdt2ind  33563  gsumwrd2dccatlem  33685  cycpmrn  33751  cyc3conja  33765  1arithidomlem1  34114  1arithidomlem2  34115  1arithidom  34116  ply1unit  34154  ply1dg3rt0irred  34163  ply1degltel  34173  ply1degleel  34174  ply1degltlss  34175  psrmonmul  34229  esplyfval2  34244  esplyfval3  34251  exsslsb  34276  ply1degltdimlem  34301  ply1degltdim  34302  fldextrspundgdvdslem  34359  fldextrspundgdvds  34360  extdgfialglem1  34371  minplyirredlem  34389  irredminply  34395  nn0constr  34440  iconstr  34445  cos9thpiminplylem1  34461  oddpwdc  35033  eulerpartlems  35039  eulerpartlemgc  35041  eulerpartlemb  35047  coinfliplem  35158  signsplypnf  35226  signslema  35238  signstfvc  35250  signstfveq0  35253  fsum2dsub  35283  reprlt  35295  reprgt  35297  reprinfz1  35298  breprexplemc  35308  lpadmax  35361  lpadright  35363  usgrgt2cycl  35986  acycgr1v  35991  erdszelem8  36050  erdsze2lem2  36056  cvmliftlem7  36143  snmlff  36181  bcprod  36596  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem13  38645  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem26  38658  poimirlem29  38661  poimirlem30  38662  poimirlem31  38663  rrnequiv  38863  lcmineqlem17  43189  lcmineqlem21  43193  3lexlogpow5ineq5  43204  aks4d1p1p4  43215  aks4d1p1p7  43218  aks4d1p3  43222  aks4d1p7d1  43226  aks6d1c1  43260  aks6d1c3  43267  aks6d1c2lem4  43271  hashnexinj  43272  aks6d1c2  43274  aks6d1c5lem1  43280  aks6d1c5lem3  43281  aks6d1c5lem2  43282  aks6d1c5  43283  2np3bcnp1  43288  2ap1caineq  43289  sticksstones6  43295  sticksstones7  43296  sticksstones22  43312  aks6d1c6lem3  43316  aks6d1c6lem4  43317  bcled  43322  bcle2d  43323  aks6d1c7lem1  43324  aks6d1c7lem2  43325  unitscyglem1  43339  unitscyglem4  43342  aks5lem8  43345  frlmvscadiccat  43667  fltnltalem  43767  eldioph2lem1  43865  pell1qrge1  43971  rmxypos  44048  ltrmynn0  44049  ltrmxnn0  44050  lermxnn0  44051  jm2.24nn  44060  jm2.24  44064  jm2.19  44094  jm2.26lem3  44102  jm2.27c  44108  hbt  44226  dgraa0p  44245  binomcxplemnn0  45427  fsumnncl  46678  mccllem  46703  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnxpaek  47046  dvnmul  47047  dvnprodlem2  47051  stoweidlem17  47121  stoweidlem24  47128  wallispilem5  47173  stirlinglem15  47192  fourierdlem48  47258  fourierdlem83  47293  fourierdlem103  47313  fourierdlem104  47314  sqwvfoura  47332  elaa2lem  47337  etransclem10  47348  etransclem19  47357  etransclem20  47358  etransclem21  47359  etransclem22  47360  etransclem23  47361  etransclem24  47362  etransclem27  47365  etransclem32  47370  etransclem35  47373  etransclem44  47382  etransclem45  47383  etransclem46  47384  etransclem47  47385  etransclem48  47386  etransc  47387  rrndistlt  47394  chnsubseqwl  47983  chnsubseq  47984  fmtnoge3  48709  sqrtpwpw2p  48717  fmtnosqrt  48718  flsqrt  48772  lighneallem4a  48787  ssnn0ssfz  49555  pgrple2abl  49571  nn0eo  49734  fllog2  49774  itcovalt2lem2lem1  49879  aacllem  51108