Theorem nn0red 12490

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-n0 12429

This theorem is referenced by:  nn0cnd  12491  nn0readdcl  12495  eluzmn  12786  flmulnn0  13777  quoremz  13805  quoremnn0ALT  13807  modaddmodup  13887  modaddmodlo  13888  expneg  14022  expnbnd  14185  facdiv  14240  faclbnd6  14252  hashdom  14332  hashun2  14336  hashunx  14339  hashfun  14390  hashf1  14410  seqcoll2  14418  hashge2el2dif  14433  hashtpg  14438  wrdlenge2n0  14505  ccatdmss  14535  ccatsymb  14536  ccatrn  14543  ccatalpha  14547  ccat2s1fvw  14592  swrdnd  14608  swrdnd0  14611  pfxnd0  14642  pfxsuffeqwrdeq  14651  swrdccat3blem  14692  cshwidxmod  14756  repswcshw  14765  swrds2  14893  modfsummods  15747  climcnds  15807  geomulcvg  15832  mertenslem1  15840  binomfallfaclem2  15996  binomrisefac  15998  fallfacval4  15999  efcllem  16033  eftlub  16067  ruclem10  16197  oddge22np1  16309  nn0oddm1d2  16345  divalglem5  16357  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  sadcaddlem  16417  sadaddlem  16426  sadasslem  16430  sadeq  16432  smuval2  16442  smupvallem  16443  smueqlem  16450  bezoutlem3  16501  bezoutlem4  16502  gcdzeq  16512  dvdssqlem  16526  nn0seqcvgd  16530  eucalglt  16545  lcmneg  16563  mulgcddvds  16615  qredeu  16618  prmdvdsbc  16687  prmdiveq  16747  odzdvds  16757  pythagtriplem3  16780  pythagtriplem6  16783  pythagtriplem7  16784  iserodd  16797  pclem  16800  pcpremul  16805  pcidlem  16834  pcgcd1  16839  pc2dvds  16841  pcz  16843  pcprmpw2  16844  fldivp1  16859  pcfaclem  16860  pcfac  16861  pcbc  16862  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  4sqlem11  16917  4sqlem12  16918  4sqlem14  16920  vdwlem11  16953  vdwlem12  16954  ramlb  16981  0ram  16982  ram0  16984  ramub1lem2  16989  ramcl  16991  psgnunilem2  19461  odmodnn0  19506  mndodconglem  19507  mndodcong  19508  oddvds  19513  odhash3  19542  gexdvds  19550  sylow1lem1  19564  sylow1lem5  19568  pgpfi  19571  pgpssslw  19580  efgsfo  19705  efgredlemd  19710  efgredlem  19713  efgred  19714  lt6abl  19861  telgsums  19959  pgpfaclem2  20050  srgbinomlem3  20200  zringlpirlem3  21454  psrbaglesupp  21912  psrbagcon  21915  psrbagleadd1  21918  mplmonmul  22024  psdmul  22142  coe1tmmul2  22251  coe1tmmul2fv  22253  coe1pwmulfv  22255  gsummoncoe1  22283  fvmptnn04if  22824  fvmptnn04ifc  22827  fvmptnn04ifd  22828  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  lebnumii  24943  dyadmaxlem  25574  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mdegmullem  26053  coe1mul3  26074  coe1mul4  26075  deg1sublt  26085  deg1mul2  26089  deg1tmle  26093  deg1tm  26094  ply1divmo  26111  ply1divex  26112  deg1submon1p  26128  dvdsq1p  26138  fta1glem2  26144  fta1blem  26146  plyco0  26167  plyeq0lem  26185  plypf1  26187  plyaddlem1  26188  coeeulem  26199  dgrub  26209  dgrlb  26211  dgreq  26219  coeaddlem  26224  coemullem  26225  coemulhi  26229  dgrlt  26241  dgradd2  26243  dgrmul  26245  dgrcolem2  26249  dgrco  26250  plydivlem3  26272  plydivlem4  26273  plydivex  26274  plydiveu  26275  fta1lem  26284  quotcan  26286  vieta1lem2  26288  radcnvlem1  26391  dvradcnv  26399  leibpi  26919  log2tlbnd  26922  birthdaylem2  26929  birthdaylem3  26930  fsumharmonic  26989  dmlogdmgm  27001  basellem3  27060  basellem5  27062  issqf  27113  ppip1le  27138  ppiltx  27154  mumullem2  27157  sgmppw  27174  ppiub  27181  chtublem  27188  chpub  27197  dchrabs  27237  bcmono  27254  bcmax  27255  bcp1ctr  27256  bclbnd  27257  bposlem5  27265  gausslemma2dlem0h  27340  gausslemma2dlem4  27346  gausslemma2dlem6  27349  lgseisenlem1  27352  2lgsoddprmlem2  27386  2sqlem7  27401  2sqlem8  27403  2sq2  27410  2sqmod  27413  chebbnd1lem1  27446  chtppilimlem1  27450  dchrisum0re  27490  mulogsumlem  27508  selberg2lem  27527  pntrlog2bndlem4  27557  pntlemr  27579  pntlemj  27580  pnt  27591  ostth2lem3  27612  vtxdgfival  29553  vtxdfiun  29566  vtxdginducedm1fi  29628  crctcsh  29907  wwlksnred  29975  wwlksnextproplem2  29993  rusgrnumwwlks  30060  eupth2lems  30323  eucrct2eupth  30330  numclwlk1lem1  30454  numclwwlk5  30473  numclwwlk6  30475  friendshipgt3  30483  nnmulge  32827  nndiffz1  32874  fzo0opth  32891  suppssnn0  32893  pfxlsw2ccat  33025  wrdt2ind  33028  gsumwrd2dccatlem  33153  cycpmrn  33219  cyc3conja  33233  1arithidomlem1  33610  1arithidomlem2  33611  1arithidom  33612  ply1unit  33650  ply1dg3rt0irred  33659  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  psrmonmul  33709  esplyfval2  33724  esplyfval3  33731  exsslsb  33756  ply1degltdimlem  33782  ply1degltdim  33783  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  extdgfialglem1  33852  minplyirredlem  33870  irredminply  33876  nn0constr  33921  iconstr  33926  cos9thpiminplylem1  33942  oddpwdc  34514  eulerpartlems  34520  eulerpartlemgc  34522  eulerpartlemb  34528  coinfliplem  34639  signsplypnf  34710  signslema  34722  signstfvc  34734  signstfveq0  34737  fsum2dsub  34767  reprlt  34779  reprgt  34781  reprinfz1  34782  breprexplemc  34792  lpadmax  34842  lpadright  34844  usgrgt2cycl  35328  acycgr1v  35347  erdszelem8  35396  erdsze2lem2  35402  cvmliftlem7  35489  snmlff  35527  bcprod  35936  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  rrnequiv  38170  lcmineqlem17  42498  lcmineqlem21  42502  3lexlogpow5ineq5  42513  aks4d1p1p4  42524  aks4d1p1p7  42527  aks4d1p3  42531  aks4d1p7d1  42535  aks6d1c1  42569  aks6d1c3  42576  aks6d1c2lem4  42580  hashnexinj  42581  aks6d1c2  42583  aks6d1c5lem1  42589  aks6d1c5lem3  42590  aks6d1c5lem2  42591  aks6d1c5  42592  2np3bcnp1  42597  2ap1caineq  42598  sticksstones6  42604  sticksstones7  42605  sticksstones22  42621  aks6d1c6lem3  42625  aks6d1c6lem4  42626  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  unitscyglem1  42648  unitscyglem4  42651  aks5lem8  42654  frlmvscadiccat  42965  fltnltalem  43109  eldioph2lem1  43206  pell1qrge1  43316  rmxypos  43393  ltrmynn0  43394  ltrmxnn0  43395  lermxnn0  43396  jm2.24nn  43405  jm2.24  43409  jm2.19  43439  jm2.26lem3  43447  jm2.27c  43453  hbt  43576  dgraa0p  43595  binomcxplemnn0  44794  fsumnncl  46020  mccllem  46045  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnxpaek  46388  dvnmul  46389  dvnprodlem2  46393  stoweidlem17  46463  stoweidlem24  46470  wallispilem5  46515  stirlinglem15  46534  fourierdlem48  46600  fourierdlem83  46635  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  elaa2lem  46679  etransclem10  46690  etransclem19  46699  etransclem20  46700  etransclem21  46701  etransclem22  46702  etransclem23  46703  etransclem24  46704  etransclem27  46707  etransclem32  46712  etransclem35  46715  etransclem44  46724  etransclem45  46725  etransclem46  46726  etransclem47  46727  etransclem48  46728  etransc  46729  rrndistlt  46736  chnsubseqwl  47325  chnsubseq  47326  fmtnoge3  48005  sqrtpwpw2p  48013  fmtnosqrt  48014  flsqrt  48068  lighneallem4a  48083  ssnn0ssfz  48837  pgrple2abl  48853  nn0eo  49016  fllog2  49056  itcovalt2lem2lem1  49161  aacllem  50288