Theorem nncn 8728

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7618  ℕcn 8720

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-cnex 7711  ax-resscn 7712  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-v 2688  df-in 3077  df-ss 3084  df-int 3772  df-inn 8721

This theorem is referenced by:  nn1m1nn  8738  nn1suc  8739  nnaddcl  8740  nnmulcl  8741  nnsub  8759  nndiv  8761  nndivtr  8762  nnnn0addcl  9007  nn0nnaddcl  9008  elnnnn0  9020  nnnegz  9057  zaddcllempos  9091  zaddcllemneg  9093  nnaddm1cl  9115  elz2  9122  zdiv  9139  zdivadd  9140  zdivmul  9141  nneoor  9153  nneo  9154  divfnzn  9413  qmulz  9415  qaddcl  9427  qnegcl  9428  qmulcl  9429  qreccl  9434  nnledivrp  9553  nn0ledivnn  9554  fseq1m1p1  9875  nnsplit  9914  ubmelm1fzo  10003  subfzo0  10019  flqdiv  10094  addmodidr  10146  modfzo0difsn  10168  nn0ennn  10206  expnegap0  10301  expm1t  10321  nnsqcl  10362  nnlesq  10396  facdiv  10484  facndiv  10485  faclbnd  10487  bcn1  10504  bcn2m1  10515  arisum  11267  arisum2  11268  expcnvap0  11271  mertenslem2  11305  ef0lem  11366  efexp  11388  nndivides  11500  modmulconst  11525  dvdsflip  11549  nn0enne  11599  nno  11603  divalgmod  11624  ndvdsadd  11628  modgcd  11679  gcddiv  11707  gcdmultiple  11708  gcdmultiplez  11709  rpmulgcd  11714  rplpwr  11715  sqgcd  11717  lcmgcdlem  11758  qredeq  11777  qredeu  11778  divgcdcoprm0  11782  cncongrcoprm  11787  prmind2  11801  isprm6  11825  sqrt2irr  11840  oddpwdclemodd  11850  divnumden  11874  divdenle  11875  nn0gcdsq  11878  hashgcdlem  11903  dvexp  12844