Theorem nn0red 12554

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℕ₀cn0 12492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12222  df-n0 12493

This theorem is referenced by:  nn0cnd  12555  nn0readdcl  12559  eluzmn  12857  flmulnn0  13848  quoremz  13876  quoremnn0ALT  13878  modaddmodup  13958  modaddmodlo  13959  expneg  14093  expnbnd  14256  facdiv  14311  faclbnd6  14323  hashdom  14403  hashun2  14407  hashunx  14410  hashfun  14462  hashf1  14482  seqcoll2  14490  hashge2el2dif  14505  hashtpg  14510  wrdlenge2n0  14577  ccatdmss  14607  ccatsymb  14608  ccatrn  14615  ccatalpha  14619  ccat2s1fvw  14664  swrdnd  14680  swrdnd0  14683  pfxnd0  14714  pfxsuffeqwrdeq  14723  swrdccat3blem  14764  cshwidxmod  14828  repswcshw  14837  swrds2  14965  modfsummods  15833  climcnds  15893  geomulcvg  15918  mertenslem1  15926  binomfallfaclem2  16082  binomrisefac  16084  fallfacval4  16085  efcllem  16119  eftlub  16153  ruclem10  16283  oddge22np1  16395  nn0oddm1d2  16431  divalglem5  16443  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  sadcaddlem  16503  sadaddlem  16512  sadasslem  16516  sadeq  16518  smuval2  16528  smupvallem  16529  smueqlem  16536  bezoutlem3  16587  bezoutlem4  16588  gcdzeq  16598  dvdssqlem  16612  nn0seqcvgd  16616  eucalglt  16631  lcmneg  16649  mulgcddvds  16701  qredeu  16704  prmdvdsbc  16773  prmdiveq  16833  odzdvds  16843  pythagtriplem3  16866  pythagtriplem6  16869  pythagtriplem7  16870  iserodd  16883  pclem  16886  pcpremul  16891  pcidlem  16920  pcgcd1  16925  pc2dvds  16927  pcz  16929  pcprmpw2  16930  fldivp1  16945  pcfaclem  16946  pcfac  16947  pcbc  16948  prmreclem2  16965  prmreclem3  16966  prmreclem4  16967  prmreclem5  16968  4sqlem11  17003  4sqlem12  17004  4sqlem14  17006  vdwlem11  17039  vdwlem12  17040  ramlb  17067  0ram  17068  ram0  17070  ramub1lem2  17075  ramcl  17077  psgnunilem2  19553  odmodnn0  19598  mndodconglem  19599  mndodcong  19600  oddvds  19605  odhash3  19634  gexdvds  19642  sylow1lem1  19656  sylow1lem5  19660  pgpfi  19663  pgpssslw  19672  efgsfo  19797  efgredlemd  19802  efgredlem  19805  efgred  19806  lt6abl  19953  telgsums  20051  pgpfaclem2  20142  srgbinomlem3  20298  zringlpirlem3  21571  psrbaglesupp  22029  psrbagcon  22032  psrbagleadd1  22035  mplmonmul  22144  psdmul  22286  coe1tmmul2  22394  coe1tmmul2fv  22396  coe1pwmulfv  22398  gsummoncoe1  22425  fvmptnn04if  22963  fvmptnn04ifc  22966  fvmptnn04ifd  22967  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  lebnumii  25082  dyadmaxlem  25713  mbfi1fseqlem3  25833  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mdegmullem  26192  coe1mul3  26213  coe1mul4  26214  deg1sublt  26224  deg1mul2  26228  deg1tmle  26232  deg1tm  26233  ply1divmo  26250  ply1divex  26251  deg1submon1p  26267  dvdsq1p  26277  fta1glem2  26283  fta1blem  26285  plyco0  26306  plyeq0lem  26324  plypf1  26326  plyaddlem1  26327  coeeulem  26338  dgrub  26348  dgrlb  26350  dgreq  26358  coeaddlem  26363  coemullem  26364  coemulhi  26368  dgrlt  26380  dgradd2  26382  dgrmul  26384  dgrcolem2  26388  dgrco  26389  plydivlem3  26413  plydivlem4  26414  plydivex  26415  plydiveu  26416  fta1lem  26425  quotcan  26427  vieta1lem2  26429  radcnvlem1  26530  dvradcnv  26538  leibpi  27061  log2tlbnd  27064  birthdaylem2  27071  birthdaylem3  27072  fsumharmonic  27130  dmlogdmgm  27142  basellem3  27201  basellem5  27203  issqf  27254  ppip1le  27279  ppiltx  27295  mumullem2  27298  sgmppw  27315  ppiub  27322  chtublem  27329  chpub  27338  dchrabs  27378  bcmono  27395  bcmax  27396  bcp1ctr  27397  bclbnd  27398  bposlem5  27406  gausslemma2dlem0h  27481  gausslemma2dlem4  27487  gausslemma2dlem6  27490  lgseisenlem1  27493  2lgsoddprmlem2  27527  2sqlem7  27542  2sqlem8  27544  2sq2  27551  2sqmod  27554  chebbnd1lem1  27587  chtppilimlem1  27591  dchrisum0re  27631  mulogsumlem  27649  selberg2lem  27668  pntrlog2bndlem4  27698  pntlemr  27720  pntlemj  27721  pnt  27732  ostth2lem3  27753  vtxdgfival  29724  vtxdfiun  29737  vtxdginducedm1fi  29799  crctcsh  30078  wwlksnred  30146  wwlksnextproplem2  30164  rusgrnumwwlks  30231  eupth2lems  30494  eucrct2eupth  30501  numclwlk1lem1  30625  numclwwlk5  30644  numclwwlk6  30646  friendshipgt3  30654  nnmulge  32992  nndiffz1  33039  fzo0opth  33056  suppssnn0  33058  pfxlsw2ccat  33178  wrdt2ind  33181  gsumwrd2dccatlem  33305  cycpmrn  33371  cyc3conja  33385  1arithidomlem1  33737  1arithidomlem2  33738  1arithidom  33739  ply1unit  33777  ply1dg3rt0irred  33786  ply1degltel  33796  ply1degleel  33797  ply1degltlss  33798  psrmonmul  33852  esplyfval2  33867  esplyfval3  33874  exsslsb  33899  ply1degltdimlem  33924  ply1degltdim  33925  fldextrspundgdvdslem  33982  fldextrspundgdvds  33983  extdgfialglem1  33994  minplyirredlem  34012  irredminply  34018  nn0constr  34063  iconstr  34068  cos9thpiminplylem1  34084  oddpwdc  34656  eulerpartlems  34662  eulerpartlemgc  34664  eulerpartlemb  34670  coinfliplem  34781  signsplypnf  34849  signslema  34861  signstfvc  34873  signstfveq0  34876  fsum2dsub  34906  reprlt  34918  reprgt  34920  reprinfz1  34921  breprexplemc  34931  lpadmax  34984  lpadright  34986  usgrgt2cycl  35488  acycgr1v  35507  erdszelem8  35556  erdsze2lem2  35562  cvmliftlem7  35649  snmlff  35687  bcprod  36096  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem13  38139  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem21  38147  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem25  38151  poimirlem26  38152  poimirlem29  38155  poimirlem30  38156  poimirlem31  38157  rrnequiv  38341  lcmineqlem17  42669  lcmineqlem21  42673  3lexlogpow5ineq5  42684  aks4d1p1p4  42695  aks4d1p1p7  42698  aks4d1p3  42702  aks4d1p7d1  42706  aks6d1c1  42740  aks6d1c3  42747  aks6d1c2lem4  42751  hashnexinj  42752  aks6d1c2  42754  aks6d1c5lem1  42760  aks6d1c5lem3  42761  aks6d1c5lem2  42762  aks6d1c5  42763  2np3bcnp1  42768  2ap1caineq  42769  sticksstones6  42775  sticksstones7  42776  sticksstones22  42792  aks6d1c6lem3  42796  aks6d1c6lem4  42797  bcled  42802  bcle2d  42803  aks6d1c7lem1  42804  aks6d1c7lem2  42805  unitscyglem1  42819  unitscyglem4  42822  aks5lem8  42825  frlmvscadiccat  43135  fltnltalem  43251  eldioph2lem1  43348  pell1qrge1  43454  rmxypos  43531  ltrmynn0  43532  ltrmxnn0  43533  lermxnn0  43534  jm2.24nn  43543  jm2.24  43547  jm2.19  43577  jm2.26lem3  43585  jm2.27c  43591  hbt  43714  dgraa0p  43733  binomcxplemnn0  44918  fsumnncl  46147  mccllem  46172  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnxpaek  46515  dvnmul  46516  dvnprodlem2  46520  stoweidlem17  46590  stoweidlem24  46597  wallispilem5  46642  stirlinglem15  46661  fourierdlem48  46727  fourierdlem83  46762  fourierdlem103  46782  fourierdlem104  46783  sqwvfoura  46801  elaa2lem  46806  etransclem10  46817  etransclem19  46826  etransclem20  46827  etransclem21  46828  etransclem22  46829  etransclem23  46830  etransclem24  46831  etransclem27  46834  etransclem32  46839  etransclem35  46842  etransclem44  46851  etransclem45  46852  etransclem46  46853  etransclem47  46854  etransclem48  46855  etransc  46856  rrndistlt  46863  chnsubseqwl  47454  chnsubseq  47455  fmtnoge3  48138  sqrtpwpw2p  48146  fmtnosqrt  48147  flsqrt  48201  lighneallem4a  48216  ssnn0ssfz  48981  pgrple2abl  48997  nn0eo  49160  fllog2  49200  itcovalt2lem2lem1  49305  aacllem  50431