Theorem nncn 9315

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

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

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 4249  ax-cnex 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

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 9308

This theorem is used by:  nn1m1nn  9325  nn1suc  9326  nnaddcl  9327  nnmulcl  9328  nnsub  9346  nndiv  9348  nndivtr  9349  nnnn0addcl  9598  nn0nnaddcl  9599  elnnnn0  9611  nnnegz  9652  zaddcllempos  9686  zaddcllemneg  9688  nnaddm1cl  9711  elz2  9721  zdiv  9739  zdivadd  9740  zdivmul  9741  nneoor  9753  nneo  9754  divfnzn  10031  qmulz  10033  qaddcl  10045  qnegcl  10046  qmulcl  10047  qreccl  10052  nnledivrp  10178  nn0ledivnn  10179  fseq1m1p1  10513  nnsplit  10555  ubmelm1fzo  10655  subfzo0  10672  flqdiv  10772  addmodidr  10824  modfzo0difsn  10846  nn0ennn  10884  expnegap0  10998  expm1t  11018  nnsqcl  11060  nnlesq  11094  facdiv  11191  facndiv  11192  faclbnd  11194  bcn1  11211  bcn2m1  11223  arisum  12283  arisum2  12284  expcnvap0  12287  mertenslem2  12321  ef0lem  12445  efexp  12467  nndivides  12582  modmulconst  12608  dvdsflip  12636  nn0enne  12687  nno  12691  divalgmod  12712  ndvdsadd  12716  modgcd  12786  gcddiv  12814  gcdmultiple  12815  gcdmultiplez  12816  rpmulgcd  12821  rplpwr  12822  sqgcd  12824  lcmgcdlem  12873  qredeq  12892  qredeu  12893  divgcdcoprm0  12897  cncongrcoprm  12902  prmind2  12916  isprm6  12944  sqrt2irr  12959  divnumden  12994  divdenle  12995  nn0gcdsq  12998  hashgcdlem  13038  pythagtriplem1  13066  pythagtriplem2  13067  pythagtriplem6  13071  pythagtriplem7  13072  pythagtriplem12  13076  pythagtriplem14  13078  pythagtriplem15  13079  pythagtriplem16  13080  pythagtriplem17  13081  pythagtriplem19  13083  pcqcl  13107  pcexp  13110  pcneg  13126  fldivp1  13149  oddprmdvds  13155  prmpwdvds  13156  infpnlem2  13161  4sqlem19  13210  mulgnegnn  13986  mulgnnass  14011  mulgmodid  14015  cnfldmulg  14964  znidomb  15044  znrrg  15046  dvexp  15864  rpcxproot  16072  logbgcd1irr  16125  birthdaylem2  16148  pellexlem1  16151  chtublem  16217  perfect  16223  pcbcctr  16225  bclbnd  16229  bposlem1  16233  lgssq2  16282  gausslemma2dlem1a  16299  gausslemma2dlem3  16304  2lgslem1a1  16327  2sqlem6  16361  2sqlem10  16366