Theorem nn0cn 9307

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024  ax-rnegex 8036

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-int 3886  df-inn 9039  df-n0 9298

This theorem is referenced by:  nn0nnaddcl  9328  elnn0nn  9339  difgtsumgt  9444  nn0n0n1ge2  9445  uzaddcl  9709  fzctr  10257  nn0split  10260  elfzoext  10323  zpnn0elfzo1  10339  ubmelm1fzo  10357  subfzo0  10373  modqmuladdnn0  10515  addmodidr  10520  modfzo0difsn  10542  nn0ennn  10580  expadd  10728  expmul  10731  bernneq  10807  bernneq2  10808  faclbnd  10888  faclbnd6  10891  bccmpl  10901  bcn0  10902  bcnn  10904  bcnp1n  10906  bcn2  10911  bcp1m1  10912  bcpasc  10913  bcn2p1  10917  hashfzo0  10970  hashfz0  10972  ccatws1lenp1bg  11092  swrdfv2  11119  swrdspsleq  11123  swrdlsw  11125  pfxmpt  11134  fisum0diag2  11791  hashiun  11822  binom1dif  11831  bcxmas  11833  geolim  11855  efaddlem  12018  efexp  12026  eftlub  12034  demoivreALT  12118  nn0ob  12252  modremain  12273  mulgcdr  12372  nn0seqcvgd  12396  modprmn0modprm0  12612  coprimeprodsq  12613  coprimeprodsq2  12614  pcexp  12665  dvdsprmpweqle  12693  difsqpwdvds  12694  znnen  12802  ennnfonelemp1  12810  mulgneg2  13525  cnfldmulg  14371  nn0subm  14378  rpcxpmul2  15418  0sgmppw  15498  2lgslem1c  15600  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610