Theorem nncn 8865

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7751  ℕcn 8857

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4100  ax-cnex 7844  ax-resscn 7845  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-v 2728  df-in 3122  df-ss 3129  df-int 3825  df-inn 8858

This theorem is referenced by:  nn1m1nn  8875  nn1suc  8876  nnaddcl  8877  nnmulcl  8878  nnsub  8896  nndiv  8898  nndivtr  8899  nnnn0addcl  9144  nn0nnaddcl  9145  elnnnn0  9157  nnnegz  9194  zaddcllempos  9228  zaddcllemneg  9230  nnaddm1cl  9252  elz2  9262  zdiv  9279  zdivadd  9280  zdivmul  9281  nneoor  9293  nneo  9294  divfnzn  9559  qmulz  9561  qaddcl  9573  qnegcl  9574  qmulcl  9575  qreccl  9580  nnledivrp  9702  nn0ledivnn  9703  fseq1m1p1  10030  nnsplit  10072  ubmelm1fzo  10161  subfzo0  10177  flqdiv  10256  addmodidr  10308  modfzo0difsn  10330  nn0ennn  10368  expnegap0  10463  expm1t  10483  nnsqcl  10524  nnlesq  10558  facdiv  10651  facndiv  10652  faclbnd  10654  bcn1  10671  bcn2m1  10682  arisum  11439  arisum2  11440  expcnvap0  11443  mertenslem2  11477  ef0lem  11601  efexp  11623  nndivides  11737  modmulconst  11763  dvdsflip  11789  nn0enne  11839  nno  11843  divalgmod  11864  ndvdsadd  11868  modgcd  11924  gcddiv  11952  gcdmultiple  11953  gcdmultiplez  11954  rpmulgcd  11959  rplpwr  11960  sqgcd  11962  lcmgcdlem  12009  qredeq  12028  qredeu  12029  divgcdcoprm0  12033  cncongrcoprm  12038  prmind2  12052  isprm6  12079  sqrt2irr  12094  oddpwdclemodd  12104  divnumden  12128  divdenle  12129  nn0gcdsq  12132  hashgcdlem  12170  pythagtriplem1  12197  pythagtriplem2  12198  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem12  12207  pythagtriplem14  12209  pythagtriplem15  12210  pythagtriplem16  12211  pythagtriplem17  12212  pythagtriplem19  12214  pcqcl  12238  pcexp  12241  pcneg  12256  fldivp1  12278  oddprmdvds  12284  prmpwdvds  12285  infpnlem2  12290  dvexp  13315  rpcxproot  13474  logbgcd1irr  13525  lgssq2  13582  2sqlem6  13596  2sqlem10  13601