Theorem nncn 9321

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 9318	. 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 8183   NNcn 9313

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 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

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 9314

This theorem is used by:  nn1m1nn  9331  nn1suc  9332  nnaddcl  9333  nnmulcl  9334  nnsub  9352  nndiv  9354  nndivtr  9355  nnnn0addcl  9604  nn0nnaddcl  9605  elnnnn0  9617  nnnegz  9658  zaddcllempos  9692  zaddcllemneg  9694  nnaddm1cl  9717  elz2  9727  zdiv  9745  zdivadd  9746  zdivmul  9747  nneoor  9759  nneo  9760  divfnzn  10037  qmulz  10039  qaddcl  10051  qnegcl  10052  qmulcl  10053  qreccl  10058  nnledivrp  10184  nn0ledivnn  10185  fseq1m1p1  10519  nnsplit  10561  ubmelm1fzo  10661  subfzo0  10678  flqdiv  10779  addmodidr  10831  modfzo0difsn  10853  nn0ennn  10891  expnegap0  11005  expm1t  11025  nnsqcl  11067  nnlesq  11101  facdiv  11198  facndiv  11199  faclbnd  11201  bcn1  11218  bcn2m1  11230  arisum  12290  arisum2  12291  expcnvap0  12294  mertenslem2  12328  ef0lem  12452  efexp  12474  nndivides  12589  modmulconst  12615  dvdsflip  12643  nn0enne  12694  nno  12698  divalgmod  12719  ndvdsadd  12723  modgcd  12793  gcddiv  12821  gcdmultiple  12822  gcdmultiplez  12823  rpmulgcd  12828  rplpwr  12829  sqgcd  12831  lcmgcdlem  12880  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  cncongrcoprm  12909  prmind2  12923  isprm6  12951  sqrt2irr  12966  divnumden  13001  divdenle  13002  nn0gcdsq  13005  hashgcdlem  13045  pythagtriplem1  13073  pythagtriplem2  13074  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  pythagtriplem19  13090  pcqcl  13114  pcexp  13117  pcneg  13133  fldivp1  13156  oddprmdvds  13162  prmpwdvds  13163  infpnlem2  13168  4sqlem19  13217  mulgnegnn  13994  mulgnnass  14019  mulgmodid  14023  cnfldmulg  15022  znidomb  15102  znrrg  15104  dvexp  15937  root1idef  16084  rpcxproot  16147  efnthr  16176  logbgcd1irr  16203  birthdaylem2  16226  pellexlem1  16229  chtublem  16295  perfect  16301  pcbcctr  16303  bclbnd  16307  bposlem1  16311  bposlem6  16316  lgssq2  16365  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  2lgslem1a1  16410  2sqlem6  16444  2sqlem10  16449