Theorem nncn 9079

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

Syntax hints:   -> wi 4   e. wcel 2178   CCcc 7958   NNcn 9071

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

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-v 2778  df-in 3180  df-ss 3187  df-int 3900  df-inn 9072

This theorem is referenced by:  nn1m1nn  9089  nn1suc  9090  nnaddcl  9091  nnmulcl  9092  nnsub  9110  nndiv  9112  nndivtr  9113  nnnn0addcl  9360  nn0nnaddcl  9361  elnnnn0  9373  nnnegz  9410  zaddcllempos  9444  zaddcllemneg  9446  nnaddm1cl  9469  elz2  9479  zdiv  9496  zdivadd  9497  zdivmul  9498  nneoor  9510  nneo  9511  divfnzn  9777  qmulz  9779  qaddcl  9791  qnegcl  9792  qmulcl  9793  qreccl  9798  nnledivrp  9923  nn0ledivnn  9924  fseq1m1p1  10252  nnsplit  10294  ubmelm1fzo  10392  subfzo0  10408  flqdiv  10503  addmodidr  10555  modfzo0difsn  10577  nn0ennn  10615  expnegap0  10729  expm1t  10749  nnsqcl  10791  nnlesq  10825  facdiv  10920  facndiv  10921  faclbnd  10923  bcn1  10940  bcn2m1  10951  arisum  11924  arisum2  11925  expcnvap0  11928  mertenslem2  11962  ef0lem  12086  efexp  12108  nndivides  12223  modmulconst  12249  dvdsflip  12277  nn0enne  12328  nno  12332  divalgmod  12353  ndvdsadd  12357  modgcd  12427  gcddiv  12455  gcdmultiple  12456  gcdmultiplez  12457  rpmulgcd  12462  rplpwr  12463  sqgcd  12465  lcmgcdlem  12514  qredeq  12533  qredeu  12534  divgcdcoprm0  12538  cncongrcoprm  12543  prmind2  12557  isprm6  12584  sqrt2irr  12599  oddpwdclemodd  12609  divnumden  12633  divdenle  12634  nn0gcdsq  12637  hashgcdlem  12675  pythagtriplem1  12703  pythagtriplem2  12704  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem15  12716  pythagtriplem16  12717  pythagtriplem17  12718  pythagtriplem19  12720  pcqcl  12744  pcexp  12747  pcneg  12763  fldivp1  12786  oddprmdvds  12792  prmpwdvds  12793  infpnlem2  12798  4sqlem19  12847  mulgnegnn  13583  mulgnnass  13608  mulgmodid  13612  cnfldmulg  14453  znidomb  14535  znrrg  14537  dvexp  15298  rpcxproot  15501  logbgcd1irr  15554  perfect  15588  lgssq2  15633  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  2lgslem1a1  15678  2sqlem6  15712  2sqlem10  15717