Theorem nncn 8990

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

Syntax hints:   -> wi 4   e. wcel 2164   CCcc 7870   NNcn 8982

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

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-v 2762  df-in 3159  df-ss 3166  df-int 3871  df-inn 8983

This theorem is referenced by:  nn1m1nn  9000  nn1suc  9001  nnaddcl  9002  nnmulcl  9003  nnsub  9021  nndiv  9023  nndivtr  9024  nnnn0addcl  9270  nn0nnaddcl  9271  elnnnn0  9283  nnnegz  9320  zaddcllempos  9354  zaddcllemneg  9356  nnaddm1cl  9378  elz2  9388  zdiv  9405  zdivadd  9406  zdivmul  9407  nneoor  9419  nneo  9420  divfnzn  9686  qmulz  9688  qaddcl  9700  qnegcl  9701  qmulcl  9702  qreccl  9707  nnledivrp  9832  nn0ledivnn  9833  fseq1m1p1  10161  nnsplit  10203  ubmelm1fzo  10293  subfzo0  10309  flqdiv  10392  addmodidr  10444  modfzo0difsn  10466  nn0ennn  10504  expnegap0  10618  expm1t  10638  nnsqcl  10680  nnlesq  10714  facdiv  10809  facndiv  10810  faclbnd  10812  bcn1  10829  bcn2m1  10840  arisum  11641  arisum2  11642  expcnvap0  11645  mertenslem2  11679  ef0lem  11803  efexp  11825  nndivides  11940  modmulconst  11966  dvdsflip  11993  nn0enne  12043  nno  12047  divalgmod  12068  ndvdsadd  12072  modgcd  12128  gcddiv  12156  gcdmultiple  12157  gcdmultiplez  12158  rpmulgcd  12163  rplpwr  12164  sqgcd  12166  lcmgcdlem  12215  qredeq  12234  qredeu  12235  divgcdcoprm0  12239  cncongrcoprm  12244  prmind2  12258  isprm6  12285  sqrt2irr  12300  oddpwdclemodd  12310  divnumden  12334  divdenle  12335  nn0gcdsq  12338  hashgcdlem  12376  pythagtriplem1  12403  pythagtriplem2  12404  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem17  12418  pythagtriplem19  12420  pcqcl  12444  pcexp  12447  pcneg  12463  fldivp1  12486  oddprmdvds  12492  prmpwdvds  12493  infpnlem2  12498  4sqlem19  12547  mulgnegnn  13202  mulgnnass  13227  mulgmodid  13231  cnfldmulg  14064  znidomb  14146  znrrg  14148  dvexp  14860  rpcxproot  15048  logbgcd1irr  15099  lgssq2  15157  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  2sqlem6  15207  2sqlem10  15212