Theorem nn0cn 9203

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

Syntax hints:   -> wi 4   e. wcel 2159   CCcc 7826   NN0cn0 9193

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170  ax-sep 4135  ax-cnex 7919  ax-resscn 7920  ax-1re 7922  ax-addrcl 7925  ax-rnegex 7937

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ral 2472  df-rex 2473  df-v 2753  df-un 3147  df-in 3149  df-ss 3156  df-sn 3612  df-int 3859  df-inn 8937  df-n0 9194

This theorem is referenced by:  nn0nnaddcl  9224  elnn0nn  9235  difgtsumgt  9339  nn0n0n1ge2  9340  uzaddcl  9603  fzctr  10150  nn0split  10153  zpnn0elfzo1  10225  ubmelm1fzo  10243  subfzo0  10259  modqmuladdnn0  10385  addmodidr  10390  modfzo0difsn  10412  nn0ennn  10450  expadd  10579  expmul  10582  bernneq  10658  bernneq2  10659  faclbnd  10738  faclbnd6  10741  bccmpl  10751  bcn0  10752  bcnn  10754  bcnp1n  10756  bcn2  10761  bcp1m1  10762  bcpasc  10763  bcn2p1  10767  hashfzo0  10820  hashfz0  10822  fisum0diag2  11472  hashiun  11503  binom1dif  11512  bcxmas  11514  geolim  11536  efaddlem  11699  efexp  11707  eftlub  11715  demoivreALT  11798  nn0ob  11930  modremain  11951  mulgcdr  12036  nn0seqcvgd  12058  modprmn0modprm0  12273  coprimeprodsq  12274  coprimeprodsq2  12275  pcexp  12326  dvdsprmpweqle  12353  difsqpwdvds  12354  znnen  12416  ennnfonelemp1  12424  mulgneg2  13061  cnfldmulg  13839  nn0subm  13846