Theorem nncn 12182

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

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

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175

This theorem is referenced by:  nncni  12184  nn1m1nn  12195  nn1suc  12196  nnaddcl  12197  nnmulcl  12198  nnadd1com  12200  nnaddcom  12201  nnmtmip  12203  nnneneg  12212  nnsub  12221  nndiv  12223  nndivtr  12224  nnnn0addcl  12467  nn0nnaddcl  12468  elnnnn0  12480  nn0sub  12487  nnnegz  12527  elz2  12542  zaddcl  12567  nnaddm1cl  12586  zdiv  12599  zdivadd  12600  zdivmul  12601  nneo  12613  peano5uzi  12618  elq  12900  qmulz  12901  qaddcl  12915  qnegcl  12916  qmulcl  12917  qreccl  12919  rpnnen1lem5  12931  nnledivrp  13056  nn0ledivnn  13057  fseq1m1p1  13553  ubmelm1fzo  13718  subfzo0  13747  quoremz  13814  quoremnn0ALT  13816  intfracq  13818  fldiv  13819  fldiv2  13820  modmulnn  13848  addmodid  13881  addmodidr  13882  modaddmodup  13896  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  nn0ennn  13941  ser1const  14020  expneg  14031  expm1t  14052  nnsqcl  14090  nnlesq  14167  digit2  14198  digit1  14199  expnngt1  14203  facdiv  14249  facndiv  14250  faclbnd  14252  faclbnd4lem1  14255  faclbnd4lem4  14258  bcn1  14275  bcm1k  14277  bcp1n  14278  bcval5  14280  bcn2m1  14286  cshwidxmod  14765  cshwidxm  14770  cshwidxn  14771  repswcshw  14774  isercoll2  15631  divcnv  15818  harmonic  15824  arisum  15825  arisum2  15826  expcnv  15829  pwdif  15833  geomulcvg  15841  mertenslem2  15850  ef0lem  16043  efexp  16068  ruclem12  16208  sqrt2irr  16216  nndivides  16231  modmulconst  16257  dvdsflip  16286  nn0enne  16346  nno  16351  pwp1fsum  16360  divalgmod  16375  ndvdsadd  16379  modgcd  16501  gcdmultiplez  16504  gcddiv  16520  rpmulgcd  16526  rplpwr  16527  sqgcd  16531  expgcd  16532  nn0expgcd  16533  lcmgcdlem  16575  qredeq  16626  qredeu  16627  cncongrcoprm  16639  prmind2  16654  isprm6  16684  divnumden  16718  divdenle  16719  nn0gcdsq  16722  hashgcdlem  16758  pythagtriplem1  16787  pythagtriplem2  16788  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem16  16801  pythagtriplem17  16802  pythagtriplem19  16804  pcqcl  16827  pcexp  16830  pcneg  16845  fldivp1  16868  oddprmdvds  16874  prmpwdvds  16875  infpnlem2  16882  prmreclem1  16887  prmreclem6  16892  4sqlem19  16934  vdwapun  16945  vdwapid1  16946  prmonn2  17010  prmgaplem7  17028  mulgnegnn  19060  mulgnnass  19085  mulgmodid  19089  odmod  19521  cnfldmulg  21384  prmirredlem  21452  znidomb  21541  znrrg  21545  cply1mul  22261  chfacfscmul0  22823  chfacfscmulfsupp  22824  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulfsupp  22828  chfacfpmmulgsum  22829  cayhamlem1  22831  cpmadugsumlemF  22841  ovolunlem1  25464  uniioombllem3  25552  vitali  25580  mbfi1fseqlem3  25684  dvexp  25920  dvexp3  25945  plyeq0lem  26175  dgrcolem1  26238  aaliou3lem2  26309  aaliou3lem7  26315  pserdv2  26395  abelthlem6  26401  logtayl  26624  logtaylsum  26625  logtayl2  26626  cxpexp  26632  cxproot  26654  root1id  26718  root1eq1  26719  cxpeq  26721  logbgcd1irr  26758  atantayl  26901  atantayl2  26902  birthdaylem2  26916  dfef2  26934  emcllem2  26960  emcllem3  26961  zetacvg  26978  lgam1  27027  gamfac  27030  basellem2  27045  basellem3  27046  basellem5  27048  basellem8  27051  mumul  27144  fsumdvdscom  27148  muinv  27156  chtublem  27174  perfect  27194  pcbcctr  27239  bclbnd  27243  bposlem1  27247  bposlem6  27252  lgssq2  27301  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  2lgslem1a1  27352  2sqlem6  27386  2sqlem10  27391  2sqnn  27402  2sqreunnltlem  27413  rplogsumlem1  27447  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumiflem1  27464  dchrvmaeq0  27467  dchrisum0re  27476  logdivbnd  27519  cusgrsize2inds  29522  wlkdlem2  29750  crctcshwlkn0lem1  29878  crctcshwlkn0lem6  29883  0enwwlksnge1  29932  wspthsnonn0vne  29985  clwwlknwwlksn  30108  clwwlkinwwlk  30110  clwwlkel  30116  clwwlkf  30117  clwwlkf1  30119  wwlksubclwwlk  30128  eucrctshift  30313  eucrct2eupth  30315  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  ipasslem4  30905  ipasslem5  30906  isarchi3  33248  oddpwdc  34498  eulerpartlemb  34512  fibp1  34545  subfacp1lem6  35367  subfaclim  35370  snmlff  35511  circum  35856  divcnvlin  35915  bcprod  35920  iprodgam  35924  faclim  35928  faclim2  35930  nn0prpwlem  36504  nndivsub  36639  knoppndvlem13  36784  poimirlem13  37954  poimirlem14  37955  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  facp2  42582  dvdsexpnn0  42766  renegmulnnass  42910  fimgmcyc  42979  dffltz  43067  irrapxlem1  43250  pellexlem1  43257  pellqrex  43307  2nn0ind  43373  jm2.17c  43390  acongrep  43408  jm2.18  43416  jm2.20nn  43425  jm2.16nn0  43432  proot1ex  43624  hashnzfzclim  44749  binomcxplemnotnn0  44783  nnsplit  45788  clim1fr1  46031  sumnnodd  46060  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  dirkerper  46524  dirkertrigeqlem1  46526  fouriersw  46659  nnfoctbdjlem  46883  deccarry  47759  subsubelfzo0  47775  submodlt  47804  mod0mul  47810  m1modmmod  47812  modlt0b  47817  sqrtpwpw2p  48001  fmtnodvds  48007  fmtnoprmfac1  48028  fmtnoprmfac2lem1  48029  fmtnoprmfac2  48030  lighneallem2  48069  lighneallem3  48070  lighneallem4  48073  nnennexALTV  48177  perfectALTV  48199  fppr2odd  48207  fpprwppr  48215  fpprwpprb  48216  tgoldbachlt  48292  gpgedgvtx0  48537  gpg3kgrtriexlem2  48560  gpg3kgrtriexlem5  48563  gpg3kgrtriex  48565  nnsgrp  48653  nnsgrpnmnd  48654  bcpascm1  48827  altgsumbcALT  48829  eluz2cnn0n1  48987  pw2m1lepw2m1  48996  nnennex  49001  logbpw2m1  49043  blenpw2m1  49055  nnpw2blen  49056  nnpw2pmod  49059  blennnt2  49065  blennn0em1  49067  nn0digval  49076  dignn0fr  49077  dignn0ldlem  49078  dig0  49082  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097