Theorem nncn 9241

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8121  ℕcn 9233

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4227  ax-cnex 8214  ax-resscn 8215  ax-1re 8217  ax-addrcl 8220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2814  df-in 3216  df-ss 3223  df-int 3949  df-inn 9234

This theorem is referenced by:  nn1m1nn  9251  nn1suc  9252  nnaddcl  9253  nnmulcl  9254  nnsub  9272  nndiv  9274  nndivtr  9275  nnnn0addcl  9522  nn0nnaddcl  9523  elnnnn0  9535  nnnegz  9576  zaddcllempos  9610  zaddcllemneg  9612  nnaddm1cl  9635  elz2  9645  zdiv  9662  zdivadd  9663  zdivmul  9664  nneoor  9676  nneo  9677  divfnzn  9949  qmulz  9951  qaddcl  9963  qnegcl  9964  qmulcl  9965  qreccl  9970  nnledivrp  10095  nn0ledivnn  10096  fseq1m1p1  10425  nnsplit  10467  ubmelm1fzo  10567  subfzo0  10584  flqdiv  10679  addmodidr  10731  modfzo0difsn  10753  nn0ennn  10791  expnegap0  10905  expm1t  10925  nnsqcl  10967  nnlesq  11001  facdiv  11096  facndiv  11097  faclbnd  11099  bcn1  11116  bcn2m1  11127  arisum  12177  arisum2  12178  expcnvap0  12181  mertenslem2  12215  ef0lem  12339  efexp  12361  nndivides  12476  modmulconst  12502  dvdsflip  12530  nn0enne  12581  nno  12585  divalgmod  12606  ndvdsadd  12610  modgcd  12680  gcddiv  12708  gcdmultiple  12709  gcdmultiplez  12710  rpmulgcd  12715  rplpwr  12716  sqgcd  12718  lcmgcdlem  12767  qredeq  12786  qredeu  12787  divgcdcoprm0  12791  cncongrcoprm  12796  prmind2  12810  isprm6  12837  sqrt2irr  12852  oddpwdclemodd  12862  divnumden  12886  divdenle  12887  nn0gcdsq  12890  hashgcdlem  12928  pythagtriplem1  12956  pythagtriplem2  12957  pythagtriplem6  12961  pythagtriplem7  12962  pythagtriplem12  12966  pythagtriplem14  12968  pythagtriplem15  12969  pythagtriplem16  12970  pythagtriplem17  12971  pythagtriplem19  12973  pcqcl  12997  pcexp  13000  pcneg  13016  fldivp1  13039  oddprmdvds  13045  prmpwdvds  13046  infpnlem2  13051  4sqlem19  13100  mulgnegnn  13838  mulgnnass  13863  mulgmodid  13867  cnfldmulg  14711  znidomb  14793  znrrg  14795  dvexp  15563  rpcxproot  15766  logbgcd1irr  15819  pellexlem1  15832  perfect  15856  lgssq2  15901  gausslemma2dlem1a  15918  gausslemma2dlem3  15923  2lgslem1a1  15946  2sqlem6  15980  2sqlem10  15985