Theorem nn0red 12511

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℕ₀cn0 12449

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-n0 12450

This theorem is referenced by:  nn0cnd  12512  nn0readdcl  12516  eluzmn  12807  flmulnn0  13796  quoremz  13824  quoremnn0ALT  13826  modaddmodup  13906  modaddmodlo  13907  expneg  14041  expnbnd  14204  facdiv  14259  faclbnd6  14271  hashdom  14351  hashun2  14355  hashunx  14358  hashfun  14409  hashf1  14429  seqcoll2  14437  hashge2el2dif  14452  hashtpg  14457  wrdlenge2n0  14524  ccatsymb  14554  ccatrn  14561  ccatalpha  14565  ccat2s1fvw  14610  swrdnd  14626  swrdnd0  14629  pfxnd0  14660  pfxsuffeqwrdeq  14670  swrdccat3blem  14711  cshwidxmod  14775  repswcshw  14784  swrds2  14913  modfsummods  15766  climcnds  15824  geomulcvg  15849  mertenslem1  15857  binomfallfaclem2  16013  binomrisefac  16015  fallfacval4  16016  efcllem  16050  eftlub  16084  ruclem10  16214  oddge22np1  16326  nn0oddm1d2  16362  divalglem5  16374  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  sadcaddlem  16434  sadaddlem  16443  sadasslem  16447  sadeq  16449  smuval2  16459  smupvallem  16460  smueqlem  16467  bezoutlem3  16518  bezoutlem4  16519  gcdzeq  16529  dvdssqlem  16543  nn0seqcvgd  16547  eucalglt  16562  lcmneg  16580  mulgcddvds  16632  qredeu  16635  prmdvdsbc  16703  prmdiveq  16763  odzdvds  16773  pythagtriplem3  16796  pythagtriplem6  16799  pythagtriplem7  16800  iserodd  16813  pclem  16816  pcpremul  16821  pcidlem  16850  pcgcd1  16855  pc2dvds  16857  pcz  16859  pcprmpw2  16860  fldivp1  16875  pcfaclem  16876  pcfac  16877  pcbc  16878  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  4sqlem11  16933  4sqlem12  16934  4sqlem14  16936  vdwlem11  16969  vdwlem12  16970  ramlb  16997  0ram  16998  ram0  17000  ramub1lem2  17005  ramcl  17007  psgnunilem2  19432  odmodnn0  19477  mndodconglem  19478  mndodcong  19479  oddvds  19484  odhash3  19513  gexdvds  19521  sylow1lem1  19535  sylow1lem5  19539  pgpfi  19542  pgpssslw  19551  efgsfo  19676  efgredlemd  19681  efgredlem  19684  efgred  19685  lt6abl  19832  telgsums  19930  pgpfaclem2  20021  srgbinomlem3  20144  zringlpirlem3  21381  psrbaglesupp  21838  psrbagcon  21841  psrbagleadd1  21844  mplmonmul  21950  psdmul  22060  coe1tmmul2  22169  coe1tmmul2fv  22171  coe1pwmulfv  22173  gsummoncoe1  22202  fvmptnn04if  22743  fvmptnn04ifc  22746  fvmptnn04ifd  22747  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  lebnumii  24872  dyadmaxlem  25505  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mdegmullem  25990  coe1mul3  26011  coe1mul4  26012  deg1sublt  26022  deg1mul2  26026  deg1tmle  26030  deg1tm  26031  ply1divmo  26048  ply1divex  26049  deg1submon1p  26065  dvdsq1p  26075  fta1glem2  26081  fta1blem  26083  plyco0  26104  plyeq0lem  26122  plypf1  26124  plyaddlem1  26125  coeeulem  26136  dgrub  26146  dgrlb  26148  dgreq  26156  coeaddlem  26161  coemullem  26162  coemulhi  26166  dgrlt  26179  dgradd2  26181  dgrmul  26183  dgrcolem2  26187  dgrco  26188  plydivlem3  26210  plydivlem4  26211  plydivex  26212  plydiveu  26213  fta1lem  26222  quotcan  26224  vieta1lem2  26226  radcnvlem1  26329  dvradcnv  26337  leibpi  26859  log2tlbnd  26862  birthdaylem2  26869  birthdaylem3  26870  fsumharmonic  26929  dmlogdmgm  26941  basellem3  27000  basellem5  27002  issqf  27053  ppip1le  27078  ppiltx  27094  mumullem2  27097  sgmppw  27115  ppiub  27122  chtublem  27129  chpub  27138  dchrabs  27178  bcmono  27195  bcmax  27196  bcp1ctr  27197  bclbnd  27198  bposlem5  27206  gausslemma2dlem0h  27281  gausslemma2dlem4  27287  gausslemma2dlem6  27290  lgseisenlem1  27293  2lgsoddprmlem2  27327  2sqlem7  27342  2sqlem8  27344  2sq2  27351  2sqmod  27354  chebbnd1lem1  27387  chtppilimlem1  27391  dchrisum0re  27431  mulogsumlem  27449  selberg2lem  27468  pntrlog2bndlem4  27498  pntlemr  27520  pntlemj  27521  pnt  27532  ostth2lem3  27553  vtxdgfival  29404  vtxdfiun  29417  vtxdginducedm1fi  29479  crctcsh  29761  wwlksnred  29829  wwlksnextproplem2  29847  rusgrnumwwlks  29911  eupth2lems  30174  eucrct2eupth  30181  numclwlk1lem1  30305  numclwwlk5  30324  numclwwlk6  30326  friendshipgt3  30334  nnmulge  32669  nndiffz1  32716  fzo0opth  32735  suppssnn0  32737  ccatdmss  32878  pfxlsw2ccat  32879  wrdt2ind  32882  gsumwrd2dccatlem  33013  cycpmrn  33107  cyc3conja  33121  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  ply1unit  33551  ply1dg3rt0irred  33558  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  exsslsb  33599  ply1degltdimlem  33625  ply1degltdim  33626  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  minplyirredlem  33707  irredminply  33713  nn0constr  33758  iconstr  33763  cos9thpiminplylem1  33779  oddpwdc  34352  eulerpartlems  34358  eulerpartlemgc  34360  eulerpartlemb  34366  coinfliplem  34477  signsplypnf  34548  signslema  34560  signstfvc  34572  signstfveq0  34575  fsum2dsub  34605  reprlt  34617  reprgt  34619  reprinfz1  34620  breprexplemc  34630  lpadmax  34680  lpadright  34682  usgrgt2cycl  35124  acycgr1v  35143  erdszelem8  35192  erdsze2lem2  35198  cvmliftlem7  35285  snmlff  35323  bcprod  35732  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  rrnequiv  37836  lcmineqlem17  42040  lcmineqlem21  42044  3lexlogpow5ineq5  42055  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p3  42073  aks4d1p7d1  42077  aks6d1c1  42111  aks6d1c3  42118  aks6d1c2lem4  42122  hashnexinj  42123  aks6d1c2  42125  aks6d1c5lem1  42131  aks6d1c5lem3  42132  aks6d1c5lem2  42133  aks6d1c5  42134  2np3bcnp1  42139  2ap1caineq  42140  sticksstones6  42146  sticksstones7  42147  sticksstones22  42163  aks6d1c6lem3  42167  aks6d1c6lem4  42168  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7lem2  42176  unitscyglem1  42190  unitscyglem4  42193  aks5lem8  42196  frlmvscadiccat  42501  fltnltalem  42657  eldioph2lem1  42755  pell1qrge1  42865  rmxypos  42943  ltrmynn0  42944  ltrmxnn0  42945  lermxnn0  42946  jm2.24nn  42955  jm2.24  42959  jm2.19  42989  jm2.26lem3  42997  jm2.27c  43003  hbt  43126  dgraa0p  43145  binomcxplemnn0  44345  fsumnncl  45577  mccllem  45602  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnxpaek  45947  dvnmul  45948  dvnprodlem2  45952  stoweidlem17  46022  stoweidlem24  46029  wallispilem5  46074  stirlinglem15  46093  fourierdlem48  46159  fourierdlem83  46194  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  elaa2lem  46238  etransclem10  46249  etransclem19  46258  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem23  46262  etransclem24  46263  etransclem27  46266  etransclem32  46271  etransclem35  46274  etransclem44  46283  etransclem45  46284  etransclem46  46285  etransclem47  46286  etransclem48  46287  etransc  46288  rrndistlt  46295  fmtnoge3  47535  sqrtpwpw2p  47543  fmtnosqrt  47544  flsqrt  47598  lighneallem4a  47613  ssnn0ssfz  48341  pgrple2abl  48357  nn0eo  48521  fllog2  48561  itcovalt2lem2lem1  48666  aacllem  49794