Theorem nncn 9250

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8130  ℕcn 9242

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 2216  ax-sep 4230  ax-cnex 8223  ax-resscn 8224  ax-1re 8226  ax-addrcl 8229

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3219  df-ss 3226  df-int 3952  df-inn 9243

This theorem is referenced by:  nn1m1nn  9260  nn1suc  9261  nnaddcl  9262  nnmulcl  9263  nnsub  9281  nndiv  9283  nndivtr  9284  nnnn0addcl  9531  nn0nnaddcl  9532  elnnnn0  9544  nnnegz  9585  zaddcllempos  9619  zaddcllemneg  9621  nnaddm1cl  9644  elz2  9654  zdiv  9672  zdivadd  9673  zdivmul  9674  nneoor  9686  nneo  9687  divfnzn  9959  qmulz  9961  qaddcl  9973  qnegcl  9974  qmulcl  9975  qreccl  9980  nnledivrp  10105  nn0ledivnn  10106  fseq1m1p1  10436  nnsplit  10478  ubmelm1fzo  10578  subfzo0  10595  flqdiv  10690  addmodidr  10742  modfzo0difsn  10764  nn0ennn  10802  expnegap0  10916  expm1t  10936  nnsqcl  10978  nnlesq  11012  facdiv  11108  facndiv  11109  faclbnd  11111  bcn1  11128  bcn2m1  11140  arisum  12192  arisum2  12193  expcnvap0  12196  mertenslem2  12230  ef0lem  12354  efexp  12376  nndivides  12491  modmulconst  12517  dvdsflip  12545  nn0enne  12596  nno  12600  divalgmod  12621  ndvdsadd  12625  modgcd  12695  gcddiv  12723  gcdmultiple  12724  gcdmultiplez  12725  rpmulgcd  12730  rplpwr  12731  sqgcd  12733  lcmgcdlem  12782  qredeq  12801  qredeu  12802  divgcdcoprm0  12806  cncongrcoprm  12811  prmind2  12825  isprm6  12852  sqrt2irr  12867  oddpwdclemodd  12877  divnumden  12901  divdenle  12902  nn0gcdsq  12905  hashgcdlem  12943  pythagtriplem1  12971  pythagtriplem2  12972  pythagtriplem6  12976  pythagtriplem7  12977  pythagtriplem12  12981  pythagtriplem14  12983  pythagtriplem15  12984  pythagtriplem16  12985  pythagtriplem17  12986  pythagtriplem19  12988  pcqcl  13012  pcexp  13015  pcneg  13031  fldivp1  13054  oddprmdvds  13060  prmpwdvds  13061  infpnlem2  13066  4sqlem19  13115  mulgnegnn  13870  mulgnnass  13895  mulgmodid  13899  cnfldmulg  14773  znidomb  14855  znrrg  14857  dvexp  15625  rpcxproot  15828  logbgcd1irr  15881  pellexlem1  15894  perfect  15918  lgssq2  15963  gausslemma2dlem1a  15980  gausslemma2dlem3  15985  2lgslem1a1  16008  2sqlem6  16042  2sqlem10  16047