Theorem nncn 12259

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11116  ℕcn 12251

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-addcl 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-nn 12252

This theorem is used by:  nncni  12261  nn1m1nn  12272  nn1suc  12273  nnaddcl  12274  nnmulcl  12275  nnadd1com  12277  nnaddcom  12278  nnmtmip  12280  nnneneg  12289  nnsub  12298  nndiv  12300  nndivtr  12301  nnnn0addcl  12552  nn0nnaddcl  12553  elnnnn0  12565  nn0sub  12572  nnnegz  12612  elz2  12627  zaddcl  12652  nnaddm1cl  12671  zdiv  12684  zdivadd  12685  zdivmul  12686  nneo  12698  peano5uzi  12703  elq  12992  qmulz  12993  qaddcl  13007  qnegcl  13008  qmulcl  13009  qreccl  13011  rpnnen1lem5  13023  nnledivrp  13148  nn0ledivnn  13149  fseq1m1p1  13646  ubmelm1fzo  13811  subfzo0  13841  quoremz  13908  quoremnn0ALT  13910  intfracq  13912  fldiv  13913  fldiv2  13914  modmulnn  13942  addmodid  13975  addmodidr  13976  modaddmodup  13990  modfzo0difsn  13999  modsumfzodifsn  14000  addmodlteq  14002  nn0ennn  14035  ser1const  14114  expneg  14125  expm1t  14146  nnsqcl  14184  nnlesq  14261  digit2  14292  digit1  14293  expnngt1  14297  facdiv  14343  facndiv  14344  faclbnd  14346  faclbnd4lem1  14349  faclbnd4lem4  14352  bcn1  14369  bcm1k  14371  bcp1n  14372  bcval5  14374  bcn2m1  14380  cshwidxmod  14866  cshwidxm  14871  cshwidxn  14872  repswcshw  14875  isercoll2  15746  divcnv  15933  harmonic  15939  arisum  15940  arisum2  15941  expcnv  15944  pwdif  15948  geomulcvg  15956  mertenslem2  15965  ef0lem  16157  efexp  16182  ruclem12  16322  sqrt2irr  16330  nndivides  16345  modmulconst  16371  dvdsflip  16400  nn0enne  16460  nno  16465  pwp1fsum  16474  divalgmod  16489  ndvdsadd  16493  modgcd  16615  gcdmultiplez  16618  gcddiv  16634  rpmulgcd  16640  rplpwr  16641  sqgcd  16645  expgcd  16646  nn0expgcd  16647  lcmgcdlem  16689  qredeq  16740  qredeu  16741  cncongrcoprm  16753  prmind2  16768  isprm6  16798  divnumden  16832  divdenle  16833  nn0gcdsq  16836  hashgcdlem  16872  pythagtriplem1  16901  pythagtriplem2  16902  pythagtriplem6  16906  pythagtriplem7  16907  pythagtriplem12  16911  pythagtriplem14  16913  pythagtriplem15  16914  pythagtriplem16  16915  pythagtriplem17  16916  pythagtriplem19  16918  pcqcl  16941  pcexp  16944  pcneg  16959  fldivp1  16982  oddprmdvds  16988  prmpwdvds  16989  infpnlem2  16996  prmreclem1  17001  prmreclem6  17006  4sqlem19  17048  vdwapun  17059  vdwapid1  17060  prmonn2  17124  prmgaplem7  17142  mulgnegnn  19181  mulgnnass  19206  mulgmodid  19210  odmod  19647  cnfldmulg  21591  prmirredlem  21659  znidomb  21748  znrrg  21752  cply1mul  22493  chfacfscmul0  23052  chfacfscmulfsupp  23053  chfacfscmulgsum  23054  chfacfpmmul0  23056  chfacfpmmulfsupp  23057  chfacfpmmulgsum  23058  cayhamlem1  23060  cpmadugsumlemF  23070  ovolunlem1  25693  uniioombllem3  25781  vitali  25809  mbfi1fseqlem3  25913  dvexp  26149  dvexp3  26174  plyeq0lem  26404  dgrcolem1  26467  aaliou3lem2  26543  aaliou3lem7  26549  pserdv2  26630  abelthlem6  26636  logtayl  26862  logtaylsum  26863  logtayl2  26864  cxpexp  26870  cxproot  26892  root1id  26956  root1eq1  26957  cxpeq  26959  logbgcd1irr  26996  atantayl  27139  atantayl2  27140  birthdaylem2  27154  dfef2  27172  emcllem2  27198  emcllem3  27199  zetacvg  27216  lgam1  27265  gamfac  27268  basellem2  27283  basellem3  27284  basellem5  27286  basellem8  27289  mumul  27382  fsumdvdscom  27386  muinv  27394  chtublem  27412  perfect  27432  pcbcctr  27477  bclbnd  27481  bposlem1  27485  bposlem6  27490  lgssq2  27539  gausslemma2dlem1a  27566  gausslemma2dlem3  27569  2lgslem1a1  27590  2sqlem6  27624  2sqlem10  27629  2sqnn  27640  2sqreunnltlem  27651  rplogsumlem1  27685  dchrmusumlema  27694  dchrmusum2  27695  dchrvmasumiflem1  27702  dchrvmaeq0  27705  dchrisum0re  27714  logdivbnd  27757  cusgrsize2inds  29840  wlkdlem2  30068  crctcshwlkn0lem1  30196  crctcshwlkn0lem6  30201  0enwwlksnge1  30250  wspthsnonn0vne  30303  clwwlknwwlksn  30426  clwwlkinwwlk  30428  clwwlkel  30434  clwwlkf  30435  clwwlkf1  30437  wwlksubclwwlk  30446  eucrctshift  30631  eucrct2eupth  30633  numclwwlk2lem1  30764  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  ipasslem4  31223  ipasslem5  31224  isarchi3  33538  oddpwdc  34776  eulerpartlemb  34790  fibp1  34823  subfacp1lem6  35698  subfaclim  35701  snmlff  35842  circum  36187  divcnvlin  36246  bcprod  36251  iprodgam  36255  faclim  36259  faclim2  36261  nn0prpwlem  36874  nndivsub  37009  knoppndvlem13  37154  poimirlem13  38325  poimirlem14  38326  poimirlem29  38341  poimirlem30  38342  poimirlem31  38343  poimirlem32  38344  mblfinlem2  38350  ovoliunnfl  38354  voliunnfl  38356  facp2  42951  dvdsexpnn0  43136  renegmulnnass  43280  fimgmcyc  43343  dffltz  43407  irrapxlem1  43590  pellexlem1  43597  pellqrex  43647  2nn0ind  43713  jm2.17c  43730  acongrep  43748  jm2.18  43756  jm2.20nn  43765  jm2.16nn0  43772  proot1ex  43964  hashnzfzclim  45073  binomcxplemnotnn0  45107  nnsplit  46115  clim1fr1  46358  sumnnodd  46387  wallispilem4  46823  wallispilem5  46824  wallispi  46825  wallispi2lem1  46826  wallispi2lem2  46827  wallispi2  46828  stirlinglem1  46829  stirlinglem3  46831  stirlinglem4  46832  stirlinglem5  46833  stirlinglem6  46834  stirlinglem7  46835  stirlinglem8  46836  stirlinglem10  46838  stirlinglem11  46839  stirlinglem12  46840  stirlinglem13  46841  stirlinglem14  46842  stirlinglem15  46843  dirkerper  46851  dirkertrigeqlem1  46853  fouriersw  46986  nnfoctbdjlem  47210  sqrtnnaa  47645  deccarry  48089  subsubelfzo0  48105  submodlt  48134  mod0mul  48140  m1modmmod  48142  modlt0b  48147  sqrtpwpw2p  48331  fmtnodvds  48337  fmtnoprmfac1  48358  fmtnoprmfac2lem1  48359  fmtnoprmfac2  48360  lighneallem2  48399  lighneallem3  48400  lighneallem4  48403  nnennexALTV  48507  perfectALTV  48529  fppr2odd  48537  fpprwppr  48545  fpprwpprb  48546  tgoldbachlt  48622  gpgedgvtx0  48867  gpg3kgrtriexlem2  48890  gpg3kgrtriexlem5  48893  gpg3kgrtriex  48895  nnsgrp  48983  nnsgrpnmnd  48984  bcpascm1  49172  altgsumbcALT  49174  eluz2cnn0n1  49332  pw2m1lepw2m1  49341  nnennex  49346  logbpw2m1  49388  blenpw2m1  49400  nnpw2blen  49401  nnpw2pmod  49404  blennnt2  49410  blennn0em1  49412  nn0digval  49421  dignn0fr  49422  dignn0ldlem  49423  dig0  49427  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441  nn0sumshdiglem1  49442