Theorem nncn 9051

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℂcc 7930  ℕcn 9043

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4166  ax-cnex 8023  ax-resscn 8024  ax-1re 8026  ax-addrcl 8029

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775  df-in 3173  df-ss 3180  df-int 3888  df-inn 9044

This theorem is referenced by:  nn1m1nn  9061  nn1suc  9062  nnaddcl  9063  nnmulcl  9064  nnsub  9082  nndiv  9084  nndivtr  9085  nnnn0addcl  9332  nn0nnaddcl  9333  elnnnn0  9345  nnnegz  9382  zaddcllempos  9416  zaddcllemneg  9418  nnaddm1cl  9441  elz2  9451  zdiv  9468  zdivadd  9469  zdivmul  9470  nneoor  9482  nneo  9483  divfnzn  9749  qmulz  9751  qaddcl  9763  qnegcl  9764  qmulcl  9765  qreccl  9770  nnledivrp  9895  nn0ledivnn  9896  fseq1m1p1  10224  nnsplit  10266  ubmelm1fzo  10362  subfzo0  10378  flqdiv  10473  addmodidr  10525  modfzo0difsn  10547  nn0ennn  10585  expnegap0  10699  expm1t  10719  nnsqcl  10761  nnlesq  10795  facdiv  10890  facndiv  10891  faclbnd  10893  bcn1  10910  bcn2m1  10921  arisum  11853  arisum2  11854  expcnvap0  11857  mertenslem2  11891  ef0lem  12015  efexp  12037  nndivides  12152  modmulconst  12178  dvdsflip  12206  nn0enne  12257  nno  12261  divalgmod  12282  ndvdsadd  12286  modgcd  12356  gcddiv  12384  gcdmultiple  12385  gcdmultiplez  12386  rpmulgcd  12391  rplpwr  12392  sqgcd  12394  lcmgcdlem  12443  qredeq  12462  qredeu  12463  divgcdcoprm0  12467  cncongrcoprm  12472  prmind2  12486  isprm6  12513  sqrt2irr  12528  oddpwdclemodd  12538  divnumden  12562  divdenle  12563  nn0gcdsq  12566  hashgcdlem  12604  pythagtriplem1  12632  pythagtriplem2  12633  pythagtriplem6  12637  pythagtriplem7  12638  pythagtriplem12  12642  pythagtriplem14  12644  pythagtriplem15  12645  pythagtriplem16  12646  pythagtriplem17  12647  pythagtriplem19  12649  pcqcl  12673  pcexp  12676  pcneg  12692  fldivp1  12715  oddprmdvds  12721  prmpwdvds  12722  infpnlem2  12727  4sqlem19  12776  mulgnegnn  13512  mulgnnass  13537  mulgmodid  13541  cnfldmulg  14382  znidomb  14464  znrrg  14466  dvexp  15227  rpcxproot  15430  logbgcd1irr  15483  perfect  15517  lgssq2  15562  gausslemma2dlem1a  15579  gausslemma2dlem3  15584  2lgslem1a1  15607  2sqlem6  15641  2sqlem10  15646