Theorem nn0cn 9573

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   NN0cn0 9563

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9305  df-n0 9564

This theorem is used by:  nn0nnaddcl  9594  elnn0nn  9605  difgtsumgt  9714  nn0n0n1ge2  9715  uzaddcl  9986  fzctr  10540  nn0split  10543  elfzoext  10610  zpnn0elfzo1  10626  ubmelm1fzo  10644  subfzo0  10661  modqmuladdnn0  10805  addmodidr  10810  modfzo0difsn  10832  nn0ennn  10870  expadd  11018  expmul  11021  bernneq  11098  bernneq2  11099  faclbnd  11179  faclbnd6  11182  bccmpl  11192  bcn0  11193  bcnn  11195  bcnp1n  11197  bcn2  11202  bcp1m1  11203  bcpasc  11204  bcn2p1  11209  hashfzo0  11264  hashfz0  11266  ccatalpha  11381  ccatws1lenp1bg  11403  ccatw2s1leng  11406  swrdfv2  11435  swrdspsleq  11439  swrdlsw  11441  pfxmpt  11452  pfxswrd  11478  wrdind  11494  wrd2ind  11495  pfxccatin12lem4  11498  pfxccatin12lem1  11500  pfxccatin12lem2  11503  pfxccatin12  11505  swrdccat3blem  11511  fisum0diag2  12214  hashiun  12245  binom1dif  12254  bcxmas  12256  geolim  12278  efaddlem  12441  efexp  12449  eftlub  12457  demoivreALT  12541  nn0ob  12675  modremain  12696  mulgcdr  12795  nn0seqcvgd  12819  modprmn0modprm0  13035  coprimeprodsq  13036  coprimeprodsq2  13037  pcexp  13088  dvdsprmpweqle  13116  difsqpwdvds  13117  znnen  13289  ennnfonelemp1  13297  mulgneg2  13959  cnfldmulg  14913  nn0subm  14920  psrbagconf1o  15064  rpcxpmul2  16015  0sgmppw  16107  2lgslem1c  16209  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  wlklenvclwlk  16614  clwwlknonex2lem2  16679