Theorem nn0cn 9584

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

Step	Hyp	Ref	Expression
1		nn0sscn 9579	. 2 |- NN0 C_ CC
2	1	sseli 3244	1 |- ( A e. NN0 -> A e. CC )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8183   NN0cn0 9574

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9314  df-n0 9575

This theorem is used by:  nn0nnaddcl  9605  elnn0nn  9616  difgtsumgt  9723  nn0n0n1ge2  9724  uzaddcl  10001  fzctr  10556  nn0split  10559  elfzoext  10626  zpnn0elfzo1  10642  ubmelm1fzo  10660  subfzo0  10677  modqmuladdnn0  10825  addmodidr  10830  modfzo0difsn  10852  nn0ennn  10890  expadd  11038  expmul  11041  bernneq  11118  bernneq2  11119  faclbnd  11200  faclbnd6  11203  bccmpl  11213  bcn0  11214  bcnn  11216  bcnp1n  11218  bcn2  11223  bcp1m1  11224  bcpasc  11225  bcn2p1  11230  hashfzo0  11285  hashfz0  11287  ccatalpha  11402  ccatws1lenp1bg  11424  ccatw2s1leng  11427  swrdfv2  11456  swrdspsleq  11460  swrdlsw  11462  pfxmpt  11473  pfxswrd  11499  wrdind  11515  wrd2ind  11516  pfxccatin12lem4  11519  pfxccatin12lem1  11521  pfxccatin12lem2  11524  pfxccatin12  11526  swrdccat3blem  11532  fisum0diag2  12238  hashiun  12269  binom1dif  12278  bcxmas  12280  geolim  12302  efaddlem  12465  efexp  12473  eftlub  12481  demoivreALT  12565  nn0ob  12699  modremain  12720  mulgcdr  12819  nn0seqcvgd  12843  modprmn0modprm0  13063  coprimeprodsq  13064  coprimeprodsq2  13065  pcexp  13116  dvdsprmpweqle  13144  difsqpwdvds  13145  znnen  13346  ennnfonelemp1  13354  mulgneg2  14017  cnfldmulg  15021  nn0subm  15028  psrbagconf1o  15177  psrass1filem  15186  psrlidmfi  15208  psrass1fi  15210  rpcxpmul2  16163  0sgmppw  16304  bcctr  16319  bcmono  16321  bcmax  16322  bcp1ctr  16323  2lgslem1c  16431  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  wlklenvclwlk  16836  clwwlknonex2lem2  16901