Theorem nn0red 12533

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-nn 12213  df-n0 12473

This theorem is referenced by:  nn0cnd  12534  nn0readdcl  12538  eluzmn  12829  flmulnn0  13792  quoremz  13820  quoremnn0ALT  13822  modaddmodup  13899  modaddmodlo  13900  expneg  14035  expnbnd  14195  facdiv  14247  faclbnd6  14259  hashdom  14339  hashun2  14343  hashunx  14346  hashfun  14397  hashf1  14418  seqcoll2  14426  hashge2el2dif  14441  hashtpg  14446  wrdlenge2n0  14502  ccatsymb  14532  ccatrn  14539  ccatalpha  14543  ccat2s1fvw  14588  swrdnd  14604  swrdnd0  14607  pfxnd0  14638  pfxsuffeqwrdeq  14648  swrdccat3blem  14689  cshwidxmod  14753  repswcshw  14762  swrds2  14891  modfsummods  15739  climcnds  15797  geomulcvg  15822  mertenslem1  15830  binomfallfaclem2  15984  binomrisefac  15986  fallfacval4  15987  efcllem  16021  eftlub  16052  ruclem10  16182  oddge22np1  16292  nn0oddm1d2  16328  divalglem5  16340  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  sadcaddlem  16398  sadaddlem  16407  sadasslem  16411  sadeq  16413  smuval2  16423  smupvallem  16424  smueqlem  16431  bezoutlem3  16483  bezoutlem4  16484  gcdzeq  16494  dvdssqlem  16503  nn0seqcvgd  16507  eucalglt  16522  lcmneg  16540  mulgcddvds  16592  qredeu  16595  prmdiveq  16719  odzdvds  16728  pythagtriplem3  16751  pythagtriplem6  16754  pythagtriplem7  16755  iserodd  16768  pclem  16771  pcpremul  16776  pcidlem  16805  pcgcd1  16810  pc2dvds  16812  pcz  16814  pcprmpw2  16815  fldivp1  16830  pcfaclem  16831  pcfac  16832  pcbc  16833  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  4sqlem11  16888  4sqlem12  16889  4sqlem14  16891  vdwlem11  16924  vdwlem12  16925  ramlb  16952  0ram  16953  ram0  16955  ramub1lem2  16960  ramcl  16962  psgnunilem2  19363  odmodnn0  19408  mndodconglem  19409  mndodcong  19410  oddvds  19415  odhash3  19444  gexdvds  19452  sylow1lem1  19466  sylow1lem5  19470  pgpfi  19473  pgpssslw  19482  efgsfo  19607  efgredlemd  19612  efgredlem  19615  efgred  19616  lt6abl  19763  telgsums  19861  pgpfaclem2  19952  srgbinomlem3  20051  zringlpirlem3  21034  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrbagcon  21483  mplmonmul  21591  coe1tmmul2  21798  coe1tmmul2fv  21800  coe1pwmulfv  21802  gsummoncoe1  21828  fvmptnn04if  22351  fvmptnn04ifc  22354  fvmptnn04ifd  22355  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  lebnumii  24482  dyadmaxlem  25114  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mdegmullem  25596  coe1mul3  25617  coe1mul4  25618  deg1sublt  25628  deg1mul2  25632  deg1tmle  25635  deg1tm  25636  ply1divmo  25653  ply1divex  25654  deg1submon1p  25670  dvdsq1p  25678  fta1glem2  25684  fta1blem  25686  plyco0  25706  plyeq0lem  25724  plypf1  25726  plyaddlem1  25727  coeeulem  25738  dgrub  25748  dgrlb  25750  dgreq  25758  coeaddlem  25763  coemullem  25764  coemulhi  25768  dgrlt  25780  dgradd2  25782  dgrmul  25784  dgrcolem2  25788  dgrco  25789  plydivlem3  25808  plydivlem4  25809  plydivex  25810  plydiveu  25811  fta1lem  25820  quotcan  25822  vieta1lem2  25824  radcnvlem1  25925  dvradcnv  25933  leibpi  26447  log2tlbnd  26450  birthdaylem2  26457  birthdaylem3  26458  fsumharmonic  26516  dmlogdmgm  26528  basellem3  26587  basellem5  26589  issqf  26640  ppip1le  26665  ppiltx  26681  mumullem2  26684  sgmppw  26700  ppiub  26707  chtublem  26714  chpub  26723  dchrabs  26763  bcmono  26780  bcmax  26781  bcp1ctr  26782  bclbnd  26783  bposlem5  26791  gausslemma2dlem0h  26866  gausslemma2dlem4  26872  gausslemma2dlem6  26875  lgseisenlem1  26878  2lgsoddprmlem2  26912  2sqlem7  26927  2sqlem8  26929  2sq2  26936  2sqmod  26939  chebbnd1lem1  26972  chtppilimlem1  26976  dchrisum0re  27016  mulogsumlem  27034  selberg2lem  27053  pntrlog2bndlem4  27083  pntlemr  27105  pntlemj  27106  pnt  27117  ostth2lem3  27138  vtxdgfival  28757  vtxdfiun  28770  vtxdginducedm1fi  28832  crctcsh  29109  wwlksnred  29177  wwlksnextproplem2  29195  rusgrnumwwlks  29259  eupth2lems  29522  eucrct2eupth  29529  numclwlk1lem1  29653  numclwwlk5  29672  numclwwlk6  29674  friendshipgt3  29682  nnmulge  31994  nndiffz1  32028  suppssnn0  32048  prmdvdsbc  32053  pfxlsw2ccat  32147  wrdt2ind  32148  cycpmrn  32333  cyc3conja  32347  ply1degltel  32697  ply1degltlss  32698  ply1degltdimlem  32738  ply1degltdim  32739  minplyirredlem  32800  nexple  33038  oddpwdc  33384  eulerpartlems  33390  eulerpartlemgc  33392  eulerpartlemb  33398  coinfliplem  33508  signsplypnf  33592  signslema  33604  signstfvc  33616  signstfveq0  33619  fsum2dsub  33650  reprlt  33662  reprgt  33664  reprinfz1  33665  breprexplemc  33675  lpadmax  33725  lpadright  33727  usgrgt2cycl  34152  acycgr1v  34171  erdszelem8  34220  erdsze2lem2  34226  cvmliftlem7  34313  snmlff  34351  bcprod  34739  poimirlem3  36539  poimirlem4  36540  poimirlem6  36542  poimirlem7  36543  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem13  36549  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem23  36559  poimirlem24  36560  poimirlem25  36561  poimirlem26  36562  poimirlem29  36565  poimirlem30  36566  poimirlem31  36567  rrnequiv  36751  lcmineqlem17  40958  lcmineqlem21  40962  3lexlogpow5ineq5  40973  aks4d1p1p4  40984  aks4d1p1p7  40987  aks4d1p3  40991  aks4d1p7d1  40995  2np3bcnp1  41008  2ap1caineq  41009  sticksstones6  41015  sticksstones7  41016  sticksstones22  41032  frlmvscadiccat  41128  fltnltalem  41452  eldioph2lem1  41546  pell1qrge1  41656  rmxypos  41734  ltrmynn0  41735  ltrmxnn0  41736  lermxnn0  41737  jm2.24nn  41746  jm2.24  41750  jm2.19  41780  jm2.26lem3  41788  jm2.27c  41794  hbt  41920  dgraa0p  41939  binomcxplemnn0  43156  fsumnncl  44336  mccllem  44361  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvnxpaek  44706  dvnmul  44707  dvnprodlem2  44711  stoweidlem17  44781  stoweidlem24  44788  wallispilem5  44833  stirlinglem15  44852  fourierdlem48  44918  fourierdlem83  44953  fourierdlem103  44973  fourierdlem104  44974  sqwvfoura  44992  elaa2lem  44997  etransclem10  45008  etransclem19  45017  etransclem20  45018  etransclem21  45019  etransclem22  45020  etransclem23  45021  etransclem24  45022  etransclem27  45025  etransclem32  45030  etransclem35  45033  etransclem44  45042  etransclem45  45043  etransclem46  45044  etransclem47  45045  etransclem48  45046  etransc  45047  rrndistlt  45054  fmtnoge3  46246  sqrtpwpw2p  46254  fmtnosqrt  46255  flsqrt  46309  lighneallem4a  46324  ssnn0ssfz  47073  pgrple2abl  47089  nn0eo  47262  fllog2  47302  itcovalt2lem2lem1  47407  aacllem  47896