Theorem nn0cn 9340

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

Syntax hints:   -> wi 4   e. wcel 2178   CCcc 7958   NN0cn0 9330

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-int 3900  df-inn 9072  df-n0 9331

This theorem is referenced by:  nn0nnaddcl  9361  elnn0nn  9372  difgtsumgt  9477  nn0n0n1ge2  9478  uzaddcl  9742  fzctr  10290  nn0split  10293  elfzoext  10358  zpnn0elfzo1  10374  ubmelm1fzo  10392  subfzo0  10408  modqmuladdnn0  10550  addmodidr  10555  modfzo0difsn  10577  nn0ennn  10615  expadd  10763  expmul  10766  bernneq  10842  bernneq2  10843  faclbnd  10923  faclbnd6  10926  bccmpl  10936  bcn0  10937  bcnn  10939  bcnp1n  10941  bcn2  10946  bcp1m1  10947  bcpasc  10948  bcn2p1  10952  hashfzo0  11005  hashfz0  11007  ccatws1lenp1bg  11127  swrdfv2  11154  swrdspsleq  11158  swrdlsw  11160  pfxmpt  11171  pfxswrd  11197  wrdind  11213  wrd2ind  11214  pfxccatin12lem4  11217  pfxccatin12lem1  11219  pfxccatin12lem2  11222  pfxccatin12  11224  swrdccat3blem  11230  fisum0diag2  11873  hashiun  11904  binom1dif  11913  bcxmas  11915  geolim  11937  efaddlem  12100  efexp  12108  eftlub  12116  demoivreALT  12200  nn0ob  12334  modremain  12355  mulgcdr  12454  nn0seqcvgd  12478  modprmn0modprm0  12694  coprimeprodsq  12695  coprimeprodsq2  12696  pcexp  12747  dvdsprmpweqle  12775  difsqpwdvds  12776  znnen  12884  ennnfonelemp1  12892  mulgneg2  13607  cnfldmulg  14453  nn0subm  14460  rpcxpmul2  15500  0sgmppw  15580  2lgslem1c  15682  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692