Theorem nn0cn 9250

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

Syntax hints:   -> wi 4   e. wcel 2164   CCcc 7870   NN0cn0 9240

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-int 3871  df-inn 8983  df-n0 9241

This theorem is referenced by:  nn0nnaddcl  9271  elnn0nn  9282  difgtsumgt  9386  nn0n0n1ge2  9387  uzaddcl  9651  fzctr  10199  nn0split  10202  zpnn0elfzo1  10275  ubmelm1fzo  10293  subfzo0  10309  modqmuladdnn0  10439  addmodidr  10444  modfzo0difsn  10466  nn0ennn  10504  expadd  10652  expmul  10655  bernneq  10731  bernneq2  10732  faclbnd  10812  faclbnd6  10815  bccmpl  10825  bcn0  10826  bcnn  10828  bcnp1n  10830  bcn2  10835  bcp1m1  10836  bcpasc  10837  bcn2p1  10841  hashfzo0  10894  hashfz0  10896  fisum0diag2  11590  hashiun  11621  binom1dif  11630  bcxmas  11632  geolim  11654  efaddlem  11817  efexp  11825  eftlub  11833  demoivreALT  11917  nn0ob  12049  modremain  12070  mulgcdr  12155  nn0seqcvgd  12179  modprmn0modprm0  12394  coprimeprodsq  12395  coprimeprodsq2  12396  pcexp  12447  dvdsprmpweqle  12475  difsqpwdvds  12476  znnen  12555  ennnfonelemp1  12563  mulgneg2  13226  cnfldmulg  14064  nn0subm  14071