Theorem nncn 8324

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

Syntax hints:   → wi 4   ∈ wcel 1434  ℂcc 7251  ℕcn 8316

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-cnex 7339  ax-resscn 7340  ax-1re 7342  ax-addrcl 7345

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2614  df-in 2990  df-ss 2997  df-int 3663  df-inn 8317

This theorem is referenced by:  nn1m1nn  8334  nn1suc  8335  nnaddcl  8336  nnmulcl  8337  nnsub  8354  nndiv  8356  nndivtr  8357  nnnn0addcl  8595  nn0nnaddcl  8596  elnnnn0  8608  nnnegz  8649  zaddcllempos  8683  zaddcllemneg  8685  nnaddm1cl  8707  elz2  8714  zdiv  8730  zdivadd  8731  zdivmul  8732  nneoor  8744  nneo  8745  divfnzn  9001  qmulz  9003  qaddcl  9015  qnegcl  9016  qmulcl  9017  qreccl  9022  nnledivrp  9132  nn0ledivnn  9133  fseq1m1p1  9402  ubmelm1fzo  9526  subfzo0  9542  flqdiv  9617  addmodidr  9669  modfzo0difsn  9691  nn0ennn  9729  expnegap0  9800  expm1t  9820  nnsqcl  9861  nnlesq  9894  facdiv  9981  facndiv  9982  faclbnd  9984  bcn1  10001  bcn2m1  10012  nndivides  10583  modmulconst  10608  dvdsflip  10632  nn0enne  10682  nno  10686  divalgmod  10707  ndvdsadd  10711  modgcd  10762  gcddiv  10788  gcdmultiple  10789  gcdmultiplez  10790  rpmulgcd  10795  rplpwr  10796  sqgcd  10798  lcmgcdlem  10839  qredeq  10858  qredeu  10859  divgcdcoprm0  10863  cncongrcoprm  10868  prmind2  10882  isprm6  10906  sqrt2irr  10921  oddpwdclemodd  10930  divnumden  10954  divdenle  10955  nn0gcdsq  10958  hashgcdlem  10983