Theorem nncn 9086

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℂcc 7965  ℕcn 9078

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-sep 4181  ax-cnex 8058  ax-resscn 8059  ax-1re 8061  ax-addrcl 8064

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-v 2781  df-in 3183  df-ss 3190  df-int 3903  df-inn 9079

This theorem is referenced by:  nn1m1nn  9096  nn1suc  9097  nnaddcl  9098  nnmulcl  9099  nnsub  9117  nndiv  9119  nndivtr  9120  nnnn0addcl  9367  nn0nnaddcl  9368  elnnnn0  9380  nnnegz  9417  zaddcllempos  9451  zaddcllemneg  9453  nnaddm1cl  9476  elz2  9486  zdiv  9503  zdivadd  9504  zdivmul  9505  nneoor  9517  nneo  9518  divfnzn  9784  qmulz  9786  qaddcl  9798  qnegcl  9799  qmulcl  9800  qreccl  9805  nnledivrp  9930  nn0ledivnn  9931  fseq1m1p1  10259  nnsplit  10301  ubmelm1fzo  10399  subfzo0  10415  flqdiv  10510  addmodidr  10562  modfzo0difsn  10584  nn0ennn  10622  expnegap0  10736  expm1t  10756  nnsqcl  10798  nnlesq  10832  facdiv  10927  facndiv  10928  faclbnd  10930  bcn1  10947  bcn2m1  10958  arisum  11975  arisum2  11976  expcnvap0  11979  mertenslem2  12013  ef0lem  12137  efexp  12159  nndivides  12274  modmulconst  12300  dvdsflip  12328  nn0enne  12379  nno  12383  divalgmod  12404  ndvdsadd  12408  modgcd  12478  gcddiv  12506  gcdmultiple  12507  gcdmultiplez  12508  rpmulgcd  12513  rplpwr  12514  sqgcd  12516  lcmgcdlem  12565  qredeq  12584  qredeu  12585  divgcdcoprm0  12589  cncongrcoprm  12594  prmind2  12608  isprm6  12635  sqrt2irr  12650  oddpwdclemodd  12660  divnumden  12684  divdenle  12685  nn0gcdsq  12688  hashgcdlem  12726  pythagtriplem1  12754  pythagtriplem2  12755  pythagtriplem6  12759  pythagtriplem7  12760  pythagtriplem12  12764  pythagtriplem14  12766  pythagtriplem15  12767  pythagtriplem16  12768  pythagtriplem17  12769  pythagtriplem19  12771  pcqcl  12795  pcexp  12798  pcneg  12814  fldivp1  12837  oddprmdvds  12843  prmpwdvds  12844  infpnlem2  12849  4sqlem19  12898  mulgnegnn  13635  mulgnnass  13660  mulgmodid  13664  cnfldmulg  14505  znidomb  14587  znrrg  14589  dvexp  15350  rpcxproot  15553  logbgcd1irr  15606  perfect  15640  lgssq2  15685  gausslemma2dlem1a  15702  gausslemma2dlem3  15707  2lgslem1a1  15730  2sqlem6  15764  2sqlem10  15769