Theorem nn0cn 9379

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   NN0cn0 9369

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 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

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 9111  df-n0 9370

This theorem is referenced by:  nn0nnaddcl  9400  elnn0nn  9411  difgtsumgt  9516  nn0n0n1ge2  9517  uzaddcl  9781  fzctr  10329  nn0split  10332  elfzoext  10398  zpnn0elfzo1  10414  ubmelm1fzo  10432  subfzo0  10448  modqmuladdnn0  10590  addmodidr  10595  modfzo0difsn  10617  nn0ennn  10655  expadd  10803  expmul  10806  bernneq  10882  bernneq2  10883  faclbnd  10963  faclbnd6  10966  bccmpl  10976  bcn0  10977  bcnn  10979  bcnp1n  10981  bcn2  10986  bcp1m1  10987  bcpasc  10988  bcn2p1  10992  hashfzo0  11045  hashfz0  11047  ccatws1lenp1bg  11168  swrdfv2  11195  swrdspsleq  11199  swrdlsw  11201  pfxmpt  11212  pfxswrd  11238  wrdind  11254  wrd2ind  11255  pfxccatin12lem4  11258  pfxccatin12lem1  11260  pfxccatin12lem2  11263  pfxccatin12  11265  swrdccat3blem  11271  fisum0diag2  11958  hashiun  11989  binom1dif  11998  bcxmas  12000  geolim  12022  efaddlem  12185  efexp  12193  eftlub  12201  demoivreALT  12285  nn0ob  12419  modremain  12440  mulgcdr  12539  nn0seqcvgd  12563  modprmn0modprm0  12779  coprimeprodsq  12780  coprimeprodsq2  12781  pcexp  12832  dvdsprmpweqle  12860  difsqpwdvds  12861  znnen  12969  ennnfonelemp1  12977  mulgneg2  13693  cnfldmulg  14540  nn0subm  14547  rpcxpmul2  15587  0sgmppw  15667  2lgslem1c  15769  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  wlklenvclwlk  16084