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

Theorem nn0cn 10868
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 10863 . 2  |-  NN0  C_  CC
21sseli 3457 1  |-  ( A  e.  NN0  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   CCcc 9526   NN0cn0 10858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-i2m1 9596  ax-1ne0 9597  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-om 6698  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-nn 10599  df-n0 10859
This theorem is referenced by:  nn0nnaddcl  10890  elnn0nn  10901  nn0sub  10909  nn0n0n1ge2  10921  uzaddcl  11204  fzctr  11890  nn0split  11893  elfzoext  11957  zpnn0elfzo1  11973  ubmelm1fzo  11993  quoremnn0ALT  12070  nn0ennn  12178  expadd  12300  expmul  12303  bernneq  12384  bernneq2  12385  faclbnd  12461  faclbnd4lem3  12466  faclbnd4lem4  12467  faclbnd6  12470  bccmpl  12480  bcn0  12481  bcnn  12483  bcnp1n  12485  bcn2  12490  bcp1m1  12491  bcpasc  12492  bcn2p1  12496  hashfzo0  12586  hashfz0  12588  hashxplem  12589  brfi1indlem  12629  ccatw2s1len  12732  addlenrevswrd  12767  swrdfv2  12776  swrdspsleq  12779  swrdlsw  12782  swrd0swrd  12791  ccats1swrdeq  12799  wrdind  12807  wrd2ind  12808  swrdccatin12lem1  12814  swrdccatin12lem2b  12816  swrdccatin12lem2  12819  swrdccatin12  12821  swrdccat3blem  12825  repswswrd  12861  repswrevw  12863  2cshw  12886  2cshwcshw  12898  cshwcshid  12900  swrds2  12988  swrd2lsw  12995  iseraltlem2  13716  fsum0diag2  13811  hashiun  13849  ackbijnn  13853  binom1dif  13858  bcxmas  13860  geolim  13893  geomulcvg  13899  risefacval2  14030  fallfacval2  14031  risefaccl  14035  fallfaccl  14036  fallrisefac  14045  risefacp1  14049  fallfacp1  14050  fallfacfac  14065  bpolysum  14073  fsumkthpow  14076  bpoly4  14079  fsumcube  14080  efaddlem  14114  efexp  14122  eftlub  14130  demoivreALT  14222  divalglem4  14341  mulgcdr  14476  nn0seqcvgd  14489  modprmn0modprm0  14710  coprimeprodsq  14711  coprimeprodsq2  14712  pcexp  14761  ramub1lem1  14936  prmop1  14948  mulgneg2  16729  mndodcongi  17127  oddvdsnn0  17128  sylow1lem1  17178  efgsrel  17312  srgbinomlem4  17704  psrbagconf1o  18526  psrass1lem  18529  psrlidm  18555  psrass1  18557  psrcom  18561  mplsubrglem  18591  mplmonmul  18616  psropprmul  18759  coe1sclmul  18803  coe1sclmul2  18805  cnfldmulg  18928  nn0subm  18951  nn0srg  18964  dvnadd  22757  ply1divex  22959  elqaalem2  23138  geolim3  23157  dvradcnv  23238  pserdv2  23247  logtayllem  23466  logtayl  23467  cxpmul2  23496  atantayl3  23727  leibpilem2  23729  leibpi  23730  log2cnv  23732  dmgmaddn0  23810  chpp1  23942  0sgmppw  23986  logexprlim  24013  dchrhash  24059  bcctr  24063  bcmono  24065  bcmax  24066  bcp1ctr  24067  dchrisumlem1  24187  ostth2lem2  24332  cusgrasizeinds  25046  wlklenvm1  25102  fargshiftfo  25208  wwlknimp  25257  wlkiswwlk1  25260  wlklniswwlkn2  25270  wwlknred  25293  wwlknext  25294  wwlknredwwlkn  25296  wwlkextwrd  25298  wwlkextinj  25300  wwlkextproplem2  25312  wwlkextproplem3  25313  clwlkisclwwlklem2a1  25349  clwlkisclwwlklem2a4  25354  clwlkisclwwlklem2a  25355  clwlkisclwwlklem1  25357  clwlkisclwwlklem0  25358  wwlkext2clwwlk  25373  wlklenvclwlk  25409  rusgranumwlks  25526  rusgranumwlk  25527  usgreghash2spot  25639  frgregordn0  25640  extwwlkfablem2  25648  numclwwlkovf2ex  25656  numclwwlk1  25668  numclwwlk3  25679  numclwwlk7  25684  gxnn0mul  25847  ipasslem1  26314  ipasslem2  26315  archirngz  28341  subfacval2  29695  bccolsum  30159  faclimlem1  30163  poimirlem28  31672  heiborlem4  31850  heiborlem6  31852  pell14qrgt0  35415  pell14qrdich  35425  pell1qrge1  35426  2nn0ind  35503  jm2.17a  35520  jm2.18  35553  jm2.19lem3  35556  proot1ex  35781  bcc0  36330  dvradcnv2  36337  binomcxplemrat  36340  binomcxplemnotnn0  36346  fperiodmullem  37134  m1expevenOLD  37246  stoweidlem10  37443  stoweidlem17  37450  stoweidlem26  37459  stirlinglem5  37513  stirlinglem7  37515  etransclem23  37693  nn0onn0exALTV  38230  nn0enn0exALTV  38231  pfxmpt  38331  addlenrevpfx  38341  pfxccatin12lem1  38367  pfxccatin12lem2  38368  pfxccatin12  38369  subsubelfzo0  38424  ply1mulgsumlem1  38951  ply1mulgsumlem2  38952  nn0ob  39104  nn0onn0ex  39105  nn0enn0ex  39106  fllog2  39153  dignn0fr  39186  digexp  39192  0dig2nn0e  39197  0dig2nn0o  39198  dignn0ehalf  39202  nn0mulfsum  39209  nn0mullong  39210  dpfrac1  39266
  Copyright terms: Public domain W3C validator