Theorem nncn 8929

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7811  ℕcn 8921

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123  ax-cnex 7904  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2741  df-in 3137  df-ss 3144  df-int 3847  df-inn 8922

This theorem is referenced by:  nn1m1nn  8939  nn1suc  8940  nnaddcl  8941  nnmulcl  8942  nnsub  8960  nndiv  8962  nndivtr  8963  nnnn0addcl  9208  nn0nnaddcl  9209  elnnnn0  9221  nnnegz  9258  zaddcllempos  9292  zaddcllemneg  9294  nnaddm1cl  9316  elz2  9326  zdiv  9343  zdivadd  9344  zdivmul  9345  nneoor  9357  nneo  9358  divfnzn  9623  qmulz  9625  qaddcl  9637  qnegcl  9638  qmulcl  9639  qreccl  9644  nnledivrp  9768  nn0ledivnn  9769  fseq1m1p1  10097  nnsplit  10139  ubmelm1fzo  10228  subfzo0  10244  flqdiv  10323  addmodidr  10375  modfzo0difsn  10397  nn0ennn  10435  expnegap0  10530  expm1t  10550  nnsqcl  10592  nnlesq  10626  facdiv  10720  facndiv  10721  faclbnd  10723  bcn1  10740  bcn2m1  10751  arisum  11508  arisum2  11509  expcnvap0  11512  mertenslem2  11546  ef0lem  11670  efexp  11692  nndivides  11806  modmulconst  11832  dvdsflip  11859  nn0enne  11909  nno  11913  divalgmod  11934  ndvdsadd  11938  modgcd  11994  gcddiv  12022  gcdmultiple  12023  gcdmultiplez  12024  rpmulgcd  12029  rplpwr  12030  sqgcd  12032  lcmgcdlem  12079  qredeq  12098  qredeu  12099  divgcdcoprm0  12103  cncongrcoprm  12108  prmind2  12122  isprm6  12149  sqrt2irr  12164  oddpwdclemodd  12174  divnumden  12198  divdenle  12199  nn0gcdsq  12202  hashgcdlem  12240  pythagtriplem1  12267  pythagtriplem2  12268  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem15  12280  pythagtriplem16  12281  pythagtriplem17  12282  pythagtriplem19  12284  pcqcl  12308  pcexp  12311  pcneg  12326  fldivp1  12348  oddprmdvds  12354  prmpwdvds  12355  infpnlem2  12360  mulgnegnn  12998  mulgnnass  13023  mulgmodid  13027  cnfldmulg  13509  dvexp  14214  rpcxproot  14373  logbgcd1irr  14424  lgssq2  14481  2sqlem6  14506  2sqlem10  14511