MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0cn Structured version   Unicode version

Theorem nn0cn 10801
Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0cn  |-  ( A  e.  NN0  ->  A  e.  CC )

Proof of Theorem nn0cn
StepHypRef Expression
1 nn0sscn 10796 . 2  |-  NN0  C_  CC
21sseli 3485 1  |-  ( A  e.  NN0  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   CCcc 9479   NN0cn0 10791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-om 6674  df-recs 7034  df-rdg 7068  df-nn 10532  df-n0 10792
This theorem is referenced by:  nn0nnaddcl  10823  elnn0nn  10834  nn0sub  10842  nn0n0n1ge2  10855  uzaddcl  11138  fzctr  11791  nn0split  11794  elfzoext  11854  zpnn0elfzo1  11870  ubmelm1fzo  11889  quoremnn0ALT  11966  addmodid  12018  nn0ennn  12071  expadd  12190  expmul  12193  bernneq  12274  bernneq2  12275  faclbnd  12350  faclbnd4lem3  12355  faclbnd4lem4  12356  faclbnd6  12359  bccmpl  12369  bcn0  12370  bcnn  12372  bcnp1n  12374  bcn2  12379  bcp1m1  12380  bcpasc  12381  bcn2p1  12385  hashfzo0  12472  hashfz0  12474  hashxplem  12475  brfi1indlem  12515  ccatw2s1len  12618  addlenrevswrd  12653  swrdfv2  12662  swrdspsleq  12665  swrdlsw  12668  swrd0swrd  12677  ccats1swrdeq  12685  wrdind  12693  wrd2ind  12694  swrdccatin12lem1  12700  swrdccatin12lem2b  12702  swrdccatin12lem2  12705  swrdccatin12  12707  swrdccat3blem  12711  repswswrd  12747  repswrevw  12749  2cshw  12772  2cshwcshw  12784  cshwcshid  12786  swrds2  12874  swrd2lsw  12881  iseraltlem2  13587  fsum0diag2  13680  hashiun  13718  ackbijnn  13722  binom1dif  13727  bcxmas  13729  geolim  13761  geomulcvg  13767  efaddlem  13910  efexp  13918  eftlub  13926  demoivreALT  14018  divalglem4  14138  mulgcdr  14270  nn0seqcvgd  14283  modprmn0modprm0  14416  coprimeprodsq  14417  coprimeprodsq2  14418  pcexp  14467  ramub1lem1  14628  mulgneg2  16368  mndodcongi  16766  oddvdsnn0  16767  sylow1lem1  16817  efgsrel  16951  srgbinomlem4  17389  psrbagconf1o  18221  psrass1lem  18224  psrlidm  18251  psrlidmOLD  18252  psrass1  18255  psrcom  18259  mplsubrglem  18295  mplsubrglemOLD  18296  mplmonmul  18321  psropprmul  18474  coe1sclmul  18518  coe1sclmul2  18520  cnfldmulg  18645  nn0subm  18668  nn0srg  18681  dvnadd  22498  ply1divex  22703  elqaalem2  22882  geolim3  22901  dvradcnv  22982  pserdv2  22991  logtayllem  23208  logtayl  23209  cxpmul2  23238  atantayl3  23467  leibpilem2  23469  leibpi  23470  log2cnv  23472  chpp1  23627  0sgmppw  23671  logexprlim  23698  dchrhash  23744  bcctr  23748  bcmono  23750  bcmax  23751  bcp1ctr  23752  dchrisumlem1  23872  ostth2lem2  24017  cusgrasizeinds  24678  wlklenvm1  24734  fargshiftfo  24840  wwlknimp  24889  wlkiswwlk1  24892  wlklniswwlkn2  24902  wwlknred  24925  wwlknext  24926  wwlknredwwlkn  24928  wwlkextwrd  24930  wwlkextinj  24932  wwlkextproplem2  24944  wwlkextproplem3  24945  clwlkisclwwlklem2a1  24981  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem2a  24987  clwlkisclwwlklem1  24989  clwlkisclwwlklem0  24990  wwlkext2clwwlk  25005  wlklenvclwlk  25041  rusgranumwlks  25158  rusgranumwlk  25159  usgreghash2spot  25271  frgregordn0  25272  extwwlkfablem2  25280  numclwwlkovf2ex  25288  numclwwlk1  25300  numclwwlk3  25311  numclwwlk7  25316  gxnn0mul  25477  ipasslem1  25944  ipasslem2  25945  archirngz  27967  dmgmaddn0  28829  subfacval2  28895  risefacval2  29373  fallfacval2  29374  risefaccl  29378  fallfaccl  29379  fallrisefac  29388  risefacp1  29392  fallfacp1  29393  fallfacfac  29408  faclimlem1  29409  bpolysum  30043  fsumkthpow  30046  bpoly4  30049  fsumcube  30050  heiborlem4  30550  heiborlem6  30552  pell14qrgt0  31034  pell14qrdich  31044  pell1qrge1  31045  2nn0ind  31120  jm2.17a  31137  jm2.18  31169  jm2.19lem3  31172  proot1ex  31402  bcc0  31486  dvradcnv2  31493  binomcxplemrat  31496  binomcxplemnotnn0  31502  fperiodmullem  31742  m1expeven  31824  stoweidlem10  32031  stoweidlem17  32038  stoweidlem26  32047  stirlinglem5  32099  stirlinglem7  32101  etransclem23  32279  nn0onn0exALTV  32604  nn0enn0exALTV  32605  pfxmpt  32615  addlenrevpfx  32625  pfxccatin12lem1  32651  pfxccatin12lem2  32652  pfxccatin12  32653  subsubelfzo0  32712  ply1mulgsumlem1  33240  ply1mulgsumlem2  33241  nn0ob  33394  nn0onn0ex  33395  nn0enn0ex  33396  fllog2  33443  dignn0fr  33476  digexp  33482  0dig2nn0e  33487  0dig2nn0o  33488  dignn0ehalf  33492  nn0mulfsum  33499  nn0mullong  33500  dpfrac1  33556
  Copyright terms: Public domain W3C validator