Theorem nncn 8114

Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nncn	|- ( A e. NN -> A e. CC )

Proof of Theorem nncn

Step	Hyp	Ref	Expression
1		nnsscn 8111	. 2 |- NN C_ CC
2	1	sseli 2996	1 |- ( A e. NN -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1434   CCcc 7041   NNcn 8106

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-cnex 7129  ax-resscn 7130  ax-1re 7132  ax-addrcl 7135

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-v 2604  df-in 2980  df-ss 2987  df-int 3645  df-inn 8107

This theorem is referenced by:  nn1m1nn  8124  nn1suc  8125  nnaddcl  8126  nnmulcl  8127  nnsub  8144  nndiv  8146  nndivtr  8147  nnnn0addcl  8385  nn0nnaddcl  8386  elnnnn0  8398  nnnegz  8435  zaddcllempos  8469  zaddcllemneg  8471  nnaddm1cl  8493  elz2  8500  zdiv  8516  zdivadd  8517  zdivmul  8518  nneoor  8530  nneo  8531  divfnzn  8787  qmulz  8789  qaddcl  8801  qnegcl  8802  qmulcl  8803  qreccl  8808  nnledivrp  8918  nn0ledivnn  8919  fseq1m1p1  9188  ubmelm1fzo  9312  subfzo0  9328  flqdiv  9403  addmodidr  9455  modfzo0difsn  9477  nn0ennn  9515  expnegap0  9581  expm1t  9601  nnsqcl  9642  nnlesq  9675  facdiv  9762  facndiv  9763  faclbnd  9765  bcn1  9782  bcn2m1  9793  nndivides  10347  modmulconst  10372  dvdsflip  10396  nn0enne  10446  nno  10450  divalgmod  10471  ndvdsadd  10475  modgcd  10526  gcddiv  10552  gcdmultiple  10553  gcdmultiplez  10554  rpmulgcd  10559  rplpwr  10560  sqgcd  10562  lcmgcdlem  10603  qredeq  10622  qredeu  10623  divgcdcoprm0  10627  cncongrcoprm  10632  prmind2  10646  isprm6  10670  sqrt2irr  10685  oddpwdclemodd  10694