Theorem nn0red 12452

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11014  ℕ₀cn0 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7676  ax-1cn 11073  ax-icn 11074  ax-addcl 11075  ax-addrcl 11076  ax-mulcl 11077  ax-mulrcl 11078  ax-i2m1 11083  ax-1ne0 11084  ax-rnegex 11086  ax-rrecex 11087  ax-cnre 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7357  df-om 7805  df-2nd 7930  df-frecs 8219  df-wrecs 8250  df-recs 8299  df-rdg 8337  df-nn 12135  df-n0 12391

This theorem is referenced by:  nn0cnd  12453  nn0readdcl  12457  eluzmn  12747  flmulnn0  13735  quoremz  13763  quoremnn0ALT  13765  modaddmodup  13845  modaddmodlo  13846  expneg  13980  expnbnd  14143  facdiv  14198  faclbnd6  14210  hashdom  14290  hashun2  14294  hashunx  14297  hashfun  14348  hashf1  14368  seqcoll2  14376  hashge2el2dif  14391  hashtpg  14396  wrdlenge2n0  14463  ccatdmss  14493  ccatsymb  14494  ccatrn  14501  ccatalpha  14505  ccat2s1fvw  14550  swrdnd  14566  swrdnd0  14569  pfxnd0  14600  pfxsuffeqwrdeq  14609  swrdccat3blem  14650  cshwidxmod  14714  repswcshw  14723  swrds2  14851  modfsummods  15704  climcnds  15762  geomulcvg  15787  mertenslem1  15795  binomfallfaclem2  15951  binomrisefac  15953  fallfacval4  15954  efcllem  15988  eftlub  16022  ruclem10  16152  oddge22np1  16264  nn0oddm1d2  16300  divalglem5  16312  bitsfzolem  16349  bitsfzo  16350  bitsmod  16351  sadcaddlem  16372  sadaddlem  16381  sadasslem  16385  sadeq  16387  smuval2  16397  smupvallem  16398  smueqlem  16405  bezoutlem3  16456  bezoutlem4  16457  gcdzeq  16467  dvdssqlem  16481  nn0seqcvgd  16485  eucalglt  16500  lcmneg  16518  mulgcddvds  16570  qredeu  16573  prmdvdsbc  16641  prmdiveq  16701  odzdvds  16711  pythagtriplem3  16734  pythagtriplem6  16737  pythagtriplem7  16738  iserodd  16751  pclem  16754  pcpremul  16759  pcidlem  16788  pcgcd1  16793  pc2dvds  16795  pcz  16797  pcprmpw2  16798  fldivp1  16813  pcfaclem  16814  pcfac  16815  pcbc  16816  prmreclem2  16833  prmreclem3  16834  prmreclem4  16835  prmreclem5  16836  4sqlem11  16871  4sqlem12  16872  4sqlem14  16874  vdwlem11  16907  vdwlem12  16908  ramlb  16935  0ram  16936  ram0  16938  ramub1lem2  16943  ramcl  16945  psgnunilem2  19411  odmodnn0  19456  mndodconglem  19457  mndodcong  19458  oddvds  19463  odhash3  19492  gexdvds  19500  sylow1lem1  19514  sylow1lem5  19518  pgpfi  19521  pgpssslw  19530  efgsfo  19655  efgredlemd  19660  efgredlem  19663  efgred  19664  lt6abl  19811  telgsums  19909  pgpfaclem2  20000  srgbinomlem3  20150  zringlpirlem3  21405  psrbaglesupp  21863  psrbagcon  21866  psrbagleadd1  21869  mplmonmul  21974  psdmul  22084  coe1tmmul2  22193  coe1tmmul2fv  22195  coe1pwmulfv  22197  gsummoncoe1  22226  fvmptnn04if  22767  fvmptnn04ifc  22770  fvmptnn04ifd  22771  chfacfscmulgsum  22778  chfacfpmmulgsum  22782  lebnumii  24895  dyadmaxlem  25528  mbfi1fseqlem3  25648  mbfi1fseqlem4  25649  mbfi1fseqlem5  25650  mdegmullem  26013  coe1mul3  26034  coe1mul4  26035  deg1sublt  26045  deg1mul2  26049  deg1tmle  26053  deg1tm  26054  ply1divmo  26071  ply1divex  26072  deg1submon1p  26088  dvdsq1p  26098  fta1glem2  26104  fta1blem  26106  plyco0  26127  plyeq0lem  26145  plypf1  26147  plyaddlem1  26148  coeeulem  26159  dgrub  26169  dgrlb  26171  dgreq  26179  coeaddlem  26184  coemullem  26185  coemulhi  26189  dgrlt  26202  dgradd2  26204  dgrmul  26206  dgrcolem2  26210  dgrco  26211  plydivlem3  26233  plydivlem4  26234  plydivex  26235  plydiveu  26236  fta1lem  26245  quotcan  26247  vieta1lem2  26249  radcnvlem1  26352  dvradcnv  26360  leibpi  26882  log2tlbnd  26885  birthdaylem2  26892  birthdaylem3  26893  fsumharmonic  26952  dmlogdmgm  26964  basellem3  27023  basellem5  27025  issqf  27076  ppip1le  27101  ppiltx  27117  mumullem2  27120  sgmppw  27138  ppiub  27145  chtublem  27152  chpub  27161  dchrabs  27201  bcmono  27218  bcmax  27219  bcp1ctr  27220  bclbnd  27221  bposlem5  27229  gausslemma2dlem0h  27304  gausslemma2dlem4  27310  gausslemma2dlem6  27313  lgseisenlem1  27316  2lgsoddprmlem2  27350  2sqlem7  27365  2sqlem8  27367  2sq2  27374  2sqmod  27377  chebbnd1lem1  27410  chtppilimlem1  27414  dchrisum0re  27454  mulogsumlem  27472  selberg2lem  27491  pntrlog2bndlem4  27521  pntlemr  27543  pntlemj  27544  pnt  27555  ostth2lem3  27576  vtxdgfival  29452  vtxdfiun  29465  vtxdginducedm1fi  29527  crctcsh  29806  wwlksnred  29874  wwlksnextproplem2  29892  rusgrnumwwlks  29959  eupth2lems  30222  eucrct2eupth  30229  numclwlk1lem1  30353  numclwwlk5  30372  numclwwlk6  30374  friendshipgt3  30382  nnmulge  32728  nndiffz1  32775  fzo0opth  32792  suppssnn0  32794  pfxlsw2ccat  32940  wrdt2ind  32943  gsumwrd2dccatlem  33055  cycpmrn  33121  cyc3conja  33135  1arithidomlem1  33509  1arithidomlem2  33510  1arithidom  33511  ply1unit  33547  ply1dg3rt0irred  33555  ply1degltel  33564  ply1degleel  33565  ply1degltlss  33566  esplyfval2  33607  esplyfval3  33614  exsslsb  33632  ply1degltdimlem  33658  ply1degltdim  33659  fldextrspundgdvdslem  33716  fldextrspundgdvds  33717  extdgfialglem1  33728  minplyirredlem  33746  irredminply  33752  nn0constr  33797  iconstr  33802  cos9thpiminplylem1  33818  oddpwdc  34390  eulerpartlems  34396  eulerpartlemgc  34398  eulerpartlemb  34404  coinfliplem  34515  signsplypnf  34586  signslema  34598  signstfvc  34610  signstfveq0  34613  fsum2dsub  34643  reprlt  34655  reprgt  34657  reprinfz1  34658  breprexplemc  34668  lpadmax  34718  lpadright  34720  usgrgt2cycl  35197  acycgr1v  35216  erdszelem8  35265  erdsze2lem2  35271  cvmliftlem7  35358  snmlff  35396  bcprod  35805  poimirlem3  37686  poimirlem4  37687  poimirlem6  37689  poimirlem7  37690  poimirlem10  37693  poimirlem11  37694  poimirlem12  37695  poimirlem13  37696  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem23  37706  poimirlem24  37707  poimirlem25  37708  poimirlem26  37709  poimirlem29  37712  poimirlem30  37713  poimirlem31  37714  rrnequiv  37898  lcmineqlem17  42161  lcmineqlem21  42165  3lexlogpow5ineq5  42176  aks4d1p1p4  42187  aks4d1p1p7  42190  aks4d1p3  42194  aks4d1p7d1  42198  aks6d1c1  42232  aks6d1c3  42239  aks6d1c2lem4  42243  hashnexinj  42244  aks6d1c2  42246  aks6d1c5lem1  42252  aks6d1c5lem3  42253  aks6d1c5lem2  42254  aks6d1c5  42255  2np3bcnp1  42260  2ap1caineq  42261  sticksstones6  42267  sticksstones7  42268  sticksstones22  42284  aks6d1c6lem3  42288  aks6d1c6lem4  42289  bcled  42294  bcle2d  42295  aks6d1c7lem1  42296  aks6d1c7lem2  42297  unitscyglem1  42311  unitscyglem4  42314  aks5lem8  42317  frlmvscadiccat  42627  fltnltalem  42783  eldioph2lem1  42880  pell1qrge1  42990  rmxypos  43067  ltrmynn0  43068  ltrmxnn0  43069  lermxnn0  43070  jm2.24nn  43079  jm2.24  43083  jm2.19  43113  jm2.26lem3  43121  jm2.27c  43127  hbt  43250  dgraa0p  43269  binomcxplemnn0  44469  fsumnncl  45699  mccllem  45724  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  dvnxpaek  46067  dvnmul  46068  dvnprodlem2  46072  stoweidlem17  46142  stoweidlem24  46149  wallispilem5  46194  stirlinglem15  46213  fourierdlem48  46279  fourierdlem83  46314  fourierdlem103  46334  fourierdlem104  46335  sqwvfoura  46353  elaa2lem  46358  etransclem10  46369  etransclem19  46378  etransclem20  46379  etransclem21  46380  etransclem22  46381  etransclem23  46382  etransclem24  46383  etransclem27  46386  etransclem32  46391  etransclem35  46394  etransclem44  46403  etransclem45  46404  etransclem46  46405  etransclem47  46406  etransclem48  46407  etransc  46408  rrndistlt  46415  chnsubseqwl  47004  chnsubseq  47005  fmtnoge3  47657  sqrtpwpw2p  47665  fmtnosqrt  47666  flsqrt  47720  lighneallem4a  47735  ssnn0ssfz  48476  pgrple2abl  48492  nn0eo  48656  fllog2  48696  itcovalt2lem2lem1  48801  aacllem  49929