Theorem nncn 8886

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  ℕcn 8878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107  ax-cnex 7865  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-in 3127  df-ss 3134  df-int 3832  df-inn 8879

This theorem is referenced by:  nn1m1nn  8896  nn1suc  8897  nnaddcl  8898  nnmulcl  8899  nnsub  8917  nndiv  8919  nndivtr  8920  nnnn0addcl  9165  nn0nnaddcl  9166  elnnnn0  9178  nnnegz  9215  zaddcllempos  9249  zaddcllemneg  9251  nnaddm1cl  9273  elz2  9283  zdiv  9300  zdivadd  9301  zdivmul  9302  nneoor  9314  nneo  9315  divfnzn  9580  qmulz  9582  qaddcl  9594  qnegcl  9595  qmulcl  9596  qreccl  9601  nnledivrp  9723  nn0ledivnn  9724  fseq1m1p1  10051  nnsplit  10093  ubmelm1fzo  10182  subfzo0  10198  flqdiv  10277  addmodidr  10329  modfzo0difsn  10351  nn0ennn  10389  expnegap0  10484  expm1t  10504  nnsqcl  10545  nnlesq  10579  facdiv  10672  facndiv  10673  faclbnd  10675  bcn1  10692  bcn2m1  10703  arisum  11461  arisum2  11462  expcnvap0  11465  mertenslem2  11499  ef0lem  11623  efexp  11645  nndivides  11759  modmulconst  11785  dvdsflip  11811  nn0enne  11861  nno  11865  divalgmod  11886  ndvdsadd  11890  modgcd  11946  gcddiv  11974  gcdmultiple  11975  gcdmultiplez  11976  rpmulgcd  11981  rplpwr  11982  sqgcd  11984  lcmgcdlem  12031  qredeq  12050  qredeu  12051  divgcdcoprm0  12055  cncongrcoprm  12060  prmind2  12074  isprm6  12101  sqrt2irr  12116  oddpwdclemodd  12126  divnumden  12150  divdenle  12151  nn0gcdsq  12154  hashgcdlem  12192  pythagtriplem1  12219  pythagtriplem2  12220  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem17  12234  pythagtriplem19  12236  pcqcl  12260  pcexp  12263  pcneg  12278  fldivp1  12300  oddprmdvds  12306  prmpwdvds  12307  infpnlem2  12312  dvexp  13469  rpcxproot  13628  logbgcd1irr  13679  lgssq2  13736  2sqlem6  13750  2sqlem10  13755