Theorem nncn 9313

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

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

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 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

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 9306

This theorem is used by:  nn1m1nn  9323  nn1suc  9324  nnaddcl  9325  nnmulcl  9326  nnsub  9344  nndiv  9346  nndivtr  9347  nnnn0addcl  9595  nn0nnaddcl  9596  elnnnn0  9608  nnnegz  9649  zaddcllempos  9683  zaddcllemneg  9685  nnaddm1cl  9708  elz2  9718  zdiv  9736  zdivadd  9737  zdivmul  9738  nneoor  9750  nneo  9751  divfnzn  10023  qmulz  10025  qaddcl  10037  qnegcl  10038  qmulcl  10039  qreccl  10044  nnledivrp  10169  nn0ledivnn  10170  fseq1m1p1  10504  nnsplit  10546  ubmelm1fzo  10646  subfzo0  10663  flqdiv  10760  addmodidr  10812  modfzo0difsn  10834  nn0ennn  10872  expnegap0  10986  expm1t  11006  nnsqcl  11048  nnlesq  11082  facdiv  11178  facndiv  11179  faclbnd  11181  bcn1  11198  bcn2m1  11210  arisum  12267  arisum2  12268  expcnvap0  12271  mertenslem2  12305  ef0lem  12429  efexp  12451  nndivides  12566  modmulconst  12592  dvdsflip  12620  nn0enne  12671  nno  12675  divalgmod  12696  ndvdsadd  12700  modgcd  12770  gcddiv  12798  gcdmultiple  12799  gcdmultiplez  12800  rpmulgcd  12805  rplpwr  12806  sqgcd  12808  lcmgcdlem  12857  qredeq  12876  qredeu  12877  divgcdcoprm0  12881  cncongrcoprm  12886  prmind2  12900  isprm6  12927  sqrt2irr  12942  oddpwdclemodd  12952  divnumden  12976  divdenle  12977  nn0gcdsq  12980  hashgcdlem  13018  pythagtriplem1  13046  pythagtriplem2  13047  pythagtriplem6  13051  pythagtriplem7  13052  pythagtriplem12  13056  pythagtriplem14  13058  pythagtriplem15  13059  pythagtriplem16  13060  pythagtriplem17  13061  pythagtriplem19  13063  pcqcl  13087  pcexp  13090  pcneg  13106  fldivp1  13129  oddprmdvds  13135  prmpwdvds  13136  infpnlem2  13141  4sqlem19  13190  mulgnegnn  13937  mulgnnass  13962  mulgmodid  13966  cnfldmulg  14915  znidomb  14995  znrrg  14997  dvexp  15814  rpcxproot  16022  logbgcd1irr  16075  birthdaylem2  16094  pellexlem1  16097  perfect  16121  pcbcctr  16123  bclbnd  16127  lgssq2  16172  gausslemma2dlem1a  16189  gausslemma2dlem3  16194  2lgslem1a1  16217  2sqlem6  16251  2sqlem10  16256