Theorem nn0cn 9138

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

Syntax hints:   -> wi 4   e. wcel 2141   CCcc 7765   NN0cn0 9128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105  ax-cnex 7858  ax-resscn 7859  ax-1re 7861  ax-addrcl 7864  ax-rnegex 7876

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3587  df-int 3830  df-inn 8872  df-n0 9129

This theorem is referenced by:  nn0nnaddcl  9159  elnn0nn  9170  difgtsumgt  9274  nn0n0n1ge2  9275  uzaddcl  9538  fzctr  10082  nn0split  10085  zpnn0elfzo1  10157  ubmelm1fzo  10175  subfzo0  10191  modqmuladdnn0  10317  addmodidr  10322  modfzo0difsn  10344  nn0ennn  10382  expadd  10511  expmul  10514  bernneq  10589  bernneq2  10590  faclbnd  10668  faclbnd6  10671  bccmpl  10681  bcn0  10682  bcnn  10684  bcnp1n  10686  bcn2  10691  bcp1m1  10692  bcpasc  10693  bcn2p1  10697  hashfzo0  10751  hashfz0  10753  fisum0diag2  11403  hashiun  11434  binom1dif  11443  bcxmas  11445  geolim  11467  efaddlem  11630  efexp  11638  eftlub  11646  demoivreALT  11729  nn0ob  11860  modremain  11881  mulgcdr  11966  nn0seqcvgd  11988  modprmn0modprm0  12203  coprimeprodsq  12204  coprimeprodsq2  12205  pcexp  12256  dvdsprmpweqle  12283  difsqpwdvds  12284  znnen  12346  ennnfonelemp1  12354