Theorem nn0red 12340

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

Syntax hints:   → wi 4   ∈ wcel 2104  ℝcr 10916  ℕ₀cn0 12279

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-i2m1 10985  ax-1ne0 10986  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020  df-n0 12280

This theorem is referenced by:  nn0cnd  12341  nn0readdcl  12345  eluzmn  12635  flmulnn0  13593  quoremz  13621  quoremnn0ALT  13623  modaddmodup  13700  modaddmodlo  13701  expneg  13836  expnbnd  13993  facdiv  14047  faclbnd6  14059  hashdom  14139  hashun2  14143  hashunx  14146  hashfun  14197  hashf1  14216  seqcoll2  14224  hashge2el2dif  14239  hashtpg  14244  wrdlenge2n0  14300  ccatsymb  14332  ccatrn  14339  ccatalpha  14343  ccat2s1fvw  14394  ccat2s1fvwOLD  14395  swrdnd  14412  swrdnd0  14415  pfxnd0  14446  pfxsuffeqwrdeq  14456  swrdccat3blem  14497  cshwidxmod  14561  repswcshw  14570  swrds2  14698  modfsummods  15550  climcnds  15608  geomulcvg  15633  mertenslem1  15641  binomfallfaclem2  15795  binomrisefac  15797  fallfacval4  15798  efcllem  15832  eftlub  15863  ruclem10  15993  oddge22np1  16103  nn0oddm1d2  16139  divalglem5  16151  bitsfzolem  16186  bitsfzo  16187  bitsmod  16188  sadcaddlem  16209  sadaddlem  16218  sadasslem  16222  sadeq  16224  smuval2  16234  smupvallem  16235  smueqlem  16242  bezoutlem3  16294  bezoutlem4  16295  gcdzeq  16307  dvdssqlem  16316  nn0seqcvgd  16320  eucalglt  16335  lcmneg  16353  mulgcddvds  16405  qredeu  16408  prmdiveq  16532  odzdvds  16541  pythagtriplem3  16564  pythagtriplem6  16567  pythagtriplem7  16568  iserodd  16581  pclem  16584  pcpremul  16589  pcidlem  16618  pcgcd1  16623  pc2dvds  16625  pcz  16627  pcprmpw2  16628  fldivp1  16643  pcfaclem  16644  pcfac  16645  pcbc  16646  prmreclem2  16663  prmreclem3  16664  prmreclem4  16665  prmreclem5  16666  4sqlem11  16701  4sqlem12  16702  4sqlem14  16704  vdwlem11  16737  vdwlem12  16738  ramlb  16765  0ram  16766  ram0  16768  ramub1lem2  16773  ramcl  16775  psgnunilem2  19148  odmodnn0  19193  mndodconglem  19194  mndodcong  19195  oddvds  19200  odhash3  19226  gexdvds  19234  sylow1lem1  19248  sylow1lem5  19252  pgpfi  19255  pgpssslw  19264  efgsfo  19390  efgredlemd  19395  efgredlem  19398  efgred  19399  lt6abl  19541  telgsums  19639  pgpfaclem2  19730  srgbinomlem3  19823  zringlpirlem3  20731  psrbaglesupp  21172  psrbaglesuppOLD  21173  psrbagcon  21178  mplmonmul  21282  coe1tmmul2  21492  coe1tmmul2fv  21494  coe1pwmulfv  21496  gsummoncoe1  21520  fvmptnn04if  22043  fvmptnn04ifc  22046  fvmptnn04ifd  22047  chfacfscmulgsum  22054  chfacfpmmulgsum  22058  lebnumii  24174  dyadmaxlem  24806  mbfi1fseqlem3  24927  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  mdegmullem  25288  coe1mul3  25309  coe1mul4  25310  deg1sublt  25320  deg1mul2  25324  deg1tmle  25327  deg1tm  25328  ply1divmo  25345  ply1divex  25346  deg1submon1p  25362  dvdsq1p  25370  fta1glem2  25376  fta1blem  25378  plyco0  25398  plyeq0lem  25416  plypf1  25418  plyaddlem1  25419  coeeulem  25430  dgrub  25440  dgrlb  25442  dgreq  25450  coeaddlem  25455  coemullem  25456  coemulhi  25460  dgrlt  25472  dgradd2  25474  dgrmul  25476  dgrcolem2  25480  dgrco  25481  plydivlem3  25500  plydivlem4  25501  plydivex  25502  plydiveu  25503  fta1lem  25512  quotcan  25514  vieta1lem2  25516  radcnvlem1  25617  dvradcnv  25625  leibpi  26137  log2tlbnd  26140  birthdaylem2  26147  birthdaylem3  26148  fsumharmonic  26206  dmlogdmgm  26218  basellem3  26277  basellem5  26279  issqf  26330  ppip1le  26355  ppiltx  26371  mumullem2  26374  sgmppw  26390  ppiub  26397  chtublem  26404  chpub  26413  dchrabs  26453  bcmono  26470  bcmax  26471  bcp1ctr  26472  bclbnd  26473  bposlem5  26481  gausslemma2dlem0h  26556  gausslemma2dlem4  26562  gausslemma2dlem6  26565  lgseisenlem1  26568  2lgsoddprmlem2  26602  2sqlem7  26617  2sqlem8  26619  2sq2  26626  2sqmod  26629  chebbnd1lem1  26662  chtppilimlem1  26666  dchrisum0re  26706  mulogsumlem  26724  selberg2lem  26743  pntrlog2bndlem4  26773  pntlemr  26795  pntlemj  26796  pnt  26807  ostth2lem3  26828  vtxdgfival  27881  vtxdfiun  27894  vtxdginducedm1fi  27956  crctcsh  28234  wwlksnred  28302  wwlksnextproplem2  28320  rusgrnumwwlks  28384  eupth2lems  28647  eucrct2eupth  28654  numclwlk1lem1  28778  numclwwlk5  28797  numclwwlk6  28799  friendshipgt3  28807  nnmulge  31118  nndiffz1  31152  prmdvdsbc  31175  pfxlsw2ccat  31269  wrdt2ind  31270  cycpmrn  31455  cyc3conja  31469  nexple  32022  oddpwdc  32366  eulerpartlems  32372  eulerpartlemgc  32374  eulerpartlemb  32380  coinfliplem  32490  signsplypnf  32574  signslema  32586  signstfvc  32598  signstfveq0  32601  fsum2dsub  32632  reprlt  32644  reprgt  32646  reprinfz1  32647  breprexplemc  32657  lpadmax  32707  lpadright  32709  usgrgt2cycl  33137  acycgr1v  33156  erdszelem8  33205  erdsze2lem2  33211  cvmliftlem7  33298  snmlff  33336  bcprod  33749  poimirlem3  35824  poimirlem4  35825  poimirlem6  35827  poimirlem7  35828  poimirlem10  35831  poimirlem11  35832  poimirlem12  35833  poimirlem13  35834  poimirlem15  35836  poimirlem16  35837  poimirlem17  35838  poimirlem19  35840  poimirlem20  35841  poimirlem21  35842  poimirlem22  35843  poimirlem23  35844  poimirlem24  35845  poimirlem25  35846  poimirlem26  35847  poimirlem29  35850  poimirlem30  35851  poimirlem31  35852  rrnequiv  36037  lcmineqlem17  40095  lcmineqlem21  40099  3lexlogpow5ineq5  40110  aks4d1p1p4  40121  aks4d1p1p7  40124  aks4d1p3  40128  aks4d1p7d1  40132  2np3bcnp1  40142  2ap1caineq  40143  sticksstones6  40149  sticksstones7  40150  sticksstones22  40166  frlmvscadiccat  40274  fltnltalem  40536  eldioph2lem1  40619  pell1qrge1  40729  rmxypos  40807  ltrmynn0  40808  ltrmxnn0  40809  lermxnn0  40810  jm2.24nn  40819  jm2.24  40823  jm2.19  40853  jm2.26lem3  40861  jm2.27c  40867  hbt  40993  dgraa0p  41012  binomcxplemnn0  42005  fsumnncl  43162  mccllem  43187  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvnxpaek  43532  dvnmul  43533  dvnprodlem2  43537  stoweidlem17  43607  stoweidlem24  43614  wallispilem5  43659  stirlinglem15  43678  fourierdlem48  43744  fourierdlem83  43779  fourierdlem103  43799  fourierdlem104  43800  sqwvfoura  43818  elaa2lem  43823  etransclem10  43834  etransclem19  43843  etransclem20  43844  etransclem21  43845  etransclem22  43846  etransclem23  43847  etransclem24  43848  etransclem27  43851  etransclem32  43856  etransclem35  43859  etransclem44  43868  etransclem45  43869  etransclem46  43870  etransclem47  43871  etransclem48  43872  etransc  43873  rrndistlt  43880  fmtnoge3  45040  sqrtpwpw2p  45048  fmtnosqrt  45049  flsqrt  45103  lighneallem4a  45118  ssnn0ssfz  45743  pgrple2abl  45759  nn0eo  45932  fllog2  45972  itcovalt2lem2lem1  46077  aacllem  46563