Theorem nncn 8957

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℂcc 7839  ℕcn 8949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4136  ax-cnex 7932  ax-resscn 7933  ax-1re 7935  ax-addrcl 7938

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754  df-in 3150  df-ss 3157  df-int 3860  df-inn 8950

This theorem is referenced by:  nn1m1nn  8967  nn1suc  8968  nnaddcl  8969  nnmulcl  8970  nnsub  8988  nndiv  8990  nndivtr  8991  nnnn0addcl  9236  nn0nnaddcl  9237  elnnnn0  9249  nnnegz  9286  zaddcllempos  9320  zaddcllemneg  9322  nnaddm1cl  9344  elz2  9354  zdiv  9371  zdivadd  9372  zdivmul  9373  nneoor  9385  nneo  9386  divfnzn  9651  qmulz  9653  qaddcl  9665  qnegcl  9666  qmulcl  9667  qreccl  9672  nnledivrp  9796  nn0ledivnn  9797  fseq1m1p1  10125  nnsplit  10167  ubmelm1fzo  10256  subfzo0  10272  flqdiv  10352  addmodidr  10404  modfzo0difsn  10426  nn0ennn  10464  expnegap0  10559  expm1t  10579  nnsqcl  10621  nnlesq  10655  facdiv  10750  facndiv  10751  faclbnd  10753  bcn1  10770  bcn2m1  10781  arisum  11538  arisum2  11539  expcnvap0  11542  mertenslem2  11576  ef0lem  11700  efexp  11722  nndivides  11836  modmulconst  11862  dvdsflip  11889  nn0enne  11939  nno  11943  divalgmod  11964  ndvdsadd  11968  modgcd  12024  gcddiv  12052  gcdmultiple  12053  gcdmultiplez  12054  rpmulgcd  12059  rplpwr  12060  sqgcd  12062  lcmgcdlem  12109  qredeq  12128  qredeu  12129  divgcdcoprm0  12133  cncongrcoprm  12138  prmind2  12152  isprm6  12179  sqrt2irr  12194  oddpwdclemodd  12204  divnumden  12228  divdenle  12229  nn0gcdsq  12232  hashgcdlem  12270  pythagtriplem1  12297  pythagtriplem2  12298  pythagtriplem6  12302  pythagtriplem7  12303  pythagtriplem12  12307  pythagtriplem14  12309  pythagtriplem15  12310  pythagtriplem16  12311  pythagtriplem17  12312  pythagtriplem19  12314  pcqcl  12338  pcexp  12341  pcneg  12357  fldivp1  12380  oddprmdvds  12386  prmpwdvds  12387  infpnlem2  12392  4sqlem19  12441  mulgnegnn  13072  mulgnnass  13097  mulgmodid  13101  cnfldmulg  13879  dvexp  14632  rpcxproot  14791  logbgcd1irr  14842  lgssq2  14900  2sqlem6  14925  2sqlem10  14930