Theorem nn0red 12614

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294  df-n0 12554

This theorem is referenced by:  nn0cnd  12615  nn0readdcl  12619  eluzmn  12910  flmulnn0  13878  quoremz  13906  quoremnn0ALT  13908  modaddmodup  13985  modaddmodlo  13986  expneg  14120  expnbnd  14281  facdiv  14336  faclbnd6  14348  hashdom  14428  hashun2  14432  hashunx  14435  hashfun  14486  hashf1  14506  seqcoll2  14514  hashge2el2dif  14529  hashtpg  14534  wrdlenge2n0  14600  ccatsymb  14630  ccatrn  14637  ccatalpha  14641  ccat2s1fvw  14686  swrdnd  14702  swrdnd0  14705  pfxnd0  14736  pfxsuffeqwrdeq  14746  swrdccat3blem  14787  cshwidxmod  14851  repswcshw  14860  swrds2  14989  modfsummods  15841  climcnds  15899  geomulcvg  15924  mertenslem1  15932  binomfallfaclem2  16088  binomrisefac  16090  fallfacval4  16091  efcllem  16125  eftlub  16157  ruclem10  16287  oddge22np1  16397  nn0oddm1d2  16433  divalglem5  16445  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  sadcaddlem  16503  sadaddlem  16512  sadasslem  16516  sadeq  16518  smuval2  16528  smupvallem  16529  smueqlem  16536  bezoutlem3  16588  bezoutlem4  16589  gcdzeq  16599  dvdssqlem  16613  nn0seqcvgd  16617  eucalglt  16632  lcmneg  16650  mulgcddvds  16702  qredeu  16705  prmdvdsbc  16773  prmdiveq  16833  odzdvds  16842  pythagtriplem3  16865  pythagtriplem6  16868  pythagtriplem7  16869  iserodd  16882  pclem  16885  pcpremul  16890  pcidlem  16919  pcgcd1  16924  pc2dvds  16926  pcz  16928  pcprmpw2  16929  fldivp1  16944  pcfaclem  16945  pcfac  16946  pcbc  16947  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  4sqlem11  17002  4sqlem12  17003  4sqlem14  17005  vdwlem11  17038  vdwlem12  17039  ramlb  17066  0ram  17067  ram0  17069  ramub1lem2  17074  ramcl  17076  psgnunilem2  19537  odmodnn0  19582  mndodconglem  19583  mndodcong  19584  oddvds  19589  odhash3  19618  gexdvds  19626  sylow1lem1  19640  sylow1lem5  19644  pgpfi  19647  pgpssslw  19656  efgsfo  19781  efgredlemd  19786  efgredlem  19789  efgred  19790  lt6abl  19937  telgsums  20035  pgpfaclem2  20126  srgbinomlem3  20255  zringlpirlem3  21498  psrbaglesupp  21965  psrbagcon  21968  psrbagleadd1  21971  mplmonmul  22077  psdmul  22193  coe1tmmul2  22300  coe1tmmul2fv  22302  coe1pwmulfv  22304  gsummoncoe1  22333  fvmptnn04if  22876  fvmptnn04ifc  22879  fvmptnn04ifd  22880  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  lebnumii  25017  dyadmaxlem  25651  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mdegmullem  26137  coe1mul3  26158  coe1mul4  26159  deg1sublt  26169  deg1mul2  26173  deg1tmle  26177  deg1tm  26178  ply1divmo  26195  ply1divex  26196  deg1submon1p  26212  dvdsq1p  26222  fta1glem2  26228  fta1blem  26230  plyco0  26251  plyeq0lem  26269  plypf1  26271  plyaddlem1  26272  coeeulem  26283  dgrub  26293  dgrlb  26295  dgreq  26303  coeaddlem  26308  coemullem  26309  coemulhi  26313  dgrlt  26326  dgradd2  26328  dgrmul  26330  dgrcolem2  26334  dgrco  26335  plydivlem3  26355  plydivlem4  26356  plydivex  26357  plydiveu  26358  fta1lem  26367  quotcan  26369  vieta1lem2  26371  radcnvlem1  26474  dvradcnv  26482  leibpi  27003  log2tlbnd  27006  birthdaylem2  27013  birthdaylem3  27014  fsumharmonic  27073  dmlogdmgm  27085  basellem3  27144  basellem5  27146  issqf  27197  ppip1le  27222  ppiltx  27238  mumullem2  27241  sgmppw  27259  ppiub  27266  chtublem  27273  chpub  27282  dchrabs  27322  bcmono  27339  bcmax  27340  bcp1ctr  27341  bclbnd  27342  bposlem5  27350  gausslemma2dlem0h  27425  gausslemma2dlem4  27431  gausslemma2dlem6  27434  lgseisenlem1  27437  2lgsoddprmlem2  27471  2sqlem7  27486  2sqlem8  27488  2sq2  27495  2sqmod  27498  chebbnd1lem1  27531  chtppilimlem1  27535  dchrisum0re  27575  mulogsumlem  27593  selberg2lem  27612  pntrlog2bndlem4  27642  pntlemr  27664  pntlemj  27665  pnt  27676  ostth2lem3  27697  vtxdgfival  29505  vtxdfiun  29518  vtxdginducedm1fi  29580  crctcsh  29857  wwlksnred  29925  wwlksnextproplem2  29943  rusgrnumwwlks  30007  eupth2lems  30270  eucrct2eupth  30277  numclwlk1lem1  30401  numclwwlk5  30420  numclwwlk6  30422  friendshipgt3  30430  nnmulge  32752  nndiffz1  32791  fzo0opth  32810  suppssnn0  32812  ccatdmss  32916  pfxlsw2ccat  32917  wrdt2ind  32920  cycpmrn  33136  cyc3conja  33150  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  ply1unit  33565  ply1dg3rt0irred  33572  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1degltdimlem  33635  ply1degltdim  33636  minplyirredlem  33703  irredminply  33707  nexple  33973  oddpwdc  34319  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemb  34333  coinfliplem  34443  signsplypnf  34527  signslema  34539  signstfvc  34551  signstfveq0  34554  fsum2dsub  34584  reprlt  34596  reprgt  34598  reprinfz1  34599  breprexplemc  34609  lpadmax  34659  lpadright  34661  usgrgt2cycl  35098  acycgr1v  35117  erdszelem8  35166  erdsze2lem2  35172  cvmliftlem7  35259  snmlff  35297  bcprod  35700  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  rrnequiv  37795  lcmineqlem17  42002  lcmineqlem21  42006  3lexlogpow5ineq5  42017  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p3  42035  aks4d1p7d1  42039  aks6d1c1  42073  aks6d1c3  42080  aks6d1c2lem4  42084  hashnexinj  42085  aks6d1c2  42087  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c5  42096  2np3bcnp1  42101  2ap1caineq  42102  sticksstones6  42108  sticksstones7  42109  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c6lem4  42130  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  unitscyglem1  42152  unitscyglem4  42155  aks5lem8  42158  frlmvscadiccat  42461  fltnltalem  42617  eldioph2lem1  42716  pell1qrge1  42826  rmxypos  42904  ltrmynn0  42905  ltrmxnn0  42906  lermxnn0  42907  jm2.24nn  42916  jm2.24  42920  jm2.19  42950  jm2.26lem3  42958  jm2.27c  42964  hbt  43087  dgraa0p  43106  binomcxplemnn0  44318  fsumnncl  45493  mccllem  45518  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnmul  45864  dvnprodlem2  45868  stoweidlem17  45938  stoweidlem24  45945  wallispilem5  45990  stirlinglem15  46009  fourierdlem48  46075  fourierdlem83  46110  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  elaa2lem  46154  etransclem10  46165  etransclem19  46174  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem27  46182  etransclem32  46187  etransclem35  46190  etransclem44  46199  etransclem45  46200  etransclem46  46201  etransclem47  46202  etransclem48  46203  etransc  46204  rrndistlt  46211  fmtnoge3  47404  sqrtpwpw2p  47412  fmtnosqrt  47413  flsqrt  47467  lighneallem4a  47482  ssnn0ssfz  48074  pgrple2abl  48090  nn0eo  48262  fllog2  48302  itcovalt2lem2lem1  48407  aacllem  48895