Theorem nncn 9015

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℕcn 9007

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3876  df-inn 9008

This theorem is referenced by:  nn1m1nn  9025  nn1suc  9026  nnaddcl  9027  nnmulcl  9028  nnsub  9046  nndiv  9048  nndivtr  9049  nnnn0addcl  9296  nn0nnaddcl  9297  elnnnn0  9309  nnnegz  9346  zaddcllempos  9380  zaddcllemneg  9382  nnaddm1cl  9404  elz2  9414  zdiv  9431  zdivadd  9432  zdivmul  9433  nneoor  9445  nneo  9446  divfnzn  9712  qmulz  9714  qaddcl  9726  qnegcl  9727  qmulcl  9728  qreccl  9733  nnledivrp  9858  nn0ledivnn  9859  fseq1m1p1  10187  nnsplit  10229  ubmelm1fzo  10319  subfzo0  10335  flqdiv  10430  addmodidr  10482  modfzo0difsn  10504  nn0ennn  10542  expnegap0  10656  expm1t  10676  nnsqcl  10718  nnlesq  10752  facdiv  10847  facndiv  10848  faclbnd  10850  bcn1  10867  bcn2m1  10878  arisum  11680  arisum2  11681  expcnvap0  11684  mertenslem2  11718  ef0lem  11842  efexp  11864  nndivides  11979  modmulconst  12005  dvdsflip  12033  nn0enne  12084  nno  12088  divalgmod  12109  ndvdsadd  12113  modgcd  12183  gcddiv  12211  gcdmultiple  12212  gcdmultiplez  12213  rpmulgcd  12218  rplpwr  12219  sqgcd  12221  lcmgcdlem  12270  qredeq  12289  qredeu  12290  divgcdcoprm0  12294  cncongrcoprm  12299  prmind2  12313  isprm6  12340  sqrt2irr  12355  oddpwdclemodd  12365  divnumden  12389  divdenle  12390  nn0gcdsq  12393  hashgcdlem  12431  pythagtriplem1  12459  pythagtriplem2  12460  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem17  12474  pythagtriplem19  12476  pcqcl  12500  pcexp  12503  pcneg  12519  fldivp1  12542  oddprmdvds  12548  prmpwdvds  12549  infpnlem2  12554  4sqlem19  12603  mulgnegnn  13338  mulgnnass  13363  mulgmodid  13367  cnfldmulg  14208  znidomb  14290  znrrg  14292  dvexp  15031  rpcxproot  15234  logbgcd1irr  15287  perfect  15321  lgssq2  15366  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  2lgslem1a1  15411  2sqlem6  15445  2sqlem10  15450