Theorem nn0red 12504

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℕ₀cn0 12442

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  nn0cnd  12505  nn0readdcl  12509  eluzmn  12800  flmulnn0  13789  quoremz  13817  quoremnn0ALT  13819  modaddmodup  13899  modaddmodlo  13900  expneg  14034  expnbnd  14197  facdiv  14252  faclbnd6  14264  hashdom  14344  hashun2  14348  hashunx  14351  hashfun  14402  hashf1  14422  seqcoll2  14430  hashge2el2dif  14445  hashtpg  14450  wrdlenge2n0  14517  ccatsymb  14547  ccatrn  14554  ccatalpha  14558  ccat2s1fvw  14603  swrdnd  14619  swrdnd0  14622  pfxnd0  14653  pfxsuffeqwrdeq  14663  swrdccat3blem  14704  cshwidxmod  14768  repswcshw  14777  swrds2  14906  modfsummods  15759  climcnds  15817  geomulcvg  15842  mertenslem1  15850  binomfallfaclem2  16006  binomrisefac  16008  fallfacval4  16009  efcllem  16043  eftlub  16077  ruclem10  16207  oddge22np1  16319  nn0oddm1d2  16355  divalglem5  16367  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  sadcaddlem  16427  sadaddlem  16436  sadasslem  16440  sadeq  16442  smuval2  16452  smupvallem  16453  smueqlem  16460  bezoutlem3  16511  bezoutlem4  16512  gcdzeq  16522  dvdssqlem  16536  nn0seqcvgd  16540  eucalglt  16555  lcmneg  16573  mulgcddvds  16625  qredeu  16628  prmdvdsbc  16696  prmdiveq  16756  odzdvds  16766  pythagtriplem3  16789  pythagtriplem6  16792  pythagtriplem7  16793  iserodd  16806  pclem  16809  pcpremul  16814  pcidlem  16843  pcgcd1  16848  pc2dvds  16850  pcz  16852  pcprmpw2  16853  fldivp1  16868  pcfaclem  16869  pcfac  16870  pcbc  16871  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  vdwlem11  16962  vdwlem12  16963  ramlb  16990  0ram  16991  ram0  16993  ramub1lem2  16998  ramcl  17000  psgnunilem2  19425  odmodnn0  19470  mndodconglem  19471  mndodcong  19472  oddvds  19477  odhash3  19506  gexdvds  19514  sylow1lem1  19528  sylow1lem5  19532  pgpfi  19535  pgpssslw  19544  efgsfo  19669  efgredlemd  19674  efgredlem  19677  efgred  19678  lt6abl  19825  telgsums  19923  pgpfaclem2  20014  srgbinomlem3  20137  zringlpirlem3  21374  psrbaglesupp  21831  psrbagcon  21834  psrbagleadd1  21837  mplmonmul  21943  psdmul  22053  coe1tmmul2  22162  coe1tmmul2fv  22164  coe1pwmulfv  22166  gsummoncoe1  22195  fvmptnn04if  22736  fvmptnn04ifc  22739  fvmptnn04ifd  22740  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  lebnumii  24865  dyadmaxlem  25498  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mdegmullem  25983  coe1mul3  26004  coe1mul4  26005  deg1sublt  26015  deg1mul2  26019  deg1tmle  26023  deg1tm  26024  ply1divmo  26041  ply1divex  26042  deg1submon1p  26058  dvdsq1p  26068  fta1glem2  26074  fta1blem  26076  plyco0  26097  plyeq0lem  26115  plypf1  26117  plyaddlem1  26118  coeeulem  26129  dgrub  26139  dgrlb  26141  dgreq  26149  coeaddlem  26154  coemullem  26155  coemulhi  26159  dgrlt  26172  dgradd2  26174  dgrmul  26176  dgrcolem2  26180  dgrco  26181  plydivlem3  26203  plydivlem4  26204  plydivex  26205  plydiveu  26206  fta1lem  26215  quotcan  26217  vieta1lem2  26219  radcnvlem1  26322  dvradcnv  26330  leibpi  26852  log2tlbnd  26855  birthdaylem2  26862  birthdaylem3  26863  fsumharmonic  26922  dmlogdmgm  26934  basellem3  26993  basellem5  26995  issqf  27046  ppip1le  27071  ppiltx  27087  mumullem2  27090  sgmppw  27108  ppiub  27115  chtublem  27122  chpub  27131  dchrabs  27171  bcmono  27188  bcmax  27189  bcp1ctr  27190  bclbnd  27191  bposlem5  27199  gausslemma2dlem0h  27274  gausslemma2dlem4  27280  gausslemma2dlem6  27283  lgseisenlem1  27286  2lgsoddprmlem2  27320  2sqlem7  27335  2sqlem8  27337  2sq2  27344  2sqmod  27347  chebbnd1lem1  27380  chtppilimlem1  27384  dchrisum0re  27424  mulogsumlem  27442  selberg2lem  27461  pntrlog2bndlem4  27491  pntlemr  27513  pntlemj  27514  pnt  27525  ostth2lem3  27546  vtxdgfival  29397  vtxdfiun  29410  vtxdginducedm1fi  29472  crctcsh  29754  wwlksnred  29822  wwlksnextproplem2  29840  rusgrnumwwlks  29904  eupth2lems  30167  eucrct2eupth  30174  numclwlk1lem1  30298  numclwwlk5  30317  numclwwlk6  30319  friendshipgt3  30327  nnmulge  32662  nndiffz1  32709  fzo0opth  32728  suppssnn0  32730  ccatdmss  32871  pfxlsw2ccat  32872  wrdt2ind  32875  gsumwrd2dccatlem  33006  cycpmrn  33100  cyc3conja  33114  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  ply1unit  33544  ply1dg3rt0irred  33551  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  exsslsb  33592  ply1degltdimlem  33618  ply1degltdim  33619  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  minplyirredlem  33700  irredminply  33706  nn0constr  33751  iconstr  33756  cos9thpiminplylem1  33772  oddpwdc  34345  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemb  34359  coinfliplem  34470  signsplypnf  34541  signslema  34553  signstfvc  34565  signstfveq0  34568  fsum2dsub  34598  reprlt  34610  reprgt  34612  reprinfz1  34613  breprexplemc  34623  lpadmax  34673  lpadright  34675  usgrgt2cycl  35117  acycgr1v  35136  erdszelem8  35185  erdsze2lem2  35191  cvmliftlem7  35278  snmlff  35316  bcprod  35725  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  rrnequiv  37829  lcmineqlem17  42033  lcmineqlem21  42037  3lexlogpow5ineq5  42048  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p3  42066  aks4d1p7d1  42070  aks6d1c1  42104  aks6d1c3  42111  aks6d1c2lem4  42115  hashnexinj  42116  aks6d1c2  42118  aks6d1c5lem1  42124  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c5  42127  2np3bcnp1  42132  2ap1caineq  42133  sticksstones6  42139  sticksstones7  42140  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  unitscyglem1  42183  unitscyglem4  42186  aks5lem8  42189  frlmvscadiccat  42494  fltnltalem  42650  eldioph2lem1  42748  pell1qrge1  42858  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  lermxnn0  42939  jm2.24nn  42948  jm2.24  42952  jm2.19  42982  jm2.26lem3  42990  jm2.27c  42996  hbt  43119  dgraa0p  43138  binomcxplemnn0  44338  fsumnncl  45570  mccllem  45595  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnmul  45941  dvnprodlem2  45945  stoweidlem17  46015  stoweidlem24  46022  wallispilem5  46067  stirlinglem15  46086  fourierdlem48  46152  fourierdlem83  46187  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  elaa2lem  46231  etransclem10  46242  etransclem19  46251  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem27  46259  etransclem32  46264  etransclem35  46267  etransclem44  46276  etransclem45  46277  etransclem46  46278  etransclem47  46279  etransclem48  46280  etransc  46281  rrndistlt  46288  fmtnoge3  47531  sqrtpwpw2p  47539  fmtnosqrt  47540  flsqrt  47594  lighneallem4a  47609  ssnn0ssfz  48337  pgrple2abl  48353  nn0eo  48517  fllog2  48557  itcovalt2lem2lem1  48662  aacllem  49790