Theorem nncn 9291

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

Syntax hints:   -> wi 4   e. wcel 2209   CCcc 8167   NNcn 9283

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 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 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266

This theorem 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-v 2823  df-in 3226  df-ss 3233  df-int 3966  df-inn 9284

This theorem is referenced by:  nn1m1nn  9301  nn1suc  9302  nnaddcl  9303  nnmulcl  9304  nnsub  9322  nndiv  9324  nndivtr  9325  nnnn0addcl  9572  nn0nnaddcl  9573  elnnnn0  9585  nnnegz  9626  zaddcllempos  9660  zaddcllemneg  9662  nnaddm1cl  9685  elz2  9695  zdiv  9713  zdivadd  9714  zdivmul  9715  nneoor  9727  nneo  9728  divfnzn  10000  qmulz  10002  qaddcl  10014  qnegcl  10015  qmulcl  10016  qreccl  10021  nnledivrp  10146  nn0ledivnn  10147  fseq1m1p1  10480  nnsplit  10522  ubmelm1fzo  10622  subfzo0  10639  flqdiv  10736  addmodidr  10788  modfzo0difsn  10810  nn0ennn  10848  expnegap0  10962  expm1t  10982  nnsqcl  11024  nnlesq  11058  facdiv  11154  facndiv  11155  faclbnd  11157  bcn1  11174  bcn2m1  11186  arisum  12243  arisum2  12244  expcnvap0  12247  mertenslem2  12281  ef0lem  12405  efexp  12427  nndivides  12542  modmulconst  12568  dvdsflip  12596  nn0enne  12647  nno  12651  divalgmod  12672  ndvdsadd  12676  modgcd  12746  gcddiv  12774  gcdmultiple  12775  gcdmultiplez  12776  rpmulgcd  12781  rplpwr  12782  sqgcd  12784  lcmgcdlem  12833  qredeq  12852  qredeu  12853  divgcdcoprm0  12857  cncongrcoprm  12862  prmind2  12876  isprm6  12903  sqrt2irr  12918  oddpwdclemodd  12928  divnumden  12952  divdenle  12953  nn0gcdsq  12956  hashgcdlem  12994  pythagtriplem1  13022  pythagtriplem2  13023  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem15  13035  pythagtriplem16  13036  pythagtriplem17  13037  pythagtriplem19  13039  pcqcl  13063  pcexp  13066  pcneg  13082  fldivp1  13105  oddprmdvds  13111  prmpwdvds  13112  infpnlem2  13117  4sqlem19  13166  mulgnegnn  13912  mulgnnass  13937  mulgmodid  13941  cnfldmulg  14885  znidomb  14965  znrrg  14967  dvexp  15735  rpcxproot  15939  logbgcd1irr  15992  pellexlem1  16005  perfect  16029  lgssq2  16074  gausslemma2dlem1a  16091  gausslemma2dlem3  16096  2lgslem1a1  16119  2sqlem6  16153  2sqlem10  16158