Theorem nncn 7922

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

Syntax hints:   -> wi 4   e. wcel 1393   CCcc 6887   NNcn 7914

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-cnex 6975  ax-resscn 6976  ax-1re 6978  ax-addrcl 6981

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-v 2559  df-in 2924  df-ss 2931  df-int 3616  df-inn 7915

This theorem is referenced by:  nn1m1nn  7932  nn1suc  7933  nnaddcl  7934  nnmulcl  7935  nnsub  7952  nndiv  7954  nndivtr  7955  nnnn0addcl  8212  nn0nnaddcl  8213  elnnnn0  8225  nnnegz  8248  zaddcllempos  8282  zaddcllemneg  8284  nnaddm1cl  8305  elz2  8312  zdiv  8328  zdivadd  8329  zdivmul  8330  nneoor  8340  nneo  8341  divfnzn  8556  qmulz  8558  qaddcl  8570  qnegcl  8571  qmulcl  8572  qreccl  8576  fseq1m1p1  8957  ubmelm1fzo  9082  subfzo0  9097  flqdiv  9163  nn0ennn  9209  expnegap0  9263  expm1t  9283  nnsqcl  9323  nnlesq  9356  sqrt2irr  9878