Theorem nncn 12274

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℕcn 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267

This theorem is referenced by:  nncni  12276  nn1m1nn  12287  nn1suc  12288  nnaddcl  12289  nnmulcl  12290  nnmtmip  12292  nnneneg  12301  nnsub  12310  nndiv  12312  nndivtr  12313  nnnn0addcl  12556  nn0nnaddcl  12557  elnnnn0  12569  nn0sub  12576  nnnegz  12616  elz2  12631  zaddcl  12657  nnaddm1cl  12675  zdiv  12688  zdivadd  12689  zdivmul  12690  nneo  12702  peano5uzi  12707  elq  12992  qmulz  12993  qaddcl  13007  qnegcl  13008  qmulcl  13009  qreccl  13011  rpnnen1lem5  13023  nnledivrp  13147  nn0ledivnn  13148  fseq1m1p1  13639  ubmelm1fzo  13802  subfzo0  13828  quoremz  13895  quoremnn0ALT  13897  intfracq  13899  fldiv  13900  fldiv2  13901  modmulnn  13929  addmodid  13960  addmodidr  13961  modaddmodup  13975  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  nn0ennn  14020  ser1const  14099  expneg  14110  expm1t  14131  nnsqcl  14168  nnlesq  14244  digit2  14275  digit1  14276  expnngt1  14280  facdiv  14326  facndiv  14327  faclbnd  14329  faclbnd4lem1  14332  faclbnd4lem4  14335  bcn1  14352  bcm1k  14354  bcp1n  14355  bcval5  14357  bcn2m1  14363  cshwidxmod  14841  cshwidxm  14846  cshwidxn  14847  repswcshw  14850  isercoll2  15705  divcnv  15889  harmonic  15895  arisum  15896  arisum2  15897  expcnv  15900  pwdif  15904  geomulcvg  15912  mertenslem2  15921  ef0lem  16114  efexp  16137  ruclem12  16277  sqrt2irr  16285  nndivides  16300  modmulconst  16325  dvdsflip  16354  nn0enne  16414  nno  16419  pwp1fsum  16428  divalgmod  16443  ndvdsadd  16447  modgcd  16569  gcdmultiplez  16572  gcddiv  16588  rpmulgcd  16594  rplpwr  16595  sqgcd  16599  expgcd  16600  nn0expgcd  16601  lcmgcdlem  16643  qredeq  16694  qredeu  16695  cncongrcoprm  16707  prmind2  16722  isprm6  16751  divnumden  16785  divdenle  16786  nn0gcdsq  16789  hashgcdlem  16825  pythagtriplem1  16854  pythagtriplem2  16855  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem15  16867  pythagtriplem16  16868  pythagtriplem17  16869  pythagtriplem19  16871  pcqcl  16894  pcexp  16897  pcneg  16912  fldivp1  16935  oddprmdvds  16941  prmpwdvds  16942  infpnlem2  16949  prmreclem1  16954  prmreclem6  16959  4sqlem19  17001  vdwapun  17012  vdwapid1  17013  prmonn2  17077  prmgaplem7  17095  mulgnegnn  19102  mulgnnass  19127  mulgmodid  19131  odmod  19564  cnfldmulg  21416  prmirredlem  21483  znidomb  21580  znrrg  21584  cply1mul  22300  chfacfscmul0  22864  chfacfscmulfsupp  22865  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulfsupp  22869  chfacfpmmulgsum  22870  cayhamlem1  22872  cpmadugsumlemF  22882  ovolunlem1  25532  uniioombllem3  25620  vitali  25648  mbfi1fseqlem3  25752  dvexp  25991  dvexp3  26016  plyeq0lem  26249  dgrcolem1  26313  aaliou3lem2  26385  aaliou3lem7  26391  pserdv2  26474  abelthlem6  26480  logtayl  26702  logtaylsum  26703  logtayl2  26704  cxpexp  26710  cxproot  26732  root1id  26797  root1eq1  26798  cxpeq  26800  logbgcd1irr  26837  atantayl  26980  atantayl2  26981  birthdaylem2  26995  dfef2  27014  emcllem2  27040  emcllem3  27041  zetacvg  27058  lgam1  27107  gamfac  27110  basellem2  27125  basellem3  27126  basellem5  27128  basellem8  27131  mumul  27224  fsumdvdscom  27228  muinv  27236  chtublem  27255  perfect  27275  pcbcctr  27320  bclbnd  27324  bposlem1  27328  bposlem6  27333  lgssq2  27382  gausslemma2dlem1a  27409  gausslemma2dlem3  27412  2lgslem1a1  27433  2sqlem6  27467  2sqlem10  27472  2sqnn  27483  2sqreunnltlem  27494  rplogsumlem1  27528  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumiflem1  27545  dchrvmaeq0  27548  dchrisum0re  27557  logdivbnd  27600  cusgrsize2inds  29471  wlkdlem2  29701  crctcshwlkn0lem1  29830  crctcshwlkn0lem6  29835  0enwwlksnge1  29884  wspthsnonn0vne  29937  clwwlknwwlksn  30057  clwwlkinwwlk  30059  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  wwlksubclwwlk  30077  eucrctshift  30262  eucrct2eupth  30264  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  ipasslem4  30853  ipasslem5  30854  isarchi3  33194  oddpwdc  34356  eulerpartlemb  34370  fibp1  34403  subfacp1lem6  35190  subfaclim  35193  snmlff  35334  circum  35679  divcnvlin  35733  bcprod  35738  iprodgam  35742  faclim  35746  faclim2  35748  nn0prpwlem  36323  nndivsub  36458  knoppndvlem13  36525  poimirlem13  37640  poimirlem14  37641  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  facp2  42144  metakunt16  42221  metakunt30  42235  fac2xp3  42240  nnadd1com  42302  nnaddcom  42303  dvdsexpnn0  42369  renegmulnnass  42483  fimgmcyc  42544  dffltz  42644  irrapxlem1  42833  pellexlem1  42840  pellqrex  42890  2nn0ind  42957  jm2.17c  42974  acongrep  42992  jm2.18  43000  jm2.20nn  43009  jm2.16nn0  43016  proot1ex  43208  hashnzfzclim  44341  binomcxplemnotnn0  44375  nnsplit  45369  clim1fr1  45616  sumnnodd  45645  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  dirkerper  46111  dirkertrigeqlem1  46113  fouriersw  46246  nnfoctbdjlem  46470  deccarry  47323  subsubelfzo0  47338  submodlt  47352  sqrtpwpw2p  47525  fmtnodvds  47531  fmtnoprmfac1  47552  fmtnoprmfac2lem1  47553  fmtnoprmfac2  47554  lighneallem2  47593  lighneallem3  47594  lighneallem4  47597  nnennexALTV  47688  perfectALTV  47710  fppr2odd  47718  fpprwppr  47726  fpprwpprb  47727  tgoldbachlt  47803  gpgedgvtx0  48019  gpg3kgrtriexlem2  48040  gpg3kgrtriexlem5  48043  gpg3kgrtriex  48045  nnsgrp  48093  nnsgrpnmnd  48094  bcpascm1  48267  altgsumbcALT  48269  eluz2cnn0n1  48428  pw2m1lepw2m1  48437  mod0mul  48440  m1modmmod  48442  nnennex  48446  logbpw2m1  48488  blenpw2m1  48500  nnpw2blen  48501  nnpw2pmod  48504  blennnt2  48510  blennn0em1  48512  nn0digval  48521  dignn0fr  48522  dignn0ldlem  48523  dig0  48527  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542