Theorem nncn 9156

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℂcc 8035  ℕcn 9148

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-sep 4208  ax-cnex 8128  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-v 2803  df-in 3205  df-ss 3212  df-int 3930  df-inn 9149

This theorem is referenced by:  nn1m1nn  9166  nn1suc  9167  nnaddcl  9168  nnmulcl  9169  nnsub  9187  nndiv  9189  nndivtr  9190  nnnn0addcl  9437  nn0nnaddcl  9438  elnnnn0  9450  nnnegz  9487  zaddcllempos  9521  zaddcllemneg  9523  nnaddm1cl  9546  elz2  9556  zdiv  9573  zdivadd  9574  zdivmul  9575  nneoor  9587  nneo  9588  divfnzn  9860  qmulz  9862  qaddcl  9874  qnegcl  9875  qmulcl  9876  qreccl  9881  nnledivrp  10006  nn0ledivnn  10007  fseq1m1p1  10335  nnsplit  10377  ubmelm1fzo  10477  subfzo0  10494  flqdiv  10589  addmodidr  10641  modfzo0difsn  10663  nn0ennn  10701  expnegap0  10815  expm1t  10835  nnsqcl  10877  nnlesq  10911  facdiv  11006  facndiv  11007  faclbnd  11009  bcn1  11026  bcn2m1  11037  arisum  12082  arisum2  12083  expcnvap0  12086  mertenslem2  12120  ef0lem  12244  efexp  12266  nndivides  12381  modmulconst  12407  dvdsflip  12435  nn0enne  12486  nno  12490  divalgmod  12511  ndvdsadd  12515  modgcd  12585  gcddiv  12613  gcdmultiple  12614  gcdmultiplez  12615  rpmulgcd  12620  rplpwr  12621  sqgcd  12623  lcmgcdlem  12672  qredeq  12691  qredeu  12692  divgcdcoprm0  12696  cncongrcoprm  12701  prmind2  12715  isprm6  12742  sqrt2irr  12757  oddpwdclemodd  12767  divnumden  12791  divdenle  12792  nn0gcdsq  12795  hashgcdlem  12833  pythagtriplem1  12861  pythagtriplem2  12862  pythagtriplem6  12866  pythagtriplem7  12867  pythagtriplem12  12871  pythagtriplem14  12873  pythagtriplem15  12874  pythagtriplem16  12875  pythagtriplem17  12876  pythagtriplem19  12878  pcqcl  12902  pcexp  12905  pcneg  12921  fldivp1  12944  oddprmdvds  12950  prmpwdvds  12951  infpnlem2  12956  4sqlem19  13005  mulgnegnn  13742  mulgnnass  13767  mulgmodid  13771  cnfldmulg  14614  znidomb  14696  znrrg  14698  dvexp  15464  rpcxproot  15667  logbgcd1irr  15720  perfect  15754  lgssq2  15799  gausslemma2dlem1a  15816  gausslemma2dlem3  15821  2lgslem1a1  15844  2sqlem6  15878  2sqlem10  15883