Theorem nn0cn 9390

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8008   NN0cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9122  df-n0 9381

This theorem is referenced by:  nn0nnaddcl  9411  elnn0nn  9422  difgtsumgt  9527  nn0n0n1ge2  9528  uzaddcl  9793  fzctr  10341  nn0split  10344  elfzoext  10410  zpnn0elfzo1  10426  ubmelm1fzo  10444  subfzo0  10460  modqmuladdnn0  10602  addmodidr  10607  modfzo0difsn  10629  nn0ennn  10667  expadd  10815  expmul  10818  bernneq  10894  bernneq2  10895  faclbnd  10975  faclbnd6  10978  bccmpl  10988  bcn0  10989  bcnn  10991  bcnp1n  10993  bcn2  10998  bcp1m1  10999  bcpasc  11000  bcn2p1  11004  hashfzo0  11058  hashfz0  11060  ccatalpha  11161  ccatws1lenp1bg  11183  swrdfv2  11211  swrdspsleq  11215  swrdlsw  11217  pfxmpt  11228  pfxswrd  11254  wrdind  11270  wrd2ind  11271  pfxccatin12lem4  11274  pfxccatin12lem1  11276  pfxccatin12lem2  11279  pfxccatin12  11281  swrdccat3blem  11287  fisum0diag2  11974  hashiun  12005  binom1dif  12014  bcxmas  12016  geolim  12038  efaddlem  12201  efexp  12209  eftlub  12217  demoivreALT  12301  nn0ob  12435  modremain  12456  mulgcdr  12555  nn0seqcvgd  12579  modprmn0modprm0  12795  coprimeprodsq  12796  coprimeprodsq2  12797  pcexp  12848  dvdsprmpweqle  12876  difsqpwdvds  12877  znnen  12985  ennnfonelemp1  12993  mulgneg2  13709  cnfldmulg  14556  nn0subm  14563  rpcxpmul2  15603  0sgmppw  15683  2lgslem1c  15785  2lgslem3a  15788  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  wlklenvclwlk  16119