Theorem nncn 12165

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕcn 12157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158

This theorem is referenced by:  nncni  12167  nn1m1nn  12178  nn1suc  12179  nnaddcl  12180  nnmulcl  12181  nnmtmip  12183  nnneneg  12192  nnsub  12201  nndiv  12203  nndivtr  12204  nnnn0addcl  12443  nn0nnaddcl  12444  elnnnn0  12456  nn0sub  12463  nnnegz  12503  elz2  12518  zaddcl  12543  nnaddm1cl  12561  zdiv  12574  zdivadd  12575  zdivmul  12576  nneo  12588  peano5uzi  12593  elq  12875  qmulz  12876  qaddcl  12890  qnegcl  12891  qmulcl  12892  qreccl  12894  rpnnen1lem5  12906  nnledivrp  13031  nn0ledivnn  13032  fseq1m1p1  13527  ubmelm1fzo  13691  subfzo0  13720  quoremz  13787  quoremnn0ALT  13789  intfracq  13791  fldiv  13792  fldiv2  13793  modmulnn  13821  addmodid  13854  addmodidr  13855  modaddmodup  13869  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  nn0ennn  13914  ser1const  13993  expneg  14004  expm1t  14025  nnsqcl  14063  nnlesq  14140  digit2  14171  digit1  14172  expnngt1  14176  facdiv  14222  facndiv  14223  faclbnd  14225  faclbnd4lem1  14228  faclbnd4lem4  14231  bcn1  14248  bcm1k  14250  bcp1n  14251  bcval5  14253  bcn2m1  14259  cshwidxmod  14738  cshwidxm  14743  cshwidxn  14744  repswcshw  14747  isercoll2  15604  divcnv  15788  harmonic  15794  arisum  15795  arisum2  15796  expcnv  15799  pwdif  15803  geomulcvg  15811  mertenslem2  15820  ef0lem  16013  efexp  16038  ruclem12  16178  sqrt2irr  16186  nndivides  16201  modmulconst  16227  dvdsflip  16256  nn0enne  16316  nno  16321  pwp1fsum  16330  divalgmod  16345  ndvdsadd  16349  modgcd  16471  gcdmultiplez  16474  gcddiv  16490  rpmulgcd  16496  rplpwr  16497  sqgcd  16501  expgcd  16502  nn0expgcd  16503  lcmgcdlem  16545  qredeq  16596  qredeu  16597  cncongrcoprm  16609  prmind2  16624  isprm6  16653  divnumden  16687  divdenle  16688  nn0gcdsq  16691  hashgcdlem  16727  pythagtriplem1  16756  pythagtriplem2  16757  pythagtriplem6  16761  pythagtriplem7  16762  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem15  16769  pythagtriplem16  16770  pythagtriplem17  16771  pythagtriplem19  16773  pcqcl  16796  pcexp  16799  pcneg  16814  fldivp1  16837  oddprmdvds  16843  prmpwdvds  16844  infpnlem2  16851  prmreclem1  16856  prmreclem6  16861  4sqlem19  16903  vdwapun  16914  vdwapid1  16915  prmonn2  16979  prmgaplem7  16997  mulgnegnn  19026  mulgnnass  19051  mulgmodid  19055  odmod  19487  cnfldmulg  21370  prmirredlem  21439  znidomb  21528  znrrg  21532  cply1mul  22252  chfacfscmul0  22814  chfacfscmulfsupp  22815  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulfsupp  22819  chfacfpmmulgsum  22820  cayhamlem1  22822  cpmadugsumlemF  22832  ovolunlem1  25466  uniioombllem3  25554  vitali  25582  mbfi1fseqlem3  25686  dvexp  25925  dvexp3  25950  plyeq0lem  26183  dgrcolem1  26247  aaliou3lem2  26319  aaliou3lem7  26325  pserdv2  26408  abelthlem6  26414  logtayl  26637  logtaylsum  26638  logtayl2  26639  cxpexp  26645  cxproot  26667  root1id  26732  root1eq1  26733  cxpeq  26735  logbgcd1irr  26772  atantayl  26915  atantayl2  26916  birthdaylem2  26930  dfef2  26949  emcllem2  26975  emcllem3  26976  zetacvg  26993  lgam1  27042  gamfac  27045  basellem2  27060  basellem3  27061  basellem5  27063  basellem8  27066  mumul  27159  fsumdvdscom  27163  muinv  27171  chtublem  27190  perfect  27210  pcbcctr  27255  bclbnd  27259  bposlem1  27263  bposlem6  27268  lgssq2  27317  gausslemma2dlem1a  27344  gausslemma2dlem3  27347  2lgslem1a1  27368  2sqlem6  27402  2sqlem10  27407  2sqnn  27418  2sqreunnltlem  27429  rplogsumlem1  27463  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumiflem1  27480  dchrvmaeq0  27483  dchrisum0re  27492  logdivbnd  27535  cusgrsize2inds  29539  wlkdlem2  29767  crctcshwlkn0lem1  29895  crctcshwlkn0lem6  29900  0enwwlksnge1  29949  wspthsnonn0vne  30002  clwwlknwwlksn  30125  clwwlkinwwlk  30127  clwwlkel  30133  clwwlkf  30134  clwwlkf1  30136  wwlksubclwwlk  30145  eucrctshift  30330  eucrct2eupth  30332  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  ipasslem4  30921  ipasslem5  30922  isarchi3  33280  oddpwdc  34531  eulerpartlemb  34545  fibp1  34578  subfacp1lem6  35398  subfaclim  35401  snmlff  35542  circum  35887  divcnvlin  35946  bcprod  35951  iprodgam  35955  faclim  35959  faclim2  35961  nn0prpwlem  36535  nndivsub  36670  knoppndvlem13  36743  poimirlem13  37878  poimirlem14  37879  poimirlem29  37894  poimirlem30  37895  poimirlem31  37896  poimirlem32  37897  mblfinlem2  37903  ovoliunnfl  37907  voliunnfl  37909  facp2  42507  nnadd1com  42631  nnaddcom  42632  dvdsexpnn0  42698  renegmulnnass  42829  fimgmcyc  42898  dffltz  42986  irrapxlem1  43173  pellexlem1  43180  pellqrex  43230  2nn0ind  43296  jm2.17c  43313  acongrep  43331  jm2.18  43339  jm2.20nn  43348  jm2.16nn0  43355  proot1ex  43547  hashnzfzclim  44672  binomcxplemnotnn0  44706  nnsplit  45711  clim1fr1  45955  sumnnodd  45984  wallispilem4  46420  wallispilem5  46421  wallispi  46422  wallispi2lem1  46423  wallispi2lem2  46424  wallispi2  46425  stirlinglem1  46426  stirlinglem3  46428  stirlinglem4  46429  stirlinglem5  46430  stirlinglem6  46431  stirlinglem7  46432  stirlinglem8  46433  stirlinglem10  46435  stirlinglem11  46436  stirlinglem12  46437  stirlinglem13  46438  stirlinglem14  46439  stirlinglem15  46440  dirkerper  46448  dirkertrigeqlem1  46450  fouriersw  46583  nnfoctbdjlem  46807  deccarry  47665  subsubelfzo0  47680  submodlt  47704  mod0mul  47710  m1modmmod  47712  modlt0b  47717  sqrtpwpw2p  47892  fmtnodvds  47898  fmtnoprmfac1  47919  fmtnoprmfac2lem1  47920  fmtnoprmfac2  47921  lighneallem2  47960  lighneallem3  47961  lighneallem4  47964  nnennexALTV  48055  perfectALTV  48077  fppr2odd  48085  fpprwppr  48093  fpprwpprb  48094  tgoldbachlt  48170  gpgedgvtx0  48415  gpg3kgrtriexlem2  48438  gpg3kgrtriexlem5  48441  gpg3kgrtriex  48443  nnsgrp  48531  nnsgrpnmnd  48532  bcpascm1  48705  altgsumbcALT  48707  eluz2cnn0n1  48865  pw2m1lepw2m1  48874  nnennex  48879  logbpw2m1  48921  blenpw2m1  48933  nnpw2blen  48934  nnpw2pmod  48937  blennnt2  48943  blennn0em1  48945  nn0digval  48954  dignn0fr  48955  dignn0ldlem  48956  dig0  48960  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974  nn0sumshdiglem1  48975