Theorem nn0red 12463

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℕ₀cn0 12401

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-n0 12402

This theorem is referenced by:  nn0cnd  12464  nn0readdcl  12468  eluzmn  12758  flmulnn0  13747  quoremz  13775  quoremnn0ALT  13777  modaddmodup  13857  modaddmodlo  13858  expneg  13992  expnbnd  14155  facdiv  14210  faclbnd6  14222  hashdom  14302  hashun2  14306  hashunx  14309  hashfun  14360  hashf1  14380  seqcoll2  14388  hashge2el2dif  14403  hashtpg  14408  wrdlenge2n0  14475  ccatdmss  14505  ccatsymb  14506  ccatrn  14513  ccatalpha  14517  ccat2s1fvw  14562  swrdnd  14578  swrdnd0  14581  pfxnd0  14612  pfxsuffeqwrdeq  14621  swrdccat3blem  14662  cshwidxmod  14726  repswcshw  14735  swrds2  14863  modfsummods  15716  climcnds  15774  geomulcvg  15799  mertenslem1  15807  binomfallfaclem2  15963  binomrisefac  15965  fallfacval4  15966  efcllem  16000  eftlub  16034  ruclem10  16164  oddge22np1  16276  nn0oddm1d2  16312  divalglem5  16324  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  sadcaddlem  16384  sadaddlem  16393  sadasslem  16397  sadeq  16399  smuval2  16409  smupvallem  16410  smueqlem  16417  bezoutlem3  16468  bezoutlem4  16469  gcdzeq  16479  dvdssqlem  16493  nn0seqcvgd  16497  eucalglt  16512  lcmneg  16530  mulgcddvds  16582  qredeu  16585  prmdvdsbc  16653  prmdiveq  16713  odzdvds  16723  pythagtriplem3  16746  pythagtriplem6  16749  pythagtriplem7  16750  iserodd  16763  pclem  16766  pcpremul  16771  pcidlem  16800  pcgcd1  16805  pc2dvds  16807  pcz  16809  pcprmpw2  16810  fldivp1  16825  pcfaclem  16826  pcfac  16827  pcbc  16828  prmreclem2  16845  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  4sqlem11  16883  4sqlem12  16884  4sqlem14  16886  vdwlem11  16919  vdwlem12  16920  ramlb  16947  0ram  16948  ram0  16950  ramub1lem2  16955  ramcl  16957  psgnunilem2  19424  odmodnn0  19469  mndodconglem  19470  mndodcong  19471  oddvds  19476  odhash3  19505  gexdvds  19513  sylow1lem1  19527  sylow1lem5  19531  pgpfi  19534  pgpssslw  19543  efgsfo  19668  efgredlemd  19673  efgredlem  19676  efgred  19677  lt6abl  19824  telgsums  19922  pgpfaclem2  20013  srgbinomlem3  20163  zringlpirlem3  21419  psrbaglesupp  21878  psrbagcon  21881  psrbagleadd1  21884  mplmonmul  21991  psdmul  22109  coe1tmmul2  22218  coe1tmmul2fv  22220  coe1pwmulfv  22222  gsummoncoe1  22252  fvmptnn04if  22793  fvmptnn04ifc  22796  fvmptnn04ifd  22797  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  lebnumii  24921  dyadmaxlem  25554  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mdegmullem  26039  coe1mul3  26060  coe1mul4  26061  deg1sublt  26071  deg1mul2  26075  deg1tmle  26079  deg1tm  26080  ply1divmo  26097  ply1divex  26098  deg1submon1p  26114  dvdsq1p  26124  fta1glem2  26130  fta1blem  26132  plyco0  26153  plyeq0lem  26171  plypf1  26173  plyaddlem1  26174  coeeulem  26185  dgrub  26195  dgrlb  26197  dgreq  26205  coeaddlem  26210  coemullem  26211  coemulhi  26215  dgrlt  26228  dgradd2  26230  dgrmul  26232  dgrcolem2  26236  dgrco  26237  plydivlem3  26259  plydivlem4  26260  plydivex  26261  plydiveu  26262  fta1lem  26271  quotcan  26273  vieta1lem2  26275  radcnvlem1  26378  dvradcnv  26386  leibpi  26908  log2tlbnd  26911  birthdaylem2  26918  birthdaylem3  26919  fsumharmonic  26978  dmlogdmgm  26990  basellem3  27049  basellem5  27051  issqf  27102  ppip1le  27127  ppiltx  27143  mumullem2  27146  sgmppw  27164  ppiub  27171  chtublem  27178  chpub  27187  dchrabs  27227  bcmono  27244  bcmax  27245  bcp1ctr  27246  bclbnd  27247  bposlem5  27255  gausslemma2dlem0h  27330  gausslemma2dlem4  27336  gausslemma2dlem6  27339  lgseisenlem1  27342  2lgsoddprmlem2  27376  2sqlem7  27391  2sqlem8  27393  2sq2  27400  2sqmod  27403  chebbnd1lem1  27436  chtppilimlem1  27440  dchrisum0re  27480  mulogsumlem  27498  selberg2lem  27517  pntrlog2bndlem4  27547  pntlemr  27569  pntlemj  27570  pnt  27581  ostth2lem3  27602  vtxdgfival  29543  vtxdfiun  29556  vtxdginducedm1fi  29618  crctcsh  29897  wwlksnred  29965  wwlksnextproplem2  29983  rusgrnumwwlks  30050  eupth2lems  30313  eucrct2eupth  30320  numclwlk1lem1  30444  numclwwlk5  30463  numclwwlk6  30465  friendshipgt3  30473  nnmulge  32818  nndiffz1  32866  fzo0opth  32883  suppssnn0  32885  pfxlsw2ccat  33032  wrdt2ind  33035  gsumwrd2dccatlem  33159  cycpmrn  33225  cyc3conja  33239  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  ply1unit  33656  ply1dg3rt0irred  33665  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  esplyfval2  33723  esplyfval3  33730  exsslsb  33753  ply1degltdimlem  33779  ply1degltdim  33780  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  extdgfialglem1  33849  minplyirredlem  33867  irredminply  33873  nn0constr  33918  iconstr  33923  cos9thpiminplylem1  33939  oddpwdc  34511  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemb  34525  coinfliplem  34636  signsplypnf  34707  signslema  34719  signstfvc  34731  signstfveq0  34734  fsum2dsub  34764  reprlt  34776  reprgt  34778  reprinfz1  34779  breprexplemc  34789  lpadmax  34839  lpadright  34841  usgrgt2cycl  35324  acycgr1v  35343  erdszelem8  35392  erdsze2lem2  35398  cvmliftlem7  35485  snmlff  35523  bcprod  35932  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  rrnequiv  38036  lcmineqlem17  42299  lcmineqlem21  42303  3lexlogpow5ineq5  42314  aks4d1p1p4  42325  aks4d1p1p7  42328  aks4d1p3  42332  aks4d1p7d1  42336  aks6d1c1  42370  aks6d1c3  42377  aks6d1c2lem4  42381  hashnexinj  42382  aks6d1c2  42384  aks6d1c5lem1  42390  aks6d1c5lem3  42391  aks6d1c5lem2  42392  aks6d1c5  42393  2np3bcnp1  42398  2ap1caineq  42399  sticksstones6  42405  sticksstones7  42406  sticksstones22  42422  aks6d1c6lem3  42426  aks6d1c6lem4  42427  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7lem2  42435  unitscyglem1  42449  unitscyglem4  42452  aks5lem8  42455  frlmvscadiccat  42761  fltnltalem  42905  eldioph2lem1  43002  pell1qrge1  43112  rmxypos  43189  ltrmynn0  43190  ltrmxnn0  43191  lermxnn0  43192  jm2.24nn  43201  jm2.24  43205  jm2.19  43235  jm2.26lem3  43243  jm2.27c  43249  hbt  43372  dgraa0p  43391  binomcxplemnn0  44590  fsumnncl  45818  mccllem  45843  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnmul  46187  dvnprodlem2  46191  stoweidlem17  46261  stoweidlem24  46268  wallispilem5  46313  stirlinglem15  46332  fourierdlem48  46398  fourierdlem83  46433  fourierdlem103  46453  fourierdlem104  46454  sqwvfoura  46472  elaa2lem  46477  etransclem10  46488  etransclem19  46497  etransclem20  46498  etransclem21  46499  etransclem22  46500  etransclem23  46501  etransclem24  46502  etransclem27  46505  etransclem32  46510  etransclem35  46513  etransclem44  46522  etransclem45  46523  etransclem46  46524  etransclem47  46525  etransclem48  46526  etransc  46527  rrndistlt  46534  chnsubseqwl  47123  chnsubseq  47124  fmtnoge3  47776  sqrtpwpw2p  47784  fmtnosqrt  47785  flsqrt  47839  lighneallem4a  47854  ssnn0ssfz  48595  pgrple2abl  48611  nn0eo  48774  fllog2  48814  itcovalt2lem2lem1  48919  aacllem  50046