Theorem nncn 9144

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 9141	. 2 ⊢ ℕ ⊆ ℂ
2	1	sseli 3221	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8023  ℕcn 9136

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8116  ax-resscn 8117  ax-1re 8119  ax-addrcl 8122

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9137

This theorem is referenced by:  nn1m1nn  9154  nn1suc  9155  nnaddcl  9156  nnmulcl  9157  nnsub  9175  nndiv  9177  nndivtr  9178  nnnn0addcl  9425  nn0nnaddcl  9426  elnnnn0  9438  nnnegz  9475  zaddcllempos  9509  zaddcllemneg  9511  nnaddm1cl  9534  elz2  9544  zdiv  9561  zdivadd  9562  zdivmul  9563  nneoor  9575  nneo  9576  divfnzn  9848  qmulz  9850  qaddcl  9862  qnegcl  9863  qmulcl  9864  qreccl  9869  nnledivrp  9994  nn0ledivnn  9995  fseq1m1p1  10323  nnsplit  10365  ubmelm1fzo  10464  subfzo0  10481  flqdiv  10576  addmodidr  10628  modfzo0difsn  10650  nn0ennn  10688  expnegap0  10802  expm1t  10822  nnsqcl  10864  nnlesq  10898  facdiv  10993  facndiv  10994  faclbnd  10996  bcn1  11013  bcn2m1  11024  arisum  12052  arisum2  12053  expcnvap0  12056  mertenslem2  12090  ef0lem  12214  efexp  12236  nndivides  12351  modmulconst  12377  dvdsflip  12405  nn0enne  12456  nno  12460  divalgmod  12481  ndvdsadd  12485  modgcd  12555  gcddiv  12583  gcdmultiple  12584  gcdmultiplez  12585  rpmulgcd  12590  rplpwr  12591  sqgcd  12593  lcmgcdlem  12642  qredeq  12661  qredeu  12662  divgcdcoprm0  12666  cncongrcoprm  12671  prmind2  12685  isprm6  12712  sqrt2irr  12727  oddpwdclemodd  12737  divnumden  12761  divdenle  12762  nn0gcdsq  12765  hashgcdlem  12803  pythagtriplem1  12831  pythagtriplem2  12832  pythagtriplem6  12836  pythagtriplem7  12837  pythagtriplem12  12841  pythagtriplem14  12843  pythagtriplem15  12844  pythagtriplem16  12845  pythagtriplem17  12846  pythagtriplem19  12848  pcqcl  12872  pcexp  12875  pcneg  12891  fldivp1  12914  oddprmdvds  12920  prmpwdvds  12921  infpnlem2  12926  4sqlem19  12975  mulgnegnn  13712  mulgnnass  13737  mulgmodid  13741  cnfldmulg  14583  znidomb  14665  znrrg  14667  dvexp  15428  rpcxproot  15631  logbgcd1irr  15684  perfect  15718  lgssq2  15763  gausslemma2dlem1a  15780  gausslemma2dlem3  15785  2lgslem1a1  15808  2sqlem6  15842  2sqlem10  15847