Theorem nncn 9126

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8005  ℕcn 9118

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8098  ax-resscn 8099  ax-1re 8101  ax-addrcl 8104

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9119

This theorem is referenced by:  nn1m1nn  9136  nn1suc  9137  nnaddcl  9138  nnmulcl  9139  nnsub  9157  nndiv  9159  nndivtr  9160  nnnn0addcl  9407  nn0nnaddcl  9408  elnnnn0  9420  nnnegz  9457  zaddcllempos  9491  zaddcllemneg  9493  nnaddm1cl  9516  elz2  9526  zdiv  9543  zdivadd  9544  zdivmul  9545  nneoor  9557  nneo  9558  divfnzn  9824  qmulz  9826  qaddcl  9838  qnegcl  9839  qmulcl  9840  qreccl  9845  nnledivrp  9970  nn0ledivnn  9971  fseq1m1p1  10299  nnsplit  10341  ubmelm1fzo  10440  subfzo0  10456  flqdiv  10551  addmodidr  10603  modfzo0difsn  10625  nn0ennn  10663  expnegap0  10777  expm1t  10797  nnsqcl  10839  nnlesq  10873  facdiv  10968  facndiv  10969  faclbnd  10971  bcn1  10988  bcn2m1  10999  arisum  12017  arisum2  12018  expcnvap0  12021  mertenslem2  12055  ef0lem  12179  efexp  12201  nndivides  12316  modmulconst  12342  dvdsflip  12370  nn0enne  12421  nno  12425  divalgmod  12446  ndvdsadd  12450  modgcd  12520  gcddiv  12548  gcdmultiple  12549  gcdmultiplez  12550  rpmulgcd  12555  rplpwr  12556  sqgcd  12558  lcmgcdlem  12607  qredeq  12626  qredeu  12627  divgcdcoprm0  12631  cncongrcoprm  12636  prmind2  12650  isprm6  12677  sqrt2irr  12692  oddpwdclemodd  12702  divnumden  12726  divdenle  12727  nn0gcdsq  12730  hashgcdlem  12768  pythagtriplem1  12796  pythagtriplem2  12797  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem15  12809  pythagtriplem16  12810  pythagtriplem17  12811  pythagtriplem19  12813  pcqcl  12837  pcexp  12840  pcneg  12856  fldivp1  12879  oddprmdvds  12885  prmpwdvds  12886  infpnlem2  12891  4sqlem19  12940  mulgnegnn  13677  mulgnnass  13702  mulgmodid  13706  cnfldmulg  14548  znidomb  14630  znrrg  14632  dvexp  15393  rpcxproot  15596  logbgcd1irr  15649  perfect  15683  lgssq2  15728  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  2lgslem1a1  15773  2sqlem6  15807  2sqlem10  15812