Theorem nncn 9322

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8184  ℕcn 9314

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8277  ax-resscn 8278  ax-1re 8280  ax-addrcl 8283

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9315

This theorem is used by:  nn1m1nn  9332  nn1suc  9333  nnaddcl  9334  nnmulcl  9335  nnsub  9353  nndiv  9355  nndivtr  9356  nnnn0addcl  9605  nn0nnaddcl  9606  elnnnn0  9618  nnnegz  9659  zaddcllempos  9693  zaddcllemneg  9695  nnaddm1cl  9718  elz2  9728  zdiv  9746  zdivadd  9747  zdivmul  9748  nneoor  9760  nneo  9761  divfnzn  10038  qmulz  10040  qaddcl  10052  qnegcl  10053  qmulcl  10054  qreccl  10059  nnledivrp  10185  nn0ledivnn  10186  fseq1m1p1  10520  nnsplit  10562  ubmelm1fzo  10662  subfzo0  10679  flqdiv  10780  addmodidr  10832  modfzo0difsn  10854  nn0ennn  10892  expnegap0  11006  expm1t  11026  nnsqcl  11068  nnlesq  11102  facdiv  11199  facndiv  11200  faclbnd  11202  bcn1  11219  bcn2m1  11231  arisum  12291  arisum2  12292  expcnvap0  12295  mertenslem2  12329  ef0lem  12453  efexp  12475  nndivides  12590  modmulconst  12616  dvdsflip  12644  nn0enne  12695  nno  12699  divalgmod  12720  ndvdsadd  12724  modgcd  12794  gcddiv  12822  gcdmultiple  12823  gcdmultiplez  12824  rpmulgcd  12829  rplpwr  12830  sqgcd  12832  lcmgcdlem  12881  qredeq  12900  qredeu  12901  divgcdcoprm0  12905  cncongrcoprm  12910  prmind2  12924  isprm6  12952  sqrt2irr  12967  divnumden  13002  divdenle  13003  nn0gcdsq  13006  hashgcdlem  13046  pythagtriplem1  13074  pythagtriplem2  13075  pythagtriplem6  13079  pythagtriplem7  13080  pythagtriplem12  13084  pythagtriplem14  13086  pythagtriplem15  13087  pythagtriplem16  13088  pythagtriplem17  13089  pythagtriplem19  13091  pcqcl  13115  pcexp  13118  pcneg  13134  fldivp1  13157  oddprmdvds  13163  prmpwdvds  13164  infpnlem2  13169  4sqlem19  13218  mulgnegnn  13995  mulgnnass  14020  mulgmodid  14024  cnfldmulg  15023  znidomb  15103  znrrg  15105  dvexp  15949  root1idef  16096  rpcxproot  16159  efnthr  16188  logbgcd1irr  16215  birthdaylem2  16238  pellexlem1  16241  chtublem  16307  perfect  16313  pcbcctr  16315  bclbnd  16319  bposlem1  16323  bposlem6  16328  lgssq2  16377  gausslemma2dlem1a  16394  gausslemma2dlem3  16399  2lgslem1a1  16422  2sqlem6  16456  2sqlem10  16461