Theorem nncn 9315

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8178   NNcn 9307

This proof depends on 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 4249  ax-cnex 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

This proof 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 3971  df-inn 9308

This theorem is used by:  nn1m1nn  9325  nn1suc  9326  nnaddcl  9327  nnmulcl  9328  nnsub  9346  nndiv  9348  nndivtr  9349  nnnn0addcl  9598  nn0nnaddcl  9599  elnnnn0  9611  nnnegz  9652  zaddcllempos  9686  zaddcllemneg  9688  nnaddm1cl  9711  elz2  9721  zdiv  9739  zdivadd  9740  zdivmul  9741  nneoor  9753  nneo  9754  divfnzn  10031  qmulz  10033  qaddcl  10045  qnegcl  10046  qmulcl  10047  qreccl  10052  nnledivrp  10178  nn0ledivnn  10179  fseq1m1p1  10513  nnsplit  10555  ubmelm1fzo  10655  subfzo0  10672  flqdiv  10773  addmodidr  10825  modfzo0difsn  10847  nn0ennn  10885  expnegap0  10999  expm1t  11019  nnsqcl  11061  nnlesq  11095  facdiv  11192  facndiv  11193  faclbnd  11195  bcn1  11212  bcn2m1  11224  arisum  12284  arisum2  12285  expcnvap0  12288  mertenslem2  12322  ef0lem  12446  efexp  12468  nndivides  12583  modmulconst  12609  dvdsflip  12637  nn0enne  12688  nno  12692  divalgmod  12713  ndvdsadd  12717  modgcd  12787  gcddiv  12815  gcdmultiple  12816  gcdmultiplez  12817  rpmulgcd  12822  rplpwr  12823  sqgcd  12825  lcmgcdlem  12874  qredeq  12893  qredeu  12894  divgcdcoprm0  12898  cncongrcoprm  12903  prmind2  12917  isprm6  12945  sqrt2irr  12960  divnumden  12995  divdenle  12996  nn0gcdsq  12999  hashgcdlem  13039  pythagtriplem1  13067  pythagtriplem2  13068  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  pythagtriplem19  13084  pcqcl  13108  pcexp  13111  pcneg  13127  fldivp1  13150  oddprmdvds  13156  prmpwdvds  13157  infpnlem2  13162  4sqlem19  13211  mulgnegnn  13988  mulgnnass  14013  mulgmodid  14017  cnfldmulg  14997  znidomb  15077  znrrg  15079  dvexp  15903  rpcxproot  16111  logbgcd1irr  16164  birthdaylem2  16187  pellexlem1  16190  chtublem  16256  perfect  16262  pcbcctr  16264  bclbnd  16268  bposlem1  16272  bposlem6  16277  lgssq2  16326  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  2lgslem1a1  16371  2sqlem6  16405  2sqlem10  16410