Theorem nncn 8047

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  ℕcn 8039

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-cnex 7067  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-v 2603  df-in 2979  df-ss 2986  df-int 3637  df-inn 8040

This theorem is referenced by:  nn1m1nn  8057  nn1suc  8058  nnaddcl  8059  nnmulcl  8060  nnsub  8077  nndiv  8079  nndivtr  8080  nnnn0addcl  8318  nn0nnaddcl  8319  elnnnn0  8331  nnnegz  8354  zaddcllempos  8388  zaddcllemneg  8390  nnaddm1cl  8412  elz2  8419  zdiv  8435  zdivadd  8436  zdivmul  8437  nneoor  8449  nneo  8450  divfnzn  8706  qmulz  8708  qaddcl  8720  qnegcl  8721  qmulcl  8722  qreccl  8727  nnledivrp  8837  nn0ledivnn  8838  fseq1m1p1  9112  ubmelm1fzo  9235  subfzo0  9251  flqdiv  9323  addmodidr  9375  modfzo0difsn  9397  nn0ennn  9425  expnegap0  9484  expm1t  9504  nnsqcl  9545  nnlesq  9578  facdiv  9665  facndiv  9666  faclbnd  9668  bcn1  9685  bcn2m1  9696  nndivides  10202  modmulconst  10227  dvdsflip  10251  nn0enne  10302  nno  10306  divalgmod  10327  ndvdsadd  10331  modgcd  10382  gcddiv  10408  gcdmultiple  10409  gcdmultiplez  10410  rpmulgcd  10415  rplpwr  10416  sqgcd  10418  lcmgcdlem  10459  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  cncongrcoprm  10488  prmind2  10502  isprm6  10526  sqrt2irr  10541  oddpwdclemodd  10550