Theorem nncn 9265

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  ℕcn 9257

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9258

This theorem is referenced by:  nn1m1nn  9275  nn1suc  9276  nnaddcl  9277  nnmulcl  9278  nnsub  9296  nndiv  9298  nndivtr  9299  nnnn0addcl  9546  nn0nnaddcl  9547  elnnnn0  9559  nnnegz  9600  zaddcllempos  9634  zaddcllemneg  9636  nnaddm1cl  9659  elz2  9669  zdiv  9687  zdivadd  9688  zdivmul  9689  nneoor  9701  nneo  9702  divfnzn  9974  qmulz  9976  qaddcl  9988  qnegcl  9989  qmulcl  9990  qreccl  9995  nnledivrp  10120  nn0ledivnn  10121  fseq1m1p1  10454  nnsplit  10496  ubmelm1fzo  10596  subfzo0  10613  flqdiv  10710  addmodidr  10762  modfzo0difsn  10784  nn0ennn  10822  expnegap0  10936  expm1t  10956  nnsqcl  10998  nnlesq  11032  facdiv  11128  facndiv  11129  faclbnd  11131  bcn1  11148  bcn2m1  11160  arisum  12212  arisum2  12213  expcnvap0  12216  mertenslem2  12250  ef0lem  12374  efexp  12396  nndivides  12511  modmulconst  12537  dvdsflip  12565  nn0enne  12616  nno  12620  divalgmod  12641  ndvdsadd  12645  modgcd  12715  gcddiv  12743  gcdmultiple  12744  gcdmultiplez  12745  rpmulgcd  12750  rplpwr  12751  sqgcd  12753  lcmgcdlem  12802  qredeq  12821  qredeu  12822  divgcdcoprm0  12826  cncongrcoprm  12831  prmind2  12845  isprm6  12872  sqrt2irr  12887  oddpwdclemodd  12897  divnumden  12921  divdenle  12922  nn0gcdsq  12925  hashgcdlem  12963  pythagtriplem1  12991  pythagtriplem2  12992  pythagtriplem6  12996  pythagtriplem7  12997  pythagtriplem12  13001  pythagtriplem14  13003  pythagtriplem15  13004  pythagtriplem16  13005  pythagtriplem17  13006  pythagtriplem19  13008  pcqcl  13032  pcexp  13035  pcneg  13051  fldivp1  13074  oddprmdvds  13080  prmpwdvds  13081  infpnlem2  13086  4sqlem19  13135  mulgnegnn  13888  mulgnnass  13913  mulgmodid  13917  cnfldmulg  14853  znidomb  14935  znrrg  14937  dvexp  15705  rpcxproot  15908  logbgcd1irr  15961  pellexlem1  15974  perfect  15998  lgssq2  16043  gausslemma2dlem1a  16060  gausslemma2dlem3  16065  2lgslem1a1  16088  2sqlem6  16122  2sqlem10  16127