Theorem nn0red 12594

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  ℕ₀cn0 12532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12262  df-n0 12533

This theorem is used by:  nn0cnd  12595  nn0readdcl  12599  eluzmn  12898  flmulnn0  13892  quoremz  13920  quoremnn0ALT  13922  modaddmodup  14002  modaddmodlo  14003  expneg  14137  expnbnd  14300  facdiv  14355  faclbnd6  14367  hashdom  14447  hashun2  14451  hashunx  14454  hashfun  14506  hashf1  14526  seqcoll2  14534  hashge2el2dif  14549  hashtpg  14554  wrdlenge2n0  14621  ccatdmss  14651  ccatsymb  14652  ccatrn  14659  ccatalpha  14664  ccat2s1fvw  14710  swrdnd  14728  swrdnd0  14731  pfxnd0  14762  pfxsuffeqwrdeq  14771  swrdccat3blem  14812  cshwidxmod  14878  repswcshw  14887  swrds2  15015  modfsummods  15884  climcnds  15944  geomulcvg  15969  mertenslem1  15977  binomfallfaclem2  16132  binomrisefac  16134  fallfacval4  16135  efcllem  16169  eftlub  16203  ruclem10  16333  oddge22np1  16445  nn0oddm1d2  16481  divalglem5  16493  bitsfzolem  16530  bitsfzo  16531  bitsmod  16532  sadcaddlem  16553  sadaddlem  16562  sadasslem  16566  sadeq  16568  smuval2  16578  smupvallem  16579  smueqlem  16586  bezoutlem3  16637  bezoutlem4  16638  gcdzeq  16648  dvdssqlem  16662  nn0seqcvgd  16666  eucalglt  16681  lcmneg  16699  mulgcddvds  16751  qredeu  16754  prmdvdsbc  16823  prmdiveq  16883  odzdvds  16893  pythagtriplem3  16916  pythagtriplem6  16919  pythagtriplem7  16920  iserodd  16933  pclem  16936  pcpremul  16941  pcidlem  16970  pcgcd1  16975  pc2dvds  16977  pcz  16979  pcprmpw2  16980  fldivp1  16995  pcfaclem  16996  pcfac  16997  pcbc  16998  prmreclem2  17015  prmreclem3  17016  prmreclem4  17017  prmreclem5  17018  4sqlem11  17053  4sqlem12  17054  4sqlem14  17056  vdwlem11  17089  vdwlem12  17090  ramlb  17117  0ram  17118  ram0  17120  ramub1lem2  17125  ramcl  17127  psgnunilem2  19628  odmodnn0  19673  mndodconglem  19674  mndodcong  19675  oddvds  19680  odhash3  19709  gexdvds  19717  sylow1lem1  19731  sylow1lem5  19735  pgpfi  19738  pgpssslw  19747  efgsfo  19872  efgredlemd  19877  efgredlem  19880  efgred  19881  lt6abl  20028  telgsums  20126  pgpfaclem2  20217  srgbinomlem3  20373  zringlpirlem3  21683  psrbaglesupp  22143  psrbagcon  22146  psrbagleadd1  22149  mplmonmul  22258  psdmul  22400  coe1tmmul2  22508  coe1tmmul2fv  22510  coe1pwmulfv  22512  gsummoncoe1  22539  fvmptnn04if  23080  fvmptnn04ifc  23083  fvmptnn04ifd  23084  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  lebnumii  25200  dyadmaxlem  25831  mbfi1fseqlem3  25951  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mdegmullem  26310  coe1mul3  26331  coe1mul4  26332  deg1sublt  26342  deg1mul2  26346  deg1tmle  26350  deg1tm  26351  ply1divmo  26368  ply1divex  26369  deg1submon1p  26385  dvdsq1p  26395  fta1glem2  26401  fta1blem  26403  plyco0  26424  plyeq0lem  26443  plypf1  26445  plyaddlem1  26446  coeeulem  26457  dgrub  26467  dgrlb  26469  dgreq  26477  coeaddlem  26482  coemullem  26483  coemulhi  26487  dgrlt  26499  dgradd2  26501  dgrmul  26503  dgrcolem2  26507  dgrco  26508  plydivlem3  26532  plydivlem4  26533  plydivex  26534  plydiveu  26535  fta1lem  26544  quotcan  26548  vieta1lem2  26550  radcnvlem1  26656  dvradcnv  26664  leibpi  27187  log2tlbnd  27190  birthdaylem2  27197  birthdaylem3  27198  fsumharmonic  27256  dmlogdmgm  27268  basellem3  27327  basellem5  27329  issqf  27380  ppip1le  27405  ppiltx  27421  mumullem2  27424  sgmppw  27441  ppiub  27448  chtublem  27455  chpub  27464  dchrabs  27504  bcmono  27521  bcmax  27522  bcp1ctr  27523  bclbnd  27524  bposlem5  27532  gausslemma2dlem0h  27607  gausslemma2dlem4  27613  gausslemma2dlem6  27616  lgseisenlem1  27619  2lgsoddprmlem2  27653  2sqlem7  27668  2sqlem8  27670  2sq2  27677  2sqmod  27680  chebbnd1lem1  27713  chtppilimlem1  27717  dchrisum0re  27757  mulogsumlem  27775  selberg2lem  27794  pntrlog2bndlem4  27824  pntlemr  27846  pntlemj  27847  pnt  27858  ostth2lem3  27879  vtxdgfival  29937  vtxdfiun  29950  vtxdginducedm1fi  30012  crctcsh  30300  wwlksnred  30368  wwlksnextproplem2  30386  rusgrnumwwlks  30453  eupth2lems  30726  eucrct2eupth  30733  numclwlk1lem1  30857  numclwwlk5  30876  numclwwlk6  30878  friendshipgt3  30886  nnmulge  33218  nndiffz1  33265  fzo0opth  33282  suppssnn0  33284  pfxlsw2ccat  33400  wrdt2ind  33403  gsumwrd2dccatlem  33525  cycpmrn  33591  cyc3conja  33605  1arithidomlem1  33953  1arithidomlem2  33954  1arithidom  33955  ply1unit  33993  ply1dg3rt0irred  34002  ply1degltel  34012  ply1degleel  34013  ply1degltlss  34014  psrmonmul  34068  esplyfval2  34083  esplyfval3  34090  exsslsb  34115  ply1degltdimlem  34140  ply1degltdim  34141  fldextrspundgdvdslem  34198  fldextrspundgdvds  34199  extdgfialglem1  34210  minplyirredlem  34228  irredminply  34234  nn0constr  34279  iconstr  34284  cos9thpiminplylem1  34300  oddpwdc  34873  eulerpartlems  34879  eulerpartlemgc  34881  eulerpartlemb  34887  coinfliplem  34998  signsplypnf  35066  signslema  35078  signstfvc  35090  signstfveq0  35093  fsum2dsub  35123  reprlt  35135  reprgt  35137  reprinfz1  35138  breprexplemc  35148  lpadmax  35201  lpadright  35203  usgrgt2cycl  35731  acycgr1v  35736  erdszelem8  35785  erdsze2lem2  35791  cvmliftlem7  35878  snmlff  35916  bcprod  36325  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem26  38403  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  rrnequiv  38593  lcmineqlem17  42919  lcmineqlem21  42923  3lexlogpow5ineq5  42934  aks4d1p1p4  42945  aks4d1p1p7  42948  aks4d1p3  42952  aks4d1p7d1  42956  aks6d1c1  42990  aks6d1c3  42997  aks6d1c2lem4  43001  hashnexinj  43002  aks6d1c2  43004  aks6d1c5lem1  43010  aks6d1c5lem3  43011  aks6d1c5lem2  43012  aks6d1c5  43013  2np3bcnp1  43018  2ap1caineq  43019  sticksstones6  43025  sticksstones7  43026  sticksstones22  43042  aks6d1c6lem3  43046  aks6d1c6lem4  43047  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7lem2  43055  unitscyglem1  43069  unitscyglem4  43072  aks5lem8  43075  frlmvscadiccat  43402  fltnltalem  43516  eldioph2lem1  43613  pell1qrge1  43719  rmxypos  43796  ltrmynn0  43797  ltrmxnn0  43798  lermxnn0  43799  jm2.24nn  43808  jm2.24  43812  jm2.19  43842  jm2.26lem3  43850  jm2.27c  43856  hbt  43979  dgraa0p  43998  binomcxplemnn0  45181  fsumnncl  46410  mccllem  46435  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnxpaek  46778  dvnmul  46779  dvnprodlem2  46783  stoweidlem17  46853  stoweidlem24  46860  wallispilem5  46905  stirlinglem15  46924  fourierdlem48  46990  fourierdlem83  47025  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  elaa2lem  47069  etransclem10  47080  etransclem19  47089  etransclem20  47090  etransclem21  47091  etransclem22  47092  etransclem23  47093  etransclem24  47094  etransclem27  47097  etransclem32  47102  etransclem35  47105  etransclem44  47114  etransclem45  47115  etransclem46  47116  etransclem47  47117  etransclem48  47118  etransc  47119  rrndistlt  47126  chnsubseqwl  47715  chnsubseq  47716  fmtnoge3  48441  sqrtpwpw2p  48449  fmtnosqrt  48450  flsqrt  48504  lighneallem4a  48519  ssnn0ssfz  49287  pgrple2abl  49303  nn0eo  49466  fllog2  49506  itcovalt2lem2lem1  49611  aacllem  50780