Theorem nncn 9150

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8029   NNcn 9142

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9143

This theorem is referenced by:  nn1m1nn  9160  nn1suc  9161  nnaddcl  9162  nnmulcl  9163  nnsub  9181  nndiv  9183  nndivtr  9184  nnnn0addcl  9431  nn0nnaddcl  9432  elnnnn0  9444  nnnegz  9481  zaddcllempos  9515  zaddcllemneg  9517  nnaddm1cl  9540  elz2  9550  zdiv  9567  zdivadd  9568  zdivmul  9569  nneoor  9581  nneo  9582  divfnzn  9854  qmulz  9856  qaddcl  9868  qnegcl  9869  qmulcl  9870  qreccl  9875  nnledivrp  10000  nn0ledivnn  10001  fseq1m1p1  10329  nnsplit  10371  ubmelm1fzo  10470  subfzo0  10487  flqdiv  10582  addmodidr  10634  modfzo0difsn  10656  nn0ennn  10694  expnegap0  10808  expm1t  10828  nnsqcl  10870  nnlesq  10904  facdiv  10999  facndiv  11000  faclbnd  11002  bcn1  11019  bcn2m1  11030  arisum  12058  arisum2  12059  expcnvap0  12062  mertenslem2  12096  ef0lem  12220  efexp  12242  nndivides  12357  modmulconst  12383  dvdsflip  12411  nn0enne  12462  nno  12466  divalgmod  12487  ndvdsadd  12491  modgcd  12561  gcddiv  12589  gcdmultiple  12590  gcdmultiplez  12591  rpmulgcd  12596  rplpwr  12597  sqgcd  12599  lcmgcdlem  12648  qredeq  12667  qredeu  12668  divgcdcoprm0  12672  cncongrcoprm  12677  prmind2  12691  isprm6  12718  sqrt2irr  12733  oddpwdclemodd  12743  divnumden  12767  divdenle  12768  nn0gcdsq  12771  hashgcdlem  12809  pythagtriplem1  12837  pythagtriplem2  12838  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem17  12852  pythagtriplem19  12854  pcqcl  12878  pcexp  12881  pcneg  12897  fldivp1  12920  oddprmdvds  12926  prmpwdvds  12927  infpnlem2  12932  4sqlem19  12981  mulgnegnn  13718  mulgnnass  13743  mulgmodid  13747  cnfldmulg  14589  znidomb  14671  znrrg  14673  dvexp  15434  rpcxproot  15637  logbgcd1irr  15690  perfect  15724  lgssq2  15769  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  2lgslem1a1  15814  2sqlem6  15848  2sqlem10  15853