Theorem nn0red 12475

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℕ₀cn0 12413

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-n0 12414

This theorem is referenced by:  nn0cnd  12476  nn0readdcl  12480  eluzmn  12770  flmulnn0  13759  quoremz  13787  quoremnn0ALT  13789  modaddmodup  13869  modaddmodlo  13870  expneg  14004  expnbnd  14167  facdiv  14222  faclbnd6  14234  hashdom  14314  hashun2  14318  hashunx  14321  hashfun  14372  hashf1  14392  seqcoll2  14400  hashge2el2dif  14415  hashtpg  14420  wrdlenge2n0  14487  ccatdmss  14517  ccatsymb  14518  ccatrn  14525  ccatalpha  14529  ccat2s1fvw  14574  swrdnd  14590  swrdnd0  14593  pfxnd0  14624  pfxsuffeqwrdeq  14633  swrdccat3blem  14674  cshwidxmod  14738  repswcshw  14747  swrds2  14875  modfsummods  15728  climcnds  15786  geomulcvg  15811  mertenslem1  15819  binomfallfaclem2  15975  binomrisefac  15977  fallfacval4  15978  efcllem  16012  eftlub  16046  ruclem10  16176  oddge22np1  16288  nn0oddm1d2  16324  divalglem5  16336  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  sadcaddlem  16396  sadaddlem  16405  sadasslem  16409  sadeq  16411  smuval2  16421  smupvallem  16422  smueqlem  16429  bezoutlem3  16480  bezoutlem4  16481  gcdzeq  16491  dvdssqlem  16505  nn0seqcvgd  16509  eucalglt  16524  lcmneg  16542  mulgcddvds  16594  qredeu  16597  prmdvdsbc  16665  prmdiveq  16725  odzdvds  16735  pythagtriplem3  16758  pythagtriplem6  16761  pythagtriplem7  16762  iserodd  16775  pclem  16778  pcpremul  16783  pcidlem  16812  pcgcd1  16817  pc2dvds  16819  pcz  16821  pcprmpw2  16822  fldivp1  16837  pcfaclem  16838  pcfac  16839  pcbc  16840  prmreclem2  16857  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  4sqlem11  16895  4sqlem12  16896  4sqlem14  16898  vdwlem11  16931  vdwlem12  16932  ramlb  16959  0ram  16960  ram0  16962  ramub1lem2  16967  ramcl  16969  psgnunilem2  19436  odmodnn0  19481  mndodconglem  19482  mndodcong  19483  oddvds  19488  odhash3  19517  gexdvds  19525  sylow1lem1  19539  sylow1lem5  19543  pgpfi  19546  pgpssslw  19555  efgsfo  19680  efgredlemd  19685  efgredlem  19688  efgred  19689  lt6abl  19836  telgsums  19934  pgpfaclem2  20025  srgbinomlem3  20175  zringlpirlem3  21431  psrbaglesupp  21890  psrbagcon  21893  psrbagleadd1  21896  mplmonmul  22003  psdmul  22121  coe1tmmul2  22230  coe1tmmul2fv  22232  coe1pwmulfv  22234  gsummoncoe1  22264  fvmptnn04if  22805  fvmptnn04ifc  22808  fvmptnn04ifd  22809  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  lebnumii  24933  dyadmaxlem  25566  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mdegmullem  26051  coe1mul3  26072  coe1mul4  26073  deg1sublt  26083  deg1mul2  26087  deg1tmle  26091  deg1tm  26092  ply1divmo  26109  ply1divex  26110  deg1submon1p  26126  dvdsq1p  26136  fta1glem2  26142  fta1blem  26144  plyco0  26165  plyeq0lem  26183  plypf1  26185  plyaddlem1  26186  coeeulem  26197  dgrub  26207  dgrlb  26209  dgreq  26217  coeaddlem  26222  coemullem  26223  coemulhi  26227  dgrlt  26240  dgradd2  26242  dgrmul  26244  dgrcolem2  26248  dgrco  26249  plydivlem3  26271  plydivlem4  26272  plydivex  26273  plydiveu  26274  fta1lem  26283  quotcan  26285  vieta1lem2  26287  radcnvlem1  26390  dvradcnv  26398  leibpi  26920  log2tlbnd  26923  birthdaylem2  26930  birthdaylem3  26931  fsumharmonic  26990  dmlogdmgm  27002  basellem3  27061  basellem5  27063  issqf  27114  ppip1le  27139  ppiltx  27155  mumullem2  27158  sgmppw  27176  ppiub  27183  chtublem  27190  chpub  27199  dchrabs  27239  bcmono  27256  bcmax  27257  bcp1ctr  27258  bclbnd  27259  bposlem5  27267  gausslemma2dlem0h  27342  gausslemma2dlem4  27348  gausslemma2dlem6  27351  lgseisenlem1  27354  2lgsoddprmlem2  27388  2sqlem7  27403  2sqlem8  27405  2sq2  27412  2sqmod  27415  chebbnd1lem1  27448  chtppilimlem1  27452  dchrisum0re  27492  mulogsumlem  27510  selberg2lem  27529  pntrlog2bndlem4  27559  pntlemr  27581  pntlemj  27582  pnt  27593  ostth2lem3  27614  vtxdgfival  29555  vtxdfiun  29568  vtxdginducedm1fi  29630  crctcsh  29909  wwlksnred  29977  wwlksnextproplem2  29995  rusgrnumwwlks  30062  eupth2lems  30325  eucrct2eupth  30332  numclwlk1lem1  30456  numclwwlk5  30475  numclwwlk6  30477  friendshipgt3  30485  nnmulge  32828  nndiffz1  32876  fzo0opth  32893  suppssnn0  32895  pfxlsw2ccat  33042  wrdt2ind  33045  gsumwrd2dccatlem  33170  cycpmrn  33236  cyc3conja  33250  1arithidomlem1  33627  1arithidomlem2  33628  1arithidom  33629  ply1unit  33667  ply1dg3rt0irred  33676  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  psrmonmul  33726  esplyfval2  33741  esplyfval3  33748  exsslsb  33773  ply1degltdimlem  33799  ply1degltdim  33800  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  extdgfialglem1  33869  minplyirredlem  33887  irredminply  33893  nn0constr  33938  iconstr  33943  cos9thpiminplylem1  33959  oddpwdc  34531  eulerpartlems  34537  eulerpartlemgc  34539  eulerpartlemb  34545  coinfliplem  34656  signsplypnf  34727  signslema  34739  signstfvc  34751  signstfveq0  34754  fsum2dsub  34784  reprlt  34796  reprgt  34798  reprinfz1  34799  breprexplemc  34809  lpadmax  34859  lpadright  34861  usgrgt2cycl  35343  acycgr1v  35362  erdszelem8  35411  erdsze2lem2  35417  cvmliftlem7  35504  snmlff  35542  bcprod  35951  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem13  37881  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem23  37891  poimirlem24  37892  poimirlem25  37893  poimirlem26  37894  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  rrnequiv  38083  lcmineqlem17  42412  lcmineqlem21  42416  3lexlogpow5ineq5  42427  aks4d1p1p4  42438  aks4d1p1p7  42441  aks4d1p3  42445  aks4d1p7d1  42449  aks6d1c1  42483  aks6d1c3  42490  aks6d1c2lem4  42494  hashnexinj  42495  aks6d1c2  42497  aks6d1c5lem1  42503  aks6d1c5lem3  42504  aks6d1c5lem2  42505  aks6d1c5  42506  2np3bcnp1  42511  2ap1caineq  42512  sticksstones6  42518  sticksstones7  42519  sticksstones22  42535  aks6d1c6lem3  42539  aks6d1c6lem4  42540  bcled  42545  bcle2d  42546  aks6d1c7lem1  42547  aks6d1c7lem2  42548  unitscyglem1  42562  unitscyglem4  42565  aks5lem8  42568  frlmvscadiccat  42873  fltnltalem  43017  eldioph2lem1  43114  pell1qrge1  43224  rmxypos  43301  ltrmynn0  43302  ltrmxnn0  43303  lermxnn0  43304  jm2.24nn  43313  jm2.24  43317  jm2.19  43347  jm2.26lem3  43355  jm2.27c  43361  hbt  43484  dgraa0p  43503  binomcxplemnn0  44702  fsumnncl  45929  mccllem  45954  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnxpaek  46297  dvnmul  46298  dvnprodlem2  46302  stoweidlem17  46372  stoweidlem24  46379  wallispilem5  46424  stirlinglem15  46443  fourierdlem48  46509  fourierdlem83  46544  fourierdlem103  46564  fourierdlem104  46565  sqwvfoura  46583  elaa2lem  46588  etransclem10  46599  etransclem19  46608  etransclem20  46609  etransclem21  46610  etransclem22  46611  etransclem23  46612  etransclem24  46613  etransclem27  46616  etransclem32  46621  etransclem35  46624  etransclem44  46633  etransclem45  46634  etransclem46  46635  etransclem47  46636  etransclem48  46637  etransc  46638  rrndistlt  46645  chnsubseqwl  47234  chnsubseq  47235  fmtnoge3  47887  sqrtpwpw2p  47895  fmtnosqrt  47896  flsqrt  47950  lighneallem4a  47965  ssnn0ssfz  48706  pgrple2abl  48722  nn0eo  48885  fllog2  48925  itcovalt2lem2lem1  49030  aacllem  50157