Theorem nn0red 12588

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℕ₀cn0 12526

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-n0 12527

This theorem is referenced by:  nn0cnd  12589  nn0readdcl  12593  eluzmn  12885  flmulnn0  13867  quoremz  13895  quoremnn0ALT  13897  modaddmodup  13975  modaddmodlo  13976  expneg  14110  expnbnd  14271  facdiv  14326  faclbnd6  14338  hashdom  14418  hashun2  14422  hashunx  14425  hashfun  14476  hashf1  14496  seqcoll2  14504  hashge2el2dif  14519  hashtpg  14524  wrdlenge2n0  14590  ccatsymb  14620  ccatrn  14627  ccatalpha  14631  ccat2s1fvw  14676  swrdnd  14692  swrdnd0  14695  pfxnd0  14726  pfxsuffeqwrdeq  14736  swrdccat3blem  14777  cshwidxmod  14841  repswcshw  14850  swrds2  14979  modfsummods  15829  climcnds  15887  geomulcvg  15912  mertenslem1  15920  binomfallfaclem2  16076  binomrisefac  16078  fallfacval4  16079  efcllem  16113  eftlub  16145  ruclem10  16275  oddge22np1  16386  nn0oddm1d2  16422  divalglem5  16434  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  sadcaddlem  16494  sadaddlem  16503  sadasslem  16507  sadeq  16509  smuval2  16519  smupvallem  16520  smueqlem  16527  bezoutlem3  16578  bezoutlem4  16579  gcdzeq  16589  dvdssqlem  16603  nn0seqcvgd  16607  eucalglt  16622  lcmneg  16640  mulgcddvds  16692  qredeu  16695  prmdvdsbc  16763  prmdiveq  16823  odzdvds  16833  pythagtriplem3  16856  pythagtriplem6  16859  pythagtriplem7  16860  iserodd  16873  pclem  16876  pcpremul  16881  pcidlem  16910  pcgcd1  16915  pc2dvds  16917  pcz  16919  pcprmpw2  16920  fldivp1  16935  pcfaclem  16936  pcfac  16937  pcbc  16938  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  4sqlem11  16993  4sqlem12  16994  4sqlem14  16996  vdwlem11  17029  vdwlem12  17030  ramlb  17057  0ram  17058  ram0  17060  ramub1lem2  17065  ramcl  17067  psgnunilem2  19513  odmodnn0  19558  mndodconglem  19559  mndodcong  19560  oddvds  19565  odhash3  19594  gexdvds  19602  sylow1lem1  19616  sylow1lem5  19620  pgpfi  19623  pgpssslw  19632  efgsfo  19757  efgredlemd  19762  efgredlem  19765  efgred  19766  lt6abl  19913  telgsums  20011  pgpfaclem2  20102  srgbinomlem3  20225  zringlpirlem3  21475  psrbaglesupp  21942  psrbagcon  21945  psrbagleadd1  21948  mplmonmul  22054  psdmul  22170  coe1tmmul2  22279  coe1tmmul2fv  22281  coe1pwmulfv  22283  gsummoncoe1  22312  fvmptnn04if  22855  fvmptnn04ifc  22858  fvmptnn04ifd  22859  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  lebnumii  24998  dyadmaxlem  25632  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mdegmullem  26117  coe1mul3  26138  coe1mul4  26139  deg1sublt  26149  deg1mul2  26153  deg1tmle  26157  deg1tm  26158  ply1divmo  26175  ply1divex  26176  deg1submon1p  26192  dvdsq1p  26202  fta1glem2  26208  fta1blem  26210  plyco0  26231  plyeq0lem  26249  plypf1  26251  plyaddlem1  26252  coeeulem  26263  dgrub  26273  dgrlb  26275  dgreq  26283  coeaddlem  26288  coemullem  26289  coemulhi  26293  dgrlt  26306  dgradd2  26308  dgrmul  26310  dgrcolem2  26314  dgrco  26315  plydivlem3  26337  plydivlem4  26338  plydivex  26339  plydiveu  26340  fta1lem  26349  quotcan  26351  vieta1lem2  26353  radcnvlem1  26456  dvradcnv  26464  leibpi  26985  log2tlbnd  26988  birthdaylem2  26995  birthdaylem3  26996  fsumharmonic  27055  dmlogdmgm  27067  basellem3  27126  basellem5  27128  issqf  27179  ppip1le  27204  ppiltx  27220  mumullem2  27223  sgmppw  27241  ppiub  27248  chtublem  27255  chpub  27264  dchrabs  27304  bcmono  27321  bcmax  27322  bcp1ctr  27323  bclbnd  27324  bposlem5  27332  gausslemma2dlem0h  27407  gausslemma2dlem4  27413  gausslemma2dlem6  27416  lgseisenlem1  27419  2lgsoddprmlem2  27453  2sqlem7  27468  2sqlem8  27470  2sq2  27477  2sqmod  27480  chebbnd1lem1  27513  chtppilimlem1  27517  dchrisum0re  27557  mulogsumlem  27575  selberg2lem  27594  pntrlog2bndlem4  27624  pntlemr  27646  pntlemj  27647  pnt  27658  ostth2lem3  27679  vtxdgfival  29487  vtxdfiun  29500  vtxdginducedm1fi  29562  crctcsh  29844  wwlksnred  29912  wwlksnextproplem2  29930  rusgrnumwwlks  29994  eupth2lems  30257  eucrct2eupth  30264  numclwlk1lem1  30388  numclwwlk5  30407  numclwwlk6  30409  friendshipgt3  30417  nnmulge  32749  nndiffz1  32788  fzo0opth  32807  suppssnn0  32809  ccatdmss  32934  pfxlsw2ccat  32935  wrdt2ind  32938  gsumwrd2dccatlem  33069  cycpmrn  33163  cyc3conja  33177  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  ply1unit  33600  ply1dg3rt0irred  33607  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  exsslsb  33647  ply1degltdimlem  33673  ply1degltdim  33674  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  minplyirredlem  33753  irredminply  33757  oddpwdc  34356  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemb  34370  coinfliplem  34481  signsplypnf  34565  signslema  34577  signstfvc  34589  signstfveq0  34592  fsum2dsub  34622  reprlt  34634  reprgt  34636  reprinfz1  34637  breprexplemc  34647  lpadmax  34697  lpadright  34699  usgrgt2cycl  35135  acycgr1v  35154  erdszelem8  35203  erdsze2lem2  35209  cvmliftlem7  35296  snmlff  35334  bcprod  35738  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  rrnequiv  37842  lcmineqlem17  42046  lcmineqlem21  42050  3lexlogpow5ineq5  42061  aks4d1p1p4  42072  aks4d1p1p7  42075  aks4d1p3  42079  aks4d1p7d1  42083  aks6d1c1  42117  aks6d1c3  42124  aks6d1c2lem4  42128  hashnexinj  42129  aks6d1c2  42131  aks6d1c5lem1  42137  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks6d1c5  42140  2np3bcnp1  42145  2ap1caineq  42146  sticksstones6  42152  sticksstones7  42153  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c6lem4  42174  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  unitscyglem1  42196  unitscyglem4  42199  aks5lem8  42202  frlmvscadiccat  42516  fltnltalem  42672  eldioph2lem1  42771  pell1qrge1  42881  rmxypos  42959  ltrmynn0  42960  ltrmxnn0  42961  lermxnn0  42962  jm2.24nn  42971  jm2.24  42975  jm2.19  43005  jm2.26lem3  43013  jm2.27c  43019  hbt  43142  dgraa0p  43161  binomcxplemnn0  44368  fsumnncl  45587  mccllem  45612  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnmul  45958  dvnprodlem2  45962  stoweidlem17  46032  stoweidlem24  46039  wallispilem5  46084  stirlinglem15  46103  fourierdlem48  46169  fourierdlem83  46204  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  elaa2lem  46248  etransclem10  46259  etransclem19  46268  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem27  46276  etransclem32  46281  etransclem35  46284  etransclem44  46293  etransclem45  46294  etransclem46  46295  etransclem47  46296  etransclem48  46297  etransc  46298  rrndistlt  46305  fmtnoge3  47517  sqrtpwpw2p  47525  fmtnosqrt  47526  flsqrt  47580  lighneallem4a  47595  ssnn0ssfz  48265  pgrple2abl  48281  nn0eo  48449  fllog2  48489  itcovalt2lem2lem1  48594  aacllem  49320