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  9657  zaddcllempos  9691  zaddcllemneg  9693  nnaddm1cl  9716  elz2  9726  zdiv  9745  zdivadd  9746  zdivmul  9747  nneoor  9759  nneo  9760  divfnzn  10037  qmulz  10039  qaddcl  10051  qnegcl  10052  qmulcl  10053  qreccl  10058  nnledivrp  10184  nn0ledivnn  10185  fseq1m1p1  10519  nnsplit  10561  ubmelm1fzo  10661  subfzo0  10678  flqdiv  10779  addmodidr  10831  modfzo0difsn  10853  nn0ennn  10891  expnegap0  11005  expm1t  11025  nnsqcl  11067  nnlesq  11101  facdiv  11198  facndiv  11199  faclbnd  11201  bcn1  11218  bcn2m1  11230  arisum  12290  arisum2  12291  expcnvap0  12294  mertenslem2  12328  ef0lem  12452  efexp  12474  nndivides  12589  modmulconst  12615  dvdsflip  12643  nn0enne  12694  nno  12698  divalgmod  12719  ndvdsadd  12723  modgcd  12793  gcddiv  12821  gcdmultiple  12822  gcdmultiplez  12823  rpmulgcd  12828  rplpwr  12829  sqgcd  12831  lcmgcdlem  12880  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  cncongrcoprm  12909  prmind2  12923  isprm6  12951  sqrt2irr  12966  divnumden  13001  divdenle  13002  nn0gcdsq  13005  hashgcdlem  13045  pythagtriplem1  13073  pythagtriplem2  13074  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  pythagtriplem19  13090  pcqcl  13114  pcexp  13117  pcneg  13133  fldivp1  13156  oddprmdvds  13162  prmpwdvds  13163  infpnlem2  13168  4sqlem19  13217  mulgnegnn  13994  mulgnnass  14019  mulgmodid  14023  cnfldmulg  15022  znidomb  15102  znrrg  15104  dvexp  15970  root1idef  16117  rpcxproot  16180  efnthr  16209  logbgcd1irr  16236  birthdaylem2  16259  pellexlem1  16262  chtublem  16328  perfect  16334  pcbcctr  16336  bclbnd  16340  bposlem1  16344  bposlem6  16349  lgssq2  16398  gausslemma2dlem1a  16415  gausslemma2dlem3  16420  2lgslem1a1  16443  2sqlem6  16477  2sqlem10  16482