Theorem nn0cn 9412

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0nnaddcl  9433  elnn0nn  9444  difgtsumgt  9549  nn0n0n1ge2  9550  uzaddcl  9820  fzctr  10368  nn0split  10371  elfzoext  10438  zpnn0elfzo1  10454  ubmelm1fzo  10472  subfzo0  10489  modqmuladdnn0  10631  addmodidr  10636  modfzo0difsn  10658  nn0ennn  10696  expadd  10844  expmul  10847  bernneq  10923  bernneq2  10924  faclbnd  11004  faclbnd6  11007  bccmpl  11017  bcn0  11018  bcnn  11020  bcnp1n  11022  bcn2  11027  bcp1m1  11028  bcpasc  11029  bcn2p1  11033  hashfzo0  11088  hashfz0  11090  ccatalpha  11194  ccatws1lenp1bg  11216  ccatw2s1leng  11219  swrdfv2  11248  swrdspsleq  11252  swrdlsw  11254  pfxmpt  11265  pfxswrd  11291  wrdind  11307  wrd2ind  11308  pfxccatin12lem4  11311  pfxccatin12lem1  11313  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat3blem  11324  fisum0diag2  12026  hashiun  12057  binom1dif  12066  bcxmas  12068  geolim  12090  efaddlem  12253  efexp  12261  eftlub  12269  demoivreALT  12353  nn0ob  12487  modremain  12508  mulgcdr  12607  nn0seqcvgd  12631  modprmn0modprm0  12847  coprimeprodsq  12848  coprimeprodsq2  12849  pcexp  12900  dvdsprmpweqle  12928  difsqpwdvds  12929  znnen  13037  ennnfonelemp1  13045  mulgneg2  13761  cnfldmulg  14609  nn0subm  14616  rpcxpmul2  15656  0sgmppw  15736  2lgslem1c  15838  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  wlklenvclwlk  16243  clwwlknonex2lem2  16308