Theorem nn0cn 9471

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 9466	. 2 |- NN0 C_ CC
2	1	sseli 3224	1 |- ( A e. NN0 -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8090   NN0cn0 9461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8183  ax-resscn 8184  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9203  df-n0 9462

This theorem is referenced by:  nn0nnaddcl  9492  elnn0nn  9503  difgtsumgt  9610  nn0n0n1ge2  9611  uzaddcl  9881  fzctr  10430  nn0split  10433  elfzoext  10500  zpnn0elfzo1  10516  ubmelm1fzo  10534  subfzo0  10551  modqmuladdnn0  10693  addmodidr  10698  modfzo0difsn  10720  nn0ennn  10758  expadd  10906  expmul  10909  bernneq  10985  bernneq2  10986  faclbnd  11066  faclbnd6  11069  bccmpl  11079  bcn0  11080  bcnn  11082  bcnp1n  11084  bcn2  11089  bcp1m1  11090  bcpasc  11091  bcn2p1  11095  hashfzo0  11150  hashfz0  11152  ccatalpha  11256  ccatws1lenp1bg  11278  ccatw2s1leng  11281  swrdfv2  11310  swrdspsleq  11314  swrdlsw  11316  pfxmpt  11327  pfxswrd  11353  wrdind  11369  wrd2ind  11370  pfxccatin12lem4  11373  pfxccatin12lem1  11375  pfxccatin12lem2  11378  pfxccatin12  11380  swrdccat3blem  11386  fisum0diag2  12088  hashiun  12119  binom1dif  12128  bcxmas  12130  geolim  12152  efaddlem  12315  efexp  12323  eftlub  12331  demoivreALT  12415  nn0ob  12549  modremain  12570  mulgcdr  12669  nn0seqcvgd  12693  modprmn0modprm0  12909  coprimeprodsq  12910  coprimeprodsq2  12911  pcexp  12962  dvdsprmpweqle  12990  difsqpwdvds  12991  znnen  13099  ennnfonelemp1  13107  mulgneg2  13823  cnfldmulg  14672  nn0subm  14679  psrbagconf1o  14774  rpcxpmul2  15724  0sgmppw  15807  2lgslem1c  15909  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  wlklenvclwlk  16314  clwwlknonex2lem2  16379