Theorem nncn 8368

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

Syntax hints:   → wi 4   ∈ wcel 1436  ℂcc 7295  ℕcn 8360

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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-cnex 7383  ax-resscn 7384  ax-1re 7386  ax-addrcl 7389

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-v 2617  df-in 2994  df-ss 3001  df-int 3674  df-inn 8361

This theorem is referenced by:  nn1m1nn  8378  nn1suc  8379  nnaddcl  8380  nnmulcl  8381  nnsub  8398  nndiv  8400  nndivtr  8401  nnnn0addcl  8639  nn0nnaddcl  8640  elnnnn0  8652  nnnegz  8689  zaddcllempos  8723  zaddcllemneg  8725  nnaddm1cl  8747  elz2  8754  zdiv  8770  zdivadd  8771  zdivmul  8772  nneoor  8784  nneo  8785  divfnzn  9041  qmulz  9043  qaddcl  9055  qnegcl  9056  qmulcl  9057  qreccl  9062  nnledivrp  9172  nn0ledivnn  9173  fseq1m1p1  9442  nnsplit  9479  ubmelm1fzo  9568  subfzo0  9584  flqdiv  9659  addmodidr  9711  modfzo0difsn  9733  nn0ennn  9771  expnegap0  9865  expm1t  9885  nnsqcl  9926  nnlesq  9959  facdiv  10046  facndiv  10047  faclbnd  10049  bcn1  10066  bcn2m1  10077  nndivides  10709  modmulconst  10734  dvdsflip  10758  nn0enne  10808  nno  10812  divalgmod  10833  ndvdsadd  10837  modgcd  10888  gcddiv  10914  gcdmultiple  10915  gcdmultiplez  10916  rpmulgcd  10921  rplpwr  10922  sqgcd  10924  lcmgcdlem  10965  qredeq  10984  qredeu  10985  divgcdcoprm0  10989  cncongrcoprm  10994  prmind2  11008  isprm6  11032  sqrt2irr  11047  oddpwdclemodd  11056  divnumden  11080  divdenle  11081  nn0gcdsq  11084  hashgcdlem  11109