Theorem nn0red 12698

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11229  ℕ₀cn0 12636

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-i2m1 11298  ax-1ne0 11299  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-nn 12366  df-n0 12637

This theorem is used by:  nn0cnd  12699  nn0readdcl  12703  eluzmn  13002  flmulnn0  13997  quoremz  14025  quoremnn0ALT  14027  modaddmodup  14107  modaddmodlo  14108  expneg  14242  expnbnd  14406  facdiv  14461  faclbnd6  14473  hashdom  14553  hashun2  14557  hashunx  14560  hashfun  14612  hashf1  14632  seqcoll2  14640  hashge2el2dif  14655  hashtpg  14660  wrdlenge2n0  14727  ccatdmss  14757  ccatsymb  14758  ccatrn  14765  ccatalpha  14770  ccat2s1fvw  14817  swrdnd  14835  swrdnd0  14838  pfxnd0  14869  pfxsuffeqwrdeq  14878  swrdccat3blem  14919  cshwidxmod  14985  repswcshw  14994  swrds2  15123  modfsummods  15992  climcnds  16052  geomulcvg  16077  mertenslem1  16085  binomfallfaclem2  16238  binomrisefac  16240  fallfacval4  16241  efcllem  16275  eftlub  16309  ruclem10  16439  oddge22np1  16551  nn0oddm1d2  16587  divalglem5  16599  bitsfzolem  16636  bitsfzo  16637  bitsmod  16638  sadcaddlem  16659  sadaddlem  16668  sadasslem  16672  sadeq  16674  smuval2  16684  smupvallem  16685  smueqlem  16692  bezoutlem3  16746  bezoutlem4  16747  gcdzeq  16757  nn0seqcvgd  16777  eucalglt  16792  lcmneg  16810  mulgcddvds  16862  qredeu  16865  prmdvdsbc  16934  prmdiveq  16995  odzdvds  17005  pythagtriplem3  17028  pythagtriplem6  17031  pythagtriplem7  17032  iserodd  17045  pclem  17048  pcpremul  17053  pcidlem  17082  pcgcd1  17087  pc2dvds  17089  pcz  17091  pcprmpw2  17092  fldivp1  17107  pcfaclem  17108  pcfac  17109  pcbc  17110  prmreclem2  17127  prmreclem3  17128  prmreclem4  17129  prmreclem5  17130  4sqlem11  17165  4sqlem12  17166  4sqlem14  17168  vdwlem11  17201  vdwlem12  17202  ramlb  17229  0ram  17230  ram0  17232  ramub1lem2  17237  ramcl  17239  psgnunilem2  19742  odmodnn0  19787  mndodconglem  19788  mndodcong  19789  oddvds  19794  odhash3  19823  gexdvds  19831  sylow1lem1  19845  sylow1lem5  19849  pgpfi  19852  pgpssslw  19861  efgsfo  19986  efgredlemd  19991  efgredlem  19994  efgred  19995  lt6abl  20142  telgsums  20240  pgpfaclem2  20331  srgbinomlem3  20487  zringlpirlem3  21803  psrbaglesupp  22263  psrbagcon  22266  psrbagleadd1  22269  mplmonmul  22378  psdmul  22520  coe1tmmul2  22628  coe1tmmul2fv  22630  coe1pwmulfv  22632  gsummoncoe1  22659  fvmptnn04if  23200  fvmptnn04ifc  23203  fvmptnn04ifd  23204  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  lebnumii  25320  dyadmaxlem  25951  mbfi1fseqlem3  26071  mbfi1fseqlem4  26072  mbfi1fseqlem5  26073  mdegmullem  26429  coe1mul3  26450  coe1mul4  26451  deg1sublt  26461  deg1mul2  26465  deg1tmle  26469  deg1tm  26470  ply1divmo  26487  ply1divex  26488  deg1submon1p  26504  dvdsq1p  26514  fta1glem2  26520  fta1blem  26522  plyco0  26543  plyeq0lem  26562  plypf1  26564  plyaddlem1  26565  coeeulem  26576  dgrub  26586  dgrlb  26588  dgreq  26596  coeaddlem  26601  coemullem  26602  coemulhi  26606  dgrlt  26618  dgradd2  26620  dgrmul  26622  dgrcolem2  26626  dgrco  26627  plydivlem3  26649  plydivlem4  26650  plydivex  26651  plydiveu  26652  fta1lem  26661  quotcan  26665  vieta1lem2  26667  radcnvlem1  26773  dvradcnv  26781  leibpi  27303  log2tlbnd  27306  birthdaylem2  27313  birthdaylem3  27314  fsumharmonic  27372  dmlogdmgm  27384  basellem3  27443  basellem5  27445  issqf  27496  ppip1le  27521  ppiltx  27537  mumullem2  27540  sgmppw  27557  ppiub  27564  chtublem  27571  chpub  27580  dchrabs  27620  bcmono  27637  bcmax  27638  bcp1ctr  27639  bclbnd  27640  bposlem5  27648  gausslemma2dlem0h  27723  gausslemma2dlem4  27729  gausslemma2dlem6  27732  lgseisenlem1  27735  2lgsoddprmlem2  27769  2sqlem7  27784  2sqlem8  27786  2sq2  27793  2sqmod  27796  chebbnd1lem1  27829  chtppilimlem1  27833  dchrisum0re  27873  mulogsumlem  27891  selberg2lem  27910  pntrlog2bndlem4  27940  pntlemr  27962  pntlemj  27963  pnt  27974  ostth2lem3  27995  vtxdgfival  30083  vtxdfiun  30096  vtxdginducedm1fi  30158  crctcsh  30446  wwlksnred  30514  wwlksnextproplem2  30532  rusgrnumwwlks  30599  eupth2lems  30872  eucrct2eupth  30879  numclwlk1lem1  31003  numclwwlk5  31022  numclwwlk6  31024  friendshipgt3  31032  nnmulge  33404  nndiffz1  33451  fzo0opth  33468  suppssnn0  33470  pfxlsw2ccat  33586  wrdt2ind  33589  gsumwrd2dccatlem  33714  cycpmrn  33780  cyc3conja  33794  1arithidomlem1  34151  1arithidomlem2  34152  1arithidom  34153  ply1unit  34190  ply1dg3rt0irred  34199  ply1degltel  34209  ply1degleel  34210  ply1degltlss  34211  psrmonmul  34265  esplyfval2  34280  esplyfval3  34287  exsslsb  34312  ply1degltdimlem  34337  ply1degltdim  34338  fldextrspundgdvdslem  34395  fldextrspundgdvds  34396  extdgfialglem1  34407  minplyirredlem  34425  irredminply  34431  nn0constr  34476  iconstr  34481  cos9thpiminplylem1  34497  oddpwdc  35069  eulerpartlems  35075  eulerpartlemgc  35077  eulerpartlemb  35083  coinfliplem  35194  signsplypnf  35262  signslema  35274  signstfvc  35286  signstfveq0  35289  fsum2dsub  35319  reprlt  35331  reprgt  35333  reprinfz1  35334  breprexplemc  35344  lpadmax  35397  lpadright  35399  usgrgt2cycl  36079  acycgr1v  36084  erdszelem8  36143  erdsze2lem2  36149  cvmliftlem7  36236  snmlff  36274  bcprod  36694  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem10  38753  poimirlem11  38754  poimirlem12  38755  poimirlem13  38756  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem25  38768  poimirlem26  38769  poimirlem29  38772  poimirlem30  38773  poimirlem31  38774  rrnequiv  38972  lcmineqlem17  43298  lcmineqlem21  43302  3lexlogpow5ineq5  43313  aks4d1p1p4  43324  aks4d1p1p7  43327  aks4d1p3  43331  aks4d1p7d1  43335  aks6d1c1  43369  aks6d1c3  43376  aks6d1c2lem4  43380  hashnexinj  43381  aks6d1c2  43383  aks6d1c5lem1  43389  aks6d1c5lem3  43390  aks6d1c5lem2  43391  aks6d1c5  43392  2np3bcnp1  43397  2ap1caineq  43398  sticksstones6  43404  sticksstones7  43405  sticksstones22  43421  aks6d1c6lem3  43425  aks6d1c6lem4  43426  bcled  43431  bcle2d  43432  aks6d1c7lem1  43433  aks6d1c7lem2  43434  unitscyglem1  43448  unitscyglem4  43451  aks5lem8  43454  frlmvscadiccat  43777  fltnltalem  43877  eldioph2lem1  43975  pell1qrge1  44081  rmxypos  44158  ltrmynn0  44159  ltrmxnn0  44160  lermxnn0  44161  jm2.24nn  44170  jm2.24  44174  jm2.19  44204  jm2.26lem3  44212  jm2.27c  44218  hbt  44335  dgraa0p  44354  binomcxplemnn0  45536  fsumnncl  46799  mccllem  46824  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  dvnxpaek  47167  dvnmul  47168  dvnprodlem2  47172  stoweidlem17  47242  stoweidlem24  47249  wallispilem5  47294  stirlinglem15  47313  fourierdlem48  47379  fourierdlem83  47414  fourierdlem103  47434  fourierdlem104  47435  sqwvfoura  47453  elaa2lem  47458  etransclem10  47469  etransclem19  47478  etransclem20  47479  etransclem21  47480  etransclem22  47481  etransclem23  47482  etransclem24  47483  etransclem27  47486  etransclem32  47491  etransclem35  47494  etransclem44  47503  etransclem45  47504  etransclem46  47505  etransclem47  47506  etransclem48  47507  etransc  47508  rrndistlt  47515  chnsubseqwl  48104  chnsubseq  48105  fmtnoge3  48830  sqrtpwpw2p  48838  fmtnosqrt  48839  flsqrt  48893  lighneallem4a  48908  ssnn0ssfz  49676  pgrple2abl  49692  nn0eo  49855  fllog2  49895  itcovalt2lem2lem1  50000  aacllem  51251