Theorem nn0red 12443

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11005  ℕ₀cn0 12381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-n0 12382

This theorem is referenced by:  nn0cnd  12444  nn0readdcl  12448  eluzmn  12739  flmulnn0  13731  quoremz  13759  quoremnn0ALT  13761  modaddmodup  13841  modaddmodlo  13842  expneg  13976  expnbnd  14139  facdiv  14194  faclbnd6  14206  hashdom  14286  hashun2  14290  hashunx  14293  hashfun  14344  hashf1  14364  seqcoll2  14372  hashge2el2dif  14387  hashtpg  14392  wrdlenge2n0  14459  ccatdmss  14489  ccatsymb  14490  ccatrn  14497  ccatalpha  14501  ccat2s1fvw  14546  swrdnd  14562  swrdnd0  14565  pfxnd0  14596  pfxsuffeqwrdeq  14605  swrdccat3blem  14646  cshwidxmod  14710  repswcshw  14719  swrds2  14847  modfsummods  15700  climcnds  15758  geomulcvg  15783  mertenslem1  15791  binomfallfaclem2  15947  binomrisefac  15949  fallfacval4  15950  efcllem  15984  eftlub  16018  ruclem10  16148  oddge22np1  16260  nn0oddm1d2  16296  divalglem5  16308  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  sadcaddlem  16368  sadaddlem  16377  sadasslem  16381  sadeq  16383  smuval2  16393  smupvallem  16394  smueqlem  16401  bezoutlem3  16452  bezoutlem4  16453  gcdzeq  16463  dvdssqlem  16477  nn0seqcvgd  16481  eucalglt  16496  lcmneg  16514  mulgcddvds  16566  qredeu  16569  prmdvdsbc  16637  prmdiveq  16697  odzdvds  16707  pythagtriplem3  16730  pythagtriplem6  16733  pythagtriplem7  16734  iserodd  16747  pclem  16750  pcpremul  16755  pcidlem  16784  pcgcd1  16789  pc2dvds  16791  pcz  16793  pcprmpw2  16794  fldivp1  16809  pcfaclem  16810  pcfac  16811  pcbc  16812  prmreclem2  16829  prmreclem3  16830  prmreclem4  16831  prmreclem5  16832  4sqlem11  16867  4sqlem12  16868  4sqlem14  16870  vdwlem11  16903  vdwlem12  16904  ramlb  16931  0ram  16932  ram0  16934  ramub1lem2  16939  ramcl  16941  psgnunilem2  19408  odmodnn0  19453  mndodconglem  19454  mndodcong  19455  oddvds  19460  odhash3  19489  gexdvds  19497  sylow1lem1  19511  sylow1lem5  19515  pgpfi  19518  pgpssslw  19527  efgsfo  19652  efgredlemd  19657  efgredlem  19660  efgred  19661  lt6abl  19808  telgsums  19906  pgpfaclem2  19997  srgbinomlem3  20147  zringlpirlem3  21402  psrbaglesupp  21860  psrbagcon  21863  psrbagleadd1  21866  mplmonmul  21972  psdmul  22082  coe1tmmul2  22191  coe1tmmul2fv  22193  coe1pwmulfv  22195  gsummoncoe1  22224  fvmptnn04if  22765  fvmptnn04ifc  22768  fvmptnn04ifd  22769  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  lebnumii  24893  dyadmaxlem  25526  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mdegmullem  26011  coe1mul3  26032  coe1mul4  26033  deg1sublt  26043  deg1mul2  26047  deg1tmle  26051  deg1tm  26052  ply1divmo  26069  ply1divex  26070  deg1submon1p  26086  dvdsq1p  26096  fta1glem2  26102  fta1blem  26104  plyco0  26125  plyeq0lem  26143  plypf1  26145  plyaddlem1  26146  coeeulem  26157  dgrub  26167  dgrlb  26169  dgreq  26177  coeaddlem  26182  coemullem  26183  coemulhi  26187  dgrlt  26200  dgradd2  26202  dgrmul  26204  dgrcolem2  26208  dgrco  26209  plydivlem3  26231  plydivlem4  26232  plydivex  26233  plydiveu  26234  fta1lem  26243  quotcan  26245  vieta1lem2  26247  radcnvlem1  26350  dvradcnv  26358  leibpi  26880  log2tlbnd  26883  birthdaylem2  26890  birthdaylem3  26891  fsumharmonic  26950  dmlogdmgm  26962  basellem3  27021  basellem5  27023  issqf  27074  ppip1le  27099  ppiltx  27115  mumullem2  27118  sgmppw  27136  ppiub  27143  chtublem  27150  chpub  27159  dchrabs  27199  bcmono  27216  bcmax  27217  bcp1ctr  27218  bclbnd  27219  bposlem5  27227  gausslemma2dlem0h  27302  gausslemma2dlem4  27308  gausslemma2dlem6  27311  lgseisenlem1  27314  2lgsoddprmlem2  27348  2sqlem7  27363  2sqlem8  27365  2sq2  27372  2sqmod  27375  chebbnd1lem1  27408  chtppilimlem1  27412  dchrisum0re  27452  mulogsumlem  27470  selberg2lem  27489  pntrlog2bndlem4  27519  pntlemr  27541  pntlemj  27542  pnt  27553  ostth2lem3  27574  vtxdgfival  29449  vtxdfiun  29462  vtxdginducedm1fi  29524  crctcsh  29803  wwlksnred  29871  wwlksnextproplem2  29889  rusgrnumwwlks  29953  eupth2lems  30216  eucrct2eupth  30223  numclwlk1lem1  30347  numclwwlk5  30366  numclwwlk6  30368  friendshipgt3  30376  nnmulge  32720  nndiffz1  32767  fzo0opth  32783  suppssnn0  32785  pfxlsw2ccat  32929  wrdt2ind  32932  gsumwrd2dccatlem  33044  cycpmrn  33110  cyc3conja  33124  1arithidomlem1  33498  1arithidomlem2  33499  1arithidom  33500  ply1unit  33536  ply1dg3rt0irred  33544  ply1degltel  33553  ply1degleel  33554  ply1degltlss  33555  exsslsb  33607  ply1degltdimlem  33633  ply1degltdim  33634  fldextrspundgdvdslem  33691  fldextrspundgdvds  33692  extdgfialglem1  33703  minplyirredlem  33721  irredminply  33727  nn0constr  33772  iconstr  33777  cos9thpiminplylem1  33793  oddpwdc  34365  eulerpartlems  34371  eulerpartlemgc  34373  eulerpartlemb  34379  coinfliplem  34490  signsplypnf  34561  signslema  34573  signstfvc  34585  signstfveq0  34588  fsum2dsub  34618  reprlt  34630  reprgt  34632  reprinfz1  34633  breprexplemc  34643  lpadmax  34693  lpadright  34695  usgrgt2cycl  35172  acycgr1v  35191  erdszelem8  35240  erdsze2lem2  35246  cvmliftlem7  35333  snmlff  35371  bcprod  35780  poimirlem3  37669  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem29  37695  poimirlem30  37696  poimirlem31  37697  rrnequiv  37881  lcmineqlem17  42084  lcmineqlem21  42088  3lexlogpow5ineq5  42099  aks4d1p1p4  42110  aks4d1p1p7  42113  aks4d1p3  42117  aks4d1p7d1  42121  aks6d1c1  42155  aks6d1c3  42162  aks6d1c2lem4  42166  hashnexinj  42167  aks6d1c2  42169  aks6d1c5lem1  42175  aks6d1c5lem3  42176  aks6d1c5lem2  42177  aks6d1c5  42178  2np3bcnp1  42183  2ap1caineq  42184  sticksstones6  42190  sticksstones7  42191  sticksstones22  42207  aks6d1c6lem3  42211  aks6d1c6lem4  42212  bcled  42217  bcle2d  42218  aks6d1c7lem1  42219  aks6d1c7lem2  42220  unitscyglem1  42234  unitscyglem4  42237  aks5lem8  42240  frlmvscadiccat  42545  fltnltalem  42701  eldioph2lem1  42799  pell1qrge1  42909  rmxypos  42986  ltrmynn0  42987  ltrmxnn0  42988  lermxnn0  42989  jm2.24nn  42998  jm2.24  43002  jm2.19  43032  jm2.26lem3  43040  jm2.27c  43046  hbt  43169  dgraa0p  43188  binomcxplemnn0  44388  fsumnncl  45618  mccllem  45643  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  dvnxpaek  45986  dvnmul  45987  dvnprodlem2  45991  stoweidlem17  46061  stoweidlem24  46068  wallispilem5  46113  stirlinglem15  46132  fourierdlem48  46198  fourierdlem83  46233  fourierdlem103  46253  fourierdlem104  46254  sqwvfoura  46272  elaa2lem  46277  etransclem10  46288  etransclem19  46297  etransclem20  46298  etransclem21  46299  etransclem22  46300  etransclem23  46301  etransclem24  46302  etransclem27  46305  etransclem32  46310  etransclem35  46313  etransclem44  46322  etransclem45  46323  etransclem46  46324  etransclem47  46325  etransclem48  46326  etransc  46327  rrndistlt  46334  fmtnoge3  47567  sqrtpwpw2p  47575  fmtnosqrt  47576  flsqrt  47630  lighneallem4a  47645  ssnn0ssfz  48386  pgrple2abl  48402  nn0eo  48566  fllog2  48606  itcovalt2lem2lem1  48711  aacllem  49839