Theorem nn0red 11957

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  ℕ₀cn0 11898

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639  df-n0 11899

This theorem is referenced by:  nn0cnd  11958  nn0readdcl  11962  eluzmn  12251  flmulnn0  13198  quoremz  13224  quoremnn0ALT  13226  modaddmodup  13303  modaddmodlo  13304  expneg  13438  expnbnd  13594  facdiv  13648  faclbnd6  13660  hashdom  13741  hashun2  13745  hashunx  13748  hashfun  13799  hashf1  13816  seqcoll2  13824  hashge2el2dif  13839  hashtpg  13844  wrdlenge2n0  13904  ccatsymb  13936  ccatrn  13943  ccatalpha  13947  ccat2s1fvw  13998  ccat2s1fvwOLD  13999  swrdnd  14016  swrdnd0  14019  pfxnd0  14050  pfxsuffeqwrdeq  14060  swrdccat3blem  14101  cshwidxmod  14165  repswcshw  14174  swrds2  14302  modfsummods  15148  climcnds  15206  geomulcvg  15232  mertenslem1  15240  binomfallfaclem2  15394  binomrisefac  15396  fallfacval4  15397  efcllem  15431  eftlub  15462  ruclem10  15592  oddge22np1  15698  nn0oddm1d2  15736  divalglem5  15748  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  sadcaddlem  15806  sadaddlem  15815  sadasslem  15819  sadeq  15821  smuval2  15831  smupvallem  15832  smueqlem  15839  bezoutlem3  15889  bezoutlem4  15890  gcdzeq  15902  dvdssqlem  15910  nn0seqcvgd  15914  eucalglt  15929  lcmneg  15947  mulgcddvds  15999  qredeu  16002  prmdiveq  16123  odzdvds  16132  pythagtriplem3  16155  pythagtriplem6  16158  pythagtriplem7  16159  iserodd  16172  pclem  16175  pcpremul  16180  pcidlem  16208  pcgcd1  16213  pc2dvds  16215  pcz  16217  pcprmpw2  16218  fldivp1  16233  pcfaclem  16234  pcfac  16235  pcbc  16236  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  4sqlem11  16291  4sqlem12  16292  4sqlem14  16294  vdwlem11  16327  vdwlem12  16328  ramlb  16355  0ram  16356  ram0  16358  ramub1lem2  16363  ramcl  16365  psgnunilem2  18623  odmodnn0  18668  mndodconglem  18669  mndodcong  18670  oddvds  18675  odhash3  18701  gexdvds  18709  sylow1lem1  18723  sylow1lem5  18727  pgpfi  18730  pgpssslw  18739  efgsfo  18865  efgredlemd  18870  efgredlem  18873  efgred  18874  lt6abl  19015  telgsums  19113  pgpfaclem2  19204  srgbinomlem3  19292  psrbaglesupp  20148  mplmonmul  20245  coe1tmmul2  20444  coe1tmmul2fv  20446  coe1pwmulfv  20448  gsummoncoe1  20472  zringlpirlem3  20633  fvmptnn04if  21457  fvmptnn04ifc  21460  fvmptnn04ifd  21461  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  lebnumii  23570  dyadmaxlem  24198  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mdegmullem  24672  coe1mul3  24693  coe1mul4  24694  deg1sublt  24704  deg1mul2  24708  deg1tmle  24711  deg1tm  24712  ply1divmo  24729  ply1divex  24730  deg1submon1p  24746  dvdsq1p  24754  fta1glem2  24760  fta1blem  24762  plyco0  24782  plyeq0lem  24800  plypf1  24802  plyaddlem1  24803  coeeulem  24814  dgrub  24824  dgrlb  24826  dgreq  24834  coeaddlem  24839  coemullem  24840  coemulhi  24844  dgrlt  24856  dgradd2  24858  dgrmul  24860  dgrcolem2  24864  dgrco  24865  plydivlem3  24884  plydivlem4  24885  plydivex  24886  plydiveu  24887  fta1lem  24896  quotcan  24898  vieta1lem2  24900  radcnvlem1  25001  dvradcnv  25009  leibpi  25520  log2tlbnd  25523  birthdaylem2  25530  birthdaylem3  25531  fsumharmonic  25589  dmlogdmgm  25601  basellem3  25660  basellem5  25662  issqf  25713  ppip1le  25738  ppiltx  25754  mumullem2  25757  sgmppw  25773  ppiub  25780  chtublem  25787  chpub  25796  dchrabs  25836  bcmono  25853  bcmax  25854  bcp1ctr  25855  bclbnd  25856  bposlem5  25864  gausslemma2dlem0h  25939  gausslemma2dlem4  25945  gausslemma2dlem6  25948  lgseisenlem1  25951  2lgsoddprmlem2  25985  2sqlem7  26000  2sqlem8  26002  2sq2  26009  2sqmod  26012  chebbnd1lem1  26045  chtppilimlem1  26049  dchrisum0re  26089  mulogsumlem  26107  selberg2lem  26126  pntrlog2bndlem4  26156  pntlemr  26178  pntlemj  26179  pnt  26190  ostth2lem3  26211  vtxdgfival  27251  vtxdfiun  27264  vtxdginducedm1fi  27326  crctcsh  27602  wwlksnred  27670  wwlksnextproplem2  27689  rusgrnumwwlks  27753  eupth2lems  28017  eucrct2eupth  28024  numclwlk1lem1  28148  numclwwlk5  28167  numclwwlk6  28169  friendshipgt3  28177  nnmulge  30474  nndiffz1  30509  prmdvdsbc  30532  pfxlsw2ccat  30626  wrdt2ind  30627  cycpmrn  30785  cyc3conja  30799  nexple  31268  oddpwdc  31612  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemb  31626  coinfliplem  31736  signsplypnf  31820  signslema  31832  signstfvc  31844  signstfveq0  31847  fsum2dsub  31878  reprlt  31890  reprgt  31892  reprinfz1  31893  breprexplemc  31903  lpadmax  31953  lpadright  31955  usgrgt2cycl  32377  acycgr1v  32396  erdszelem8  32445  erdsze2lem2  32451  cvmliftlem7  32538  snmlff  32576  bcprod  32970  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  rrnequiv  35128  frlmvscadiccat  39194  fltnltalem  39323  eldioph2lem1  39406  pell1qrge1  39516  rmxypos  39593  ltrmynn0  39594  ltrmxnn0  39595  lermxnn0  39596  jm2.24nn  39605  jm2.24  39609  jm2.19  39639  jm2.26lem3  39647  jm2.27c  39653  hbt  39779  dgraa0p  39798  binomcxplemnn0  40730  fsumnncl  41901  mccllem  41927  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnxpaek  42276  dvnmul  42277  dvnprodlem2  42281  stoweidlem17  42351  stoweidlem24  42358  wallispilem5  42403  stirlinglem15  42422  fourierdlem48  42488  fourierdlem83  42523  fourierdlem103  42543  fourierdlem104  42544  sqwvfoura  42562  elaa2lem  42567  etransclem10  42578  etransclem19  42587  etransclem20  42588  etransclem21  42589  etransclem22  42590  etransclem23  42591  etransclem24  42592  etransclem27  42595  etransclem32  42600  etransclem35  42603  etransclem44  42612  etransclem45  42613  etransclem46  42614  etransclem47  42615  etransclem48  42616  etransc  42617  rrndistlt  42624  fmtnoge3  43741  sqrtpwpw2p  43749  fmtnosqrt  43750  flsqrt  43805  lighneallem4a  43822  ssnn0ssfz  44446  pgrple2abl  44462  nn0eo  44637  fllog2  44677  aacllem  44951