Theorem nncn 8926

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7808   NNcn 8918

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739  df-in 3135  df-ss 3142  df-int 3845  df-inn 8919

This theorem is referenced by:  nn1m1nn  8936  nn1suc  8937  nnaddcl  8938  nnmulcl  8939  nnsub  8957  nndiv  8959  nndivtr  8960  nnnn0addcl  9205  nn0nnaddcl  9206  elnnnn0  9218  nnnegz  9255  zaddcllempos  9289  zaddcllemneg  9291  nnaddm1cl  9313  elz2  9323  zdiv  9340  zdivadd  9341  zdivmul  9342  nneoor  9354  nneo  9355  divfnzn  9620  qmulz  9622  qaddcl  9634  qnegcl  9635  qmulcl  9636  qreccl  9641  nnledivrp  9765  nn0ledivnn  9766  fseq1m1p1  10094  nnsplit  10136  ubmelm1fzo  10225  subfzo0  10241  flqdiv  10320  addmodidr  10372  modfzo0difsn  10394  nn0ennn  10432  expnegap0  10527  expm1t  10547  nnsqcl  10589  nnlesq  10623  facdiv  10717  facndiv  10718  faclbnd  10720  bcn1  10737  bcn2m1  10748  arisum  11505  arisum2  11506  expcnvap0  11509  mertenslem2  11543  ef0lem  11667  efexp  11689  nndivides  11803  modmulconst  11829  dvdsflip  11856  nn0enne  11906  nno  11910  divalgmod  11931  ndvdsadd  11935  modgcd  11991  gcddiv  12019  gcdmultiple  12020  gcdmultiplez  12021  rpmulgcd  12026  rplpwr  12027  sqgcd  12029  lcmgcdlem  12076  qredeq  12095  qredeu  12096  divgcdcoprm0  12100  cncongrcoprm  12105  prmind2  12119  isprm6  12146  sqrt2irr  12161  oddpwdclemodd  12171  divnumden  12195  divdenle  12196  nn0gcdsq  12199  hashgcdlem  12237  pythagtriplem1  12264  pythagtriplem2  12265  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem15  12277  pythagtriplem16  12278  pythagtriplem17  12279  pythagtriplem19  12281  pcqcl  12305  pcexp  12308  pcneg  12323  fldivp1  12345  oddprmdvds  12351  prmpwdvds  12352  infpnlem2  12357  mulgnegnn  12992  mulgnnass  13016  mulgmodid  13020  cnfldmulg  13440  dvexp  14145  rpcxproot  14304  logbgcd1irr  14355  lgssq2  14412  2sqlem6  14437  2sqlem10  14442