Theorem nn0cn 9523

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   NN0cn0 9513

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 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-int 3955  df-inn 9255  df-n0 9514

This theorem is referenced by:  nn0nnaddcl  9544  elnn0nn  9555  difgtsumgt  9664  nn0n0n1ge2  9665  uzaddcl  9936  fzctr  10489  nn0split  10492  elfzoext  10559  zpnn0elfzo1  10575  ubmelm1fzo  10593  subfzo0  10610  modqmuladdnn0  10754  addmodidr  10759  modfzo0difsn  10781  nn0ennn  10819  expadd  10967  expmul  10970  bernneq  11047  bernneq2  11048  faclbnd  11128  faclbnd6  11131  bccmpl  11141  bcn0  11142  bcnn  11144  bcnp1n  11146  bcn2  11151  bcp1m1  11152  bcpasc  11153  bcn2p1  11158  hashfzo0  11213  hashfz0  11215  ccatalpha  11326  ccatws1lenp1bg  11348  ccatw2s1leng  11351  swrdfv2  11380  swrdspsleq  11384  swrdlsw  11386  pfxmpt  11397  pfxswrd  11423  wrdind  11439  wrd2ind  11440  pfxccatin12lem4  11443  pfxccatin12lem1  11445  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccat3blem  11456  fisum0diag2  12158  hashiun  12189  binom1dif  12198  bcxmas  12200  geolim  12222  efaddlem  12385  efexp  12393  eftlub  12401  demoivreALT  12485  nn0ob  12619  modremain  12640  mulgcdr  12739  nn0seqcvgd  12763  modprmn0modprm0  12979  coprimeprodsq  12980  coprimeprodsq2  12981  pcexp  13032  dvdsprmpweqle  13060  difsqpwdvds  13061  znnen  13233  ennnfonelemp1  13241  mulgneg2  13909  cnfldmulg  14850  nn0subm  14857  psrbagconf1o  14954  rpcxpmul2  15904  0sgmppw  15987  2lgslem1c  16089  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  wlklenvclwlk  16494  clwwlknonex2lem2  16559