Theorem nncn 12140

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11011  ℕcn 12132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11071  ax-addcl 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-nn 12133

This theorem is referenced by:  nncni  12142  nn1m1nn  12153  nn1suc  12154  nnaddcl  12155  nnmulcl  12156  nnmtmip  12158  nnneneg  12167  nnsub  12176  nndiv  12178  nndivtr  12179  nnnn0addcl  12418  nn0nnaddcl  12419  elnnnn0  12431  nn0sub  12438  nnnegz  12478  elz2  12493  zaddcl  12518  nnaddm1cl  12536  zdiv  12549  zdivadd  12550  zdivmul  12551  nneo  12563  peano5uzi  12568  elq  12850  qmulz  12851  qaddcl  12865  qnegcl  12866  qmulcl  12867  qreccl  12869  rpnnen1lem5  12881  nnledivrp  13006  nn0ledivnn  13007  fseq1m1p1  13501  ubmelm1fzo  13665  subfzo0  13694  quoremz  13761  quoremnn0ALT  13763  intfracq  13765  fldiv  13766  fldiv2  13767  modmulnn  13795  addmodid  13828  addmodidr  13829  modaddmodup  13843  modfzo0difsn  13852  modsumfzodifsn  13853  addmodlteq  13855  nn0ennn  13888  ser1const  13967  expneg  13978  expm1t  13999  nnsqcl  14037  nnlesq  14114  digit2  14145  digit1  14146  expnngt1  14150  facdiv  14196  facndiv  14197  faclbnd  14199  faclbnd4lem1  14202  faclbnd4lem4  14205  bcn1  14222  bcm1k  14224  bcp1n  14225  bcval5  14227  bcn2m1  14233  cshwidxmod  14712  cshwidxm  14717  cshwidxn  14718  repswcshw  14721  isercoll2  15578  divcnv  15762  harmonic  15768  arisum  15769  arisum2  15770  expcnv  15773  pwdif  15777  geomulcvg  15785  mertenslem2  15794  ef0lem  15987  efexp  16012  ruclem12  16152  sqrt2irr  16160  nndivides  16175  modmulconst  16201  dvdsflip  16230  nn0enne  16290  nno  16295  pwp1fsum  16304  divalgmod  16319  ndvdsadd  16323  modgcd  16445  gcdmultiplez  16448  gcddiv  16464  rpmulgcd  16470  rplpwr  16471  sqgcd  16475  expgcd  16476  nn0expgcd  16477  lcmgcdlem  16519  qredeq  16570  qredeu  16571  cncongrcoprm  16583  prmind2  16598  isprm6  16627  divnumden  16661  divdenle  16662  nn0gcdsq  16665  hashgcdlem  16701  pythagtriplem1  16730  pythagtriplem2  16731  pythagtriplem6  16735  pythagtriplem7  16736  pythagtriplem12  16740  pythagtriplem14  16742  pythagtriplem15  16743  pythagtriplem16  16744  pythagtriplem17  16745  pythagtriplem19  16747  pcqcl  16770  pcexp  16773  pcneg  16788  fldivp1  16811  oddprmdvds  16817  prmpwdvds  16818  infpnlem2  16825  prmreclem1  16830  prmreclem6  16835  4sqlem19  16877  vdwapun  16888  vdwapid1  16889  prmonn2  16953  prmgaplem7  16971  mulgnegnn  18999  mulgnnass  19024  mulgmodid  19028  odmod  19460  cnfldmulg  21342  prmirredlem  21411  znidomb  21500  znrrg  21504  cply1mul  22212  chfacfscmul0  22774  chfacfscmulfsupp  22775  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulfsupp  22779  chfacfpmmulgsum  22780  cayhamlem1  22782  cpmadugsumlemF  22792  ovolunlem1  25426  uniioombllem3  25514  vitali  25542  mbfi1fseqlem3  25646  dvexp  25885  dvexp3  25910  plyeq0lem  26143  dgrcolem1  26207  aaliou3lem2  26279  aaliou3lem7  26285  pserdv2  26368  abelthlem6  26374  logtayl  26597  logtaylsum  26598  logtayl2  26599  cxpexp  26605  cxproot  26627  root1id  26692  root1eq1  26693  cxpeq  26695  logbgcd1irr  26732  atantayl  26875  atantayl2  26876  birthdaylem2  26890  dfef2  26909  emcllem2  26935  emcllem3  26936  zetacvg  26953  lgam1  27002  gamfac  27005  basellem2  27020  basellem3  27021  basellem5  27023  basellem8  27026  mumul  27119  fsumdvdscom  27123  muinv  27131  chtublem  27150  perfect  27170  pcbcctr  27215  bclbnd  27219  bposlem1  27223  bposlem6  27228  lgssq2  27277  gausslemma2dlem1a  27304  gausslemma2dlem3  27307  2lgslem1a1  27328  2sqlem6  27362  2sqlem10  27367  2sqnn  27378  2sqreunnltlem  27389  rplogsumlem1  27423  dchrmusumlema  27432  dchrmusum2  27433  dchrvmasumiflem1  27440  dchrvmaeq0  27443  dchrisum0re  27452  logdivbnd  27495  cusgrsize2inds  29434  wlkdlem2  29662  crctcshwlkn0lem1  29790  crctcshwlkn0lem6  29795  0enwwlksnge1  29844  wspthsnonn0vne  29897  clwwlknwwlksn  30020  clwwlkinwwlk  30022  clwwlkel  30028  clwwlkf  30029  clwwlkf1  30031  wwlksubclwwlk  30040  eucrctshift  30225  eucrct2eupth  30227  numclwwlk2lem1  30358  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  ipasslem4  30816  ipasslem5  30817  isarchi3  33163  oddpwdc  34388  eulerpartlemb  34402  fibp1  34435  subfacp1lem6  35250  subfaclim  35253  snmlff  35394  circum  35739  divcnvlin  35798  bcprod  35803  iprodgam  35807  faclim  35811  faclim2  35813  nn0prpwlem  36387  nndivsub  36522  knoppndvlem13  36589  poimirlem13  37693  poimirlem14  37694  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  mblfinlem2  37718  ovoliunnfl  37722  voliunnfl  37724  facp2  42256  nnadd1com  42385  nnaddcom  42386  dvdsexpnn0  42452  renegmulnnass  42583  fimgmcyc  42652  dffltz  42752  irrapxlem1  42939  pellexlem1  42946  pellqrex  42996  2nn0ind  43062  jm2.17c  43079  acongrep  43097  jm2.18  43105  jm2.20nn  43114  jm2.16nn0  43121  proot1ex  43313  hashnzfzclim  44439  binomcxplemnotnn0  44473  nnsplit  45481  clim1fr1  45725  sumnnodd  45754  wallispilem4  46190  wallispilem5  46191  wallispi  46192  wallispi2lem1  46193  wallispi2lem2  46194  wallispi2  46195  stirlinglem1  46196  stirlinglem3  46198  stirlinglem4  46199  stirlinglem5  46200  stirlinglem6  46201  stirlinglem7  46202  stirlinglem8  46203  stirlinglem10  46205  stirlinglem11  46206  stirlinglem12  46207  stirlinglem13  46208  stirlinglem14  46209  stirlinglem15  46210  dirkerper  46218  dirkertrigeqlem1  46220  fouriersw  46353  nnfoctbdjlem  46577  deccarry  47435  subsubelfzo0  47450  submodlt  47474  mod0mul  47480  m1modmmod  47482  modlt0b  47487  sqrtpwpw2p  47662  fmtnodvds  47668  fmtnoprmfac1  47689  fmtnoprmfac2lem1  47690  fmtnoprmfac2  47691  lighneallem2  47730  lighneallem3  47731  lighneallem4  47734  nnennexALTV  47825  perfectALTV  47847  fppr2odd  47855  fpprwppr  47863  fpprwpprb  47864  tgoldbachlt  47940  gpgedgvtx0  48185  gpg3kgrtriexlem2  48208  gpg3kgrtriexlem5  48211  gpg3kgrtriex  48213  nnsgrp  48301  nnsgrpnmnd  48302  bcpascm1  48475  altgsumbcALT  48477  eluz2cnn0n1  48636  pw2m1lepw2m1  48645  nnennex  48650  logbpw2m1  48692  blenpw2m1  48704  nnpw2blen  48705  nnpw2pmod  48708  blennnt2  48714  blennn0em1  48716  nn0digval  48725  dignn0fr  48726  dignn0ldlem  48727  dig0  48731  nn0sumshdiglemA  48744  nn0sumshdiglemB  48745  nn0sumshdiglem1  48746