Theorem nncn 9017

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  ℕcn 9009

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 7989  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

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 9010

This theorem is referenced by:  nn1m1nn  9027  nn1suc  9028  nnaddcl  9029  nnmulcl  9030  nnsub  9048  nndiv  9050  nndivtr  9051  nnnn0addcl  9298  nn0nnaddcl  9299  elnnnn0  9311  nnnegz  9348  zaddcllempos  9382  zaddcllemneg  9384  nnaddm1cl  9406  elz2  9416  zdiv  9433  zdivadd  9434  zdivmul  9435  nneoor  9447  nneo  9448  divfnzn  9714  qmulz  9716  qaddcl  9728  qnegcl  9729  qmulcl  9730  qreccl  9735  nnledivrp  9860  nn0ledivnn  9861  fseq1m1p1  10189  nnsplit  10231  ubmelm1fzo  10321  subfzo0  10337  flqdiv  10432  addmodidr  10484  modfzo0difsn  10506  nn0ennn  10544  expnegap0  10658  expm1t  10678  nnsqcl  10720  nnlesq  10754  facdiv  10849  facndiv  10850  faclbnd  10852  bcn1  10869  bcn2m1  10880  arisum  11682  arisum2  11683  expcnvap0  11686  mertenslem2  11720  ef0lem  11844  efexp  11866  nndivides  11981  modmulconst  12007  dvdsflip  12035  nn0enne  12086  nno  12090  divalgmod  12111  ndvdsadd  12115  modgcd  12185  gcddiv  12213  gcdmultiple  12214  gcdmultiplez  12215  rpmulgcd  12220  rplpwr  12221  sqgcd  12223  lcmgcdlem  12272  qredeq  12291  qredeu  12292  divgcdcoprm0  12296  cncongrcoprm  12301  prmind2  12315  isprm6  12342  sqrt2irr  12357  oddpwdclemodd  12367  divnumden  12391  divdenle  12392  nn0gcdsq  12395  hashgcdlem  12433  pythagtriplem1  12461  pythagtriplem2  12462  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem15  12474  pythagtriplem16  12475  pythagtriplem17  12476  pythagtriplem19  12478  pcqcl  12502  pcexp  12505  pcneg  12521  fldivp1  12544  oddprmdvds  12550  prmpwdvds  12551  infpnlem2  12556  4sqlem19  12605  mulgnegnn  13340  mulgnnass  13365  mulgmodid  13369  cnfldmulg  14210  znidomb  14292  znrrg  14294  dvexp  15055  rpcxproot  15258  logbgcd1irr  15311  perfect  15345  lgssq2  15390  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  2lgslem1a1  15435  2sqlem6  15469  2sqlem10  15474