Theorem nncn 8586

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

Syntax hints:   → wi 4   ∈ wcel 1448  ℂcc 7498  ℕcn 8578

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-cnex 7586  ax-resscn 7587  ax-1re 7589  ax-addrcl 7592

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-v 2643  df-in 3027  df-ss 3034  df-int 3719  df-inn 8579

This theorem is referenced by:  nn1m1nn  8596  nn1suc  8597  nnaddcl  8598  nnmulcl  8599  nnsub  8617  nndiv  8619  nndivtr  8620  nnnn0addcl  8859  nn0nnaddcl  8860  elnnnn0  8872  nnnegz  8909  zaddcllempos  8943  zaddcllemneg  8945  nnaddm1cl  8967  elz2  8974  zdiv  8991  zdivadd  8992  zdivmul  8993  nneoor  9005  nneo  9006  divfnzn  9263  qmulz  9265  qaddcl  9277  qnegcl  9278  qmulcl  9279  qreccl  9284  nnledivrp  9394  nn0ledivnn  9395  fseq1m1p1  9716  nnsplit  9755  ubmelm1fzo  9844  subfzo0  9860  flqdiv  9935  addmodidr  9987  modfzo0difsn  10009  nn0ennn  10047  expnegap0  10142  expm1t  10162  nnsqcl  10203  nnlesq  10237  facdiv  10325  facndiv  10326  faclbnd  10328  bcn1  10345  bcn2m1  10356  arisum  11106  arisum2  11107  expcnvap0  11110  mertenslem2  11144  ef0lem  11164  efexp  11186  nndivides  11295  modmulconst  11320  dvdsflip  11344  nn0enne  11394  nno  11398  divalgmod  11419  ndvdsadd  11423  modgcd  11474  gcddiv  11500  gcdmultiple  11501  gcdmultiplez  11502  rpmulgcd  11507  rplpwr  11508  sqgcd  11510  lcmgcdlem  11551  qredeq  11570  qredeu  11571  divgcdcoprm0  11575  cncongrcoprm  11580  prmind2  11594  isprm6  11618  sqrt2irr  11633  oddpwdclemodd  11642  divnumden  11666  divdenle  11667  nn0gcdsq  11670  hashgcdlem  11695