Theorem nncn 8873

Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nncn	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Proof of Theorem nncn

Step	Hyp	Ref	Expression
1		nnsscn 8870	. 2 ⊢ ℕ ⊆ ℂ
2	1	sseli 3143	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7759  ℕcn 8865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105  ax-cnex 7852  ax-resscn 7853  ax-1re 7855  ax-addrcl 7858

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-in 3127  df-ss 3134  df-int 3830  df-inn 8866

This theorem is referenced by:  nn1m1nn  8883  nn1suc  8884  nnaddcl  8885  nnmulcl  8886  nnsub  8904  nndiv  8906  nndivtr  8907  nnnn0addcl  9152  nn0nnaddcl  9153  elnnnn0  9165  nnnegz  9202  zaddcllempos  9236  zaddcllemneg  9238  nnaddm1cl  9260  elz2  9270  zdiv  9287  zdivadd  9288  zdivmul  9289  nneoor  9301  nneo  9302  divfnzn  9567  qmulz  9569  qaddcl  9581  qnegcl  9582  qmulcl  9583  qreccl  9588  nnledivrp  9710  nn0ledivnn  9711  fseq1m1p1  10038  nnsplit  10080  ubmelm1fzo  10169  subfzo0  10185  flqdiv  10264  addmodidr  10316  modfzo0difsn  10338  nn0ennn  10376  expnegap0  10471  expm1t  10491  nnsqcl  10532  nnlesq  10566  facdiv  10659  facndiv  10660  faclbnd  10662  bcn1  10679  bcn2m1  10690  arisum  11448  arisum2  11449  expcnvap0  11452  mertenslem2  11486  ef0lem  11610  efexp  11632  nndivides  11746  modmulconst  11772  dvdsflip  11798  nn0enne  11848  nno  11852  divalgmod  11873  ndvdsadd  11877  modgcd  11933  gcddiv  11961  gcdmultiple  11962  gcdmultiplez  11963  rpmulgcd  11968  rplpwr  11969  sqgcd  11971  lcmgcdlem  12018  qredeq  12037  qredeu  12038  divgcdcoprm0  12042  cncongrcoprm  12047  prmind2  12061  isprm6  12088  sqrt2irr  12103  oddpwdclemodd  12113  divnumden  12137  divdenle  12138  nn0gcdsq  12141  hashgcdlem  12179  pythagtriplem1  12206  pythagtriplem2  12207  pythagtriplem6  12211  pythagtriplem7  12212  pythagtriplem12  12216  pythagtriplem14  12218  pythagtriplem15  12219  pythagtriplem16  12220  pythagtriplem17  12221  pythagtriplem19  12223  pcqcl  12247  pcexp  12250  pcneg  12265  fldivp1  12287  oddprmdvds  12293  prmpwdvds  12294  infpnlem2  12299  dvexp  13390  rpcxproot  13549  logbgcd1irr  13600  lgssq2  13657  2sqlem6  13671  2sqlem10  13676