Theorem nncn 12201

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℕcn 12193

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194

This theorem is referenced by:  nncni  12203  nn1m1nn  12214  nn1suc  12215  nnaddcl  12216  nnmulcl  12217  nnmtmip  12219  nnneneg  12228  nnsub  12237  nndiv  12239  nndivtr  12240  nnnn0addcl  12479  nn0nnaddcl  12480  elnnnn0  12492  nn0sub  12499  nnnegz  12539  elz2  12554  zaddcl  12580  nnaddm1cl  12598  zdiv  12611  zdivadd  12612  zdivmul  12613  nneo  12625  peano5uzi  12630  elq  12916  qmulz  12917  qaddcl  12931  qnegcl  12932  qmulcl  12933  qreccl  12935  rpnnen1lem5  12947  nnledivrp  13072  nn0ledivnn  13073  fseq1m1p1  13567  ubmelm1fzo  13731  subfzo0  13757  quoremz  13824  quoremnn0ALT  13826  intfracq  13828  fldiv  13829  fldiv2  13830  modmulnn  13858  addmodid  13891  addmodidr  13892  modaddmodup  13906  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  nn0ennn  13951  ser1const  14030  expneg  14041  expm1t  14062  nnsqcl  14100  nnlesq  14177  digit2  14208  digit1  14209  expnngt1  14213  facdiv  14259  facndiv  14260  faclbnd  14262  faclbnd4lem1  14265  faclbnd4lem4  14268  bcn1  14285  bcm1k  14287  bcp1n  14288  bcval5  14290  bcn2m1  14296  cshwidxmod  14775  cshwidxm  14780  cshwidxn  14781  repswcshw  14784  isercoll2  15642  divcnv  15826  harmonic  15832  arisum  15833  arisum2  15834  expcnv  15837  pwdif  15841  geomulcvg  15849  mertenslem2  15858  ef0lem  16051  efexp  16076  ruclem12  16216  sqrt2irr  16224  nndivides  16239  modmulconst  16265  dvdsflip  16294  nn0enne  16354  nno  16359  pwp1fsum  16368  divalgmod  16383  ndvdsadd  16387  modgcd  16509  gcdmultiplez  16512  gcddiv  16528  rpmulgcd  16534  rplpwr  16535  sqgcd  16539  expgcd  16540  nn0expgcd  16541  lcmgcdlem  16583  qredeq  16634  qredeu  16635  cncongrcoprm  16647  prmind2  16662  isprm6  16691  divnumden  16725  divdenle  16726  nn0gcdsq  16729  hashgcdlem  16765  pythagtriplem1  16794  pythagtriplem2  16795  pythagtriplem6  16799  pythagtriplem7  16800  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem15  16807  pythagtriplem16  16808  pythagtriplem17  16809  pythagtriplem19  16811  pcqcl  16834  pcexp  16837  pcneg  16852  fldivp1  16875  oddprmdvds  16881  prmpwdvds  16882  infpnlem2  16889  prmreclem1  16894  prmreclem6  16899  4sqlem19  16941  vdwapun  16952  vdwapid1  16953  prmonn2  17017  prmgaplem7  17035  mulgnegnn  19023  mulgnnass  19048  mulgmodid  19052  odmod  19483  cnfldmulg  21322  prmirredlem  21389  znidomb  21478  znrrg  21482  cply1mul  22190  chfacfscmul0  22752  chfacfscmulfsupp  22753  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulfsupp  22757  chfacfpmmulgsum  22758  cayhamlem1  22760  cpmadugsumlemF  22770  ovolunlem1  25405  uniioombllem3  25493  vitali  25521  mbfi1fseqlem3  25625  dvexp  25864  dvexp3  25889  plyeq0lem  26122  dgrcolem1  26186  aaliou3lem2  26258  aaliou3lem7  26264  pserdv2  26347  abelthlem6  26353  logtayl  26576  logtaylsum  26577  logtayl2  26578  cxpexp  26584  cxproot  26606  root1id  26671  root1eq1  26672  cxpeq  26674  logbgcd1irr  26711  atantayl  26854  atantayl2  26855  birthdaylem2  26869  dfef2  26888  emcllem2  26914  emcllem3  26915  zetacvg  26932  lgam1  26981  gamfac  26984  basellem2  26999  basellem3  27000  basellem5  27002  basellem8  27005  mumul  27098  fsumdvdscom  27102  muinv  27110  chtublem  27129  perfect  27149  pcbcctr  27194  bclbnd  27198  bposlem1  27202  bposlem6  27207  lgssq2  27256  gausslemma2dlem1a  27283  gausslemma2dlem3  27286  2lgslem1a1  27307  2sqlem6  27341  2sqlem10  27346  2sqnn  27357  2sqreunnltlem  27368  rplogsumlem1  27402  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumiflem1  27419  dchrvmaeq0  27422  dchrisum0re  27431  logdivbnd  27474  cusgrsize2inds  29388  wlkdlem2  29618  crctcshwlkn0lem1  29747  crctcshwlkn0lem6  29752  0enwwlksnge1  29801  wspthsnonn0vne  29854  clwwlknwwlksn  29974  clwwlkinwwlk  29976  clwwlkel  29982  clwwlkf  29983  clwwlkf1  29985  wwlksubclwwlk  29994  eucrctshift  30179  eucrct2eupth  30181  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  ipasslem4  30770  ipasslem5  30771  isarchi3  33148  oddpwdc  34352  eulerpartlemb  34366  fibp1  34399  subfacp1lem6  35179  subfaclim  35182  snmlff  35323  circum  35668  divcnvlin  35727  bcprod  35732  iprodgam  35736  faclim  35740  faclim2  35742  nn0prpwlem  36317  nndivsub  36452  knoppndvlem13  36519  poimirlem13  37634  poimirlem14  37635  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  facp2  42138  nnadd1com  42262  nnaddcom  42263  dvdsexpnn0  42329  renegmulnnass  42460  fimgmcyc  42529  dffltz  42629  irrapxlem1  42817  pellexlem1  42824  pellqrex  42874  2nn0ind  42941  jm2.17c  42958  acongrep  42976  jm2.18  42984  jm2.20nn  42993  jm2.16nn0  43000  proot1ex  43192  hashnzfzclim  44318  binomcxplemnotnn0  44352  nnsplit  45361  clim1fr1  45606  sumnnodd  45635  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  dirkerper  46101  dirkertrigeqlem1  46103  fouriersw  46236  nnfoctbdjlem  46460  deccarry  47316  subsubelfzo0  47331  submodlt  47355  mod0mul  47361  m1modmmod  47363  modlt0b  47368  sqrtpwpw2p  47543  fmtnodvds  47549  fmtnoprmfac1  47570  fmtnoprmfac2lem1  47571  fmtnoprmfac2  47572  lighneallem2  47611  lighneallem3  47612  lighneallem4  47615  nnennexALTV  47706  perfectALTV  47728  fppr2odd  47736  fpprwppr  47744  fpprwpprb  47745  tgoldbachlt  47821  gpgedgvtx0  48056  gpg3kgrtriexlem2  48079  gpg3kgrtriexlem5  48082  gpg3kgrtriex  48084  nnsgrp  48169  nnsgrpnmnd  48170  bcpascm1  48343  altgsumbcALT  48345  eluz2cnn0n1  48504  pw2m1lepw2m1  48513  nnennex  48518  logbpw2m1  48560  blenpw2m1  48572  nnpw2blen  48573  nnpw2pmod  48576  blennnt2  48582  blennn0em1  48584  nn0digval  48593  dignn0fr  48594  dignn0ldlem  48595  dig0  48599  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614