Theorem nncn 12324

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11179  ℕcn 12316

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-1cn 11239  ax-addcl 11241

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-nn 12317

This theorem is used by:  nncni  12326  nn1m1nn  12337  nn1suc  12338  nnaddcl  12339  nnmulcl  12340  nnadd1com  12342  nnaddcom  12343  nnmtmip  12345  nnneneg  12354  nnsub  12363  nndiv  12365  nndivtr  12366  nnnn0addcl  12617  nn0nnaddcl  12618  elnnnn0  12630  nn0sub  12637  nnnegz  12677  elz2  12692  zaddcl  12717  nnaddm1cl  12737  zdiv  12750  zdivadd  12751  zdivmul  12752  nneo  12764  peano5uzi  12769  elq  13058  qmulz  13059  qaddcl  13074  qnegcl  13075  qmulcl  13076  qreccl  13078  rpnnen1lem5  13090  nnledivrp  13215  nn0ledivnn  13216  fseq1m1p1  13713  ubmelm1fzo  13878  subfzo0  13908  quoremz  13975  quoremnn0ALT  13977  intfracq  13979  fldiv  13980  fldiv2  13981  modmulnn  14009  addmodid  14042  addmodidr  14043  modaddmodup  14057  modfzo0difsn  14066  modsumfzodifsn  14067  addmodlteq  14069  nn0ennn  14102  ser1const  14181  expneg  14192  expm1t  14213  nnsqcl  14251  nnlesq  14329  digit2  14360  digit1  14361  expnngt1  14365  facdiv  14411  facndiv  14412  faclbnd  14414  faclbnd4lem1  14417  faclbnd4lem4  14420  bcn1  14437  bcm1k  14439  bcp1n  14440  bcval5  14442  bcn2m1  14448  cshwidxmod  14934  cshwidxm  14939  cshwidxn  14940  repswcshw  14943  isercoll2  15816  divcnv  16002  harmonic  16008  arisum  16009  arisum2  16010  expcnv  16013  pwdif  16017  geomulcvg  16025  mertenslem2  16034  ef0lem  16224  efexp  16249  ruclem12  16389  sqrt2irr  16397  nndivides  16412  modmulconst  16438  dvdsflip  16467  nn0enne  16527  nno  16532  pwp1fsum  16541  divalgmod  16556  ndvdsadd  16560  modgcd  16685  gcdmultiplez  16688  gcddiv  16704  rpmulgcd  16711  rplpwr  16712  sqgcd  16716  expgcd  16717  nn0expgcd  16718  lcmgcdlem  16761  qredeq  16812  qredeu  16813  cncongrcoprm  16825  prmind2  16840  isprm6  16870  divnumden  16904  divdenle  16905  nn0gcdsq  16908  hashgcdlem  16945  pythagtriplem1  16974  pythagtriplem2  16975  pythagtriplem6  16979  pythagtriplem7  16980  pythagtriplem12  16984  pythagtriplem14  16986  pythagtriplem15  16987  pythagtriplem16  16988  pythagtriplem17  16989  pythagtriplem19  16991  pcqcl  17014  pcexp  17017  pcneg  17032  fldivp1  17055  oddprmdvds  17061  prmpwdvds  17062  infpnlem2  17069  prmreclem1  17074  prmreclem6  17079  4sqlem19  17121  vdwapun  17132  vdwapid1  17133  prmonn2  17197  prmgaplem7  17215  mulgnegnn  19274  mulgnnass  19299  mulgmodid  19303  odmod  19740  cnfldmulg  21690  prmirredlem  21758  znidomb  21847  znrrg  21851  cply1mul  22594  chfacfscmul0  23156  chfacfscmulfsupp  23157  chfacfscmulgsum  23158  chfacfpmmul0  23160  chfacfpmmulfsupp  23161  chfacfpmmulgsum  23162  cayhamlem1  23164  cpmadugsumlemF  23174  ovolunlem1  25798  uniioombllem3  25886  vitali  25914  mbfi1fseqlem3  26018  dvexp  26253  dvexp3  26278  plyeq0lem  26509  dgrcolem1  26572  aaliou3lem2  26652  aaliou3lem7  26658  pserdv2  26739  abelthlem6  26745  logtayl  26970  logtaylsum  26971  logtayl2  26972  cxpexp  26978  cxproot  27000  root1id  27064  root1eq1  27065  cxpeq  27067  logbgcd1irr  27104  atantayl  27247  atantayl2  27248  birthdaylem2  27262  dfef2  27280  emcllem2  27306  emcllem3  27307  zetacvg  27324  lgam1  27373  gamfac  27376  basellem2  27391  basellem3  27392  basellem5  27394  basellem8  27397  mumul  27490  fsumdvdscom  27494  muinv  27502  chtublem  27520  perfect  27540  pcbcctr  27585  bclbnd  27589  bposlem1  27593  bposlem6  27598  lgssq2  27647  gausslemma2dlem1a  27674  gausslemma2dlem3  27677  2lgslem1a1  27698  2sqlem6  27732  2sqlem10  27737  2sqnn  27748  2sqreunnltlem  27759  rplogsumlem1  27793  dchrmusumlema  27802  dchrmusum2  27803  dchrvmasumiflem1  27810  dchrvmaeq0  27813  dchrisum0re  27822  logdivbnd  27865  cusgrsize2inds  30016  wlkdlem2  30244  crctcshwlkn0lem1  30381  crctcshwlkn0lem6  30386  0enwwlksnge1  30435  wspthsnonn0vne  30488  clwwlknwwlksn  30611  clwwlkinwwlk  30613  clwwlkel  30619  clwwlkf  30620  clwwlkf1  30622  wwlksubclwwlk  30631  eucrctshift  30826  eucrct2eupth  30828  numclwwlk2lem1  30959  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  ipasslem4  31418  ipasslem5  31419  isarchi3  33730  oddpwdc  34969  eulerpartlemb  34983  fibp1  35016  subfacp1lem6  35919  subfaclim  35922  snmlff  36063  circum  36408  divcnvlin  36467  bcprod  36472  iprodgam  36476  faclim  36480  faclim2  36482  nn0prpwlem  37080  nndivsub  37215  knoppndvlem13  37360  poimirlem13  38519  poimirlem14  38520  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  mblfinlem2  38544  ovoliunnfl  38548  voliunnfl  38550  facp2  43161  dvdsexpnn0  43354  renegmulnnass  43497  fimgmcyc  43560  dffltz  43624  irrapxlem1  43782  pellexlem1  43789  pellqrex  43839  2nn0ind  43905  jm2.17c  43922  acongrep  43940  jm2.18  43948  jm2.20nn  43957  jm2.16nn0  43964  proot1ex  44156  hashnzfzclim  45265  binomcxplemnotnn0  45299  nnsplit  46314  clim1fr1  46557  sumnnodd  46586  wallispilem4  47022  wallispilem5  47023  wallispi  47024  wallispi2lem1  47025  wallispi2lem2  47026  wallispi2  47027  stirlinglem1  47028  stirlinglem3  47030  stirlinglem4  47031  stirlinglem5  47032  stirlinglem6  47033  stirlinglem7  47034  stirlinglem8  47035  stirlinglem10  47037  stirlinglem11  47038  stirlinglem12  47039  stirlinglem13  47040  stirlinglem14  47041  stirlinglem15  47042  dirkerper  47050  dirkertrigeqlem1  47052  fouriersw  47185  nnfoctbdjlem  47409  sqrtnnaa  47857  deccarry  48325  subsubelfzo0  48341  submodlt  48370  mod0mul  48376  m1modmmod  48378  modlt0b  48383  sqrtpwpw2p  48567  fmtnodvds  48573  fmtnoprmfac1  48594  fmtnoprmfac2lem1  48595  fmtnoprmfac2  48596  lighneallem2  48635  lighneallem3  48636  lighneallem4  48639  nnennexALTV  48743  perfectALTV  48765  fppr2odd  48773  fpprwppr  48781  fpprwpprb  48782  tgoldbachlt  48858  gpgedgvtx0  49103  gpg3kgrtriexlem2  49126  gpg3kgrtriexlem5  49129  gpg3kgrtriex  49131  nnsgrp  49218  nnsgrpnmnd  49219  bcpascm1  49407  altgsumbcALT  49409  eluz2cnn0n1  49567  pw2m1lepw2m1  49576  nnennex  49581  logbpw2m1  49623  blenpw2m1  49635  nnpw2blen  49636  nnpw2pmod  49639  blennnt2  49645  blennn0em1  49647  nn0digval  49656  dignn0fr  49657  dignn0ldlem  49658  dig0  49662  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  nn0sumshdiglem1  49677