Theorem nncn 9295

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8171  ℕcn 9287

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 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 4247  ax-cnex 8264  ax-resscn 8265  ax-1re 8267  ax-addrcl 8270

This theorem 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 3969  df-inn 9288

This theorem is referenced by:  nn1m1nn  9305  nn1suc  9306  nnaddcl  9307  nnmulcl  9308  nnsub  9326  nndiv  9328  nndivtr  9329  nnnn0addcl  9576  nn0nnaddcl  9577  elnnnn0  9589  nnnegz  9630  zaddcllempos  9664  zaddcllemneg  9666  nnaddm1cl  9689  elz2  9699  zdiv  9717  zdivadd  9718  zdivmul  9719  nneoor  9731  nneo  9732  divfnzn  10004  qmulz  10006  qaddcl  10018  qnegcl  10019  qmulcl  10020  qreccl  10025  nnledivrp  10150  nn0ledivnn  10151  fseq1m1p1  10485  nnsplit  10527  ubmelm1fzo  10627  subfzo0  10644  flqdiv  10741  addmodidr  10793  modfzo0difsn  10815  nn0ennn  10853  expnegap0  10967  expm1t  10987  nnsqcl  11029  nnlesq  11063  facdiv  11159  facndiv  11160  faclbnd  11162  bcn1  11179  bcn2m1  11191  arisum  12248  arisum2  12249  expcnvap0  12252  mertenslem2  12286  ef0lem  12410  efexp  12432  nndivides  12547  modmulconst  12573  dvdsflip  12601  nn0enne  12652  nno  12656  divalgmod  12677  ndvdsadd  12681  modgcd  12751  gcddiv  12779  gcdmultiple  12780  gcdmultiplez  12781  rpmulgcd  12786  rplpwr  12787  sqgcd  12789  lcmgcdlem  12838  qredeq  12857  qredeu  12858  divgcdcoprm0  12862  cncongrcoprm  12867  prmind2  12881  isprm6  12908  sqrt2irr  12923  oddpwdclemodd  12933  divnumden  12957  divdenle  12958  nn0gcdsq  12961  hashgcdlem  12999  pythagtriplem1  13027  pythagtriplem2  13028  pythagtriplem6  13032  pythagtriplem7  13033  pythagtriplem12  13037  pythagtriplem14  13039  pythagtriplem15  13040  pythagtriplem16  13041  pythagtriplem17  13042  pythagtriplem19  13044  pcqcl  13068  pcexp  13071  pcneg  13087  fldivp1  13110  oddprmdvds  13116  prmpwdvds  13117  infpnlem2  13122  4sqlem19  13171  mulgnegnn  13918  mulgnnass  13943  mulgmodid  13947  cnfldmulg  14896  znidomb  14976  znrrg  14978  dvexp  15795  rpcxproot  15999  logbgcd1irr  16052  birthdaylem2  16071  pellexlem1  16074  perfect  16098  lgssq2  16143  gausslemma2dlem1a  16160  gausslemma2dlem3  16165  2lgslem1a1  16188  2sqlem6  16222  2sqlem10  16227