Theorem nncn 12271

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℕcn 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264

This theorem is referenced by:  nncni  12273  nn1m1nn  12284  nn1suc  12285  nnaddcl  12286  nnmulcl  12287  nnmtmip  12289  nnneneg  12298  nnsub  12307  nndiv  12309  nndivtr  12310  nnnn0addcl  12553  nn0nnaddcl  12554  elnnnn0  12566  nn0sub  12573  nnnegz  12613  elz2  12628  zaddcl  12654  nnaddm1cl  12672  zdiv  12685  zdivadd  12686  zdivmul  12687  nneo  12699  peano5uzi  12704  elq  12989  qmulz  12990  qaddcl  13004  qnegcl  13005  qmulcl  13006  qreccl  13008  rpnnen1lem5  13020  nnledivrp  13144  nn0ledivnn  13145  fseq1m1p1  13635  ubmelm1fzo  13798  subfzo0  13824  quoremz  13891  quoremnn0ALT  13893  intfracq  13895  fldiv  13896  fldiv2  13897  modmulnn  13925  addmodid  13956  addmodidr  13957  modaddmodup  13971  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  nn0ennn  14016  ser1const  14095  expneg  14106  expm1t  14127  nnsqcl  14164  nnlesq  14240  digit2  14271  digit1  14272  expnngt1  14276  facdiv  14322  facndiv  14323  faclbnd  14325  faclbnd4lem1  14328  faclbnd4lem4  14331  bcn1  14348  bcm1k  14350  bcp1n  14351  bcval5  14353  bcn2m1  14359  cshwidxmod  14837  cshwidxm  14842  cshwidxn  14843  repswcshw  14846  isercoll2  15701  divcnv  15885  harmonic  15891  arisum  15892  arisum2  15893  expcnv  15896  pwdif  15900  geomulcvg  15908  mertenslem2  15917  ef0lem  16110  efexp  16133  ruclem12  16273  sqrt2irr  16281  nndivides  16296  modmulconst  16321  dvdsflip  16350  nn0enne  16410  nno  16415  pwp1fsum  16424  divalgmod  16439  ndvdsadd  16443  modgcd  16565  gcdmultiplez  16568  gcddiv  16584  rpmulgcd  16590  rplpwr  16591  sqgcd  16595  expgcd  16596  nn0expgcd  16597  lcmgcdlem  16639  qredeq  16690  qredeu  16691  cncongrcoprm  16703  prmind2  16718  isprm6  16747  divnumden  16781  divdenle  16782  nn0gcdsq  16785  hashgcdlem  16821  pythagtriplem1  16849  pythagtriplem2  16850  pythagtriplem6  16854  pythagtriplem7  16855  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem15  16862  pythagtriplem16  16863  pythagtriplem17  16864  pythagtriplem19  16866  pcqcl  16889  pcexp  16892  pcneg  16907  fldivp1  16930  oddprmdvds  16936  prmpwdvds  16937  infpnlem2  16944  prmreclem1  16949  prmreclem6  16954  4sqlem19  16996  vdwapun  17007  vdwapid1  17008  prmonn2  17072  prmgaplem7  17090  mulgnegnn  19114  mulgnnass  19139  mulgmodid  19143  odmod  19578  cnfldmulg  21433  prmirredlem  21500  znidomb  21597  znrrg  21601  cply1mul  22315  chfacfscmul0  22879  chfacfscmulfsupp  22880  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulfsupp  22884  chfacfpmmulgsum  22885  cayhamlem1  22887  cpmadugsumlemF  22897  ovolunlem1  25545  uniioombllem3  25633  vitali  25661  mbfi1fseqlem3  25766  dvexp  26005  dvexp3  26030  plyeq0lem  26263  dgrcolem1  26327  aaliou3lem2  26399  aaliou3lem7  26405  pserdv2  26488  abelthlem6  26494  logtayl  26716  logtaylsum  26717  logtayl2  26718  cxpexp  26724  cxproot  26746  root1id  26811  root1eq1  26812  cxpeq  26814  logbgcd1irr  26851  atantayl  26994  atantayl2  26995  birthdaylem2  27009  dfef2  27028  emcllem2  27054  emcllem3  27055  zetacvg  27072  lgam1  27121  gamfac  27124  basellem2  27139  basellem3  27140  basellem5  27142  basellem8  27145  mumul  27238  fsumdvdscom  27242  muinv  27250  chtublem  27269  perfect  27289  pcbcctr  27334  bclbnd  27338  bposlem1  27342  bposlem6  27347  lgssq2  27396  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  2lgslem1a1  27447  2sqlem6  27481  2sqlem10  27486  2sqnn  27497  2sqreunnltlem  27508  rplogsumlem1  27542  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumiflem1  27559  dchrvmaeq0  27562  dchrisum0re  27571  logdivbnd  27614  cusgrsize2inds  29485  wlkdlem2  29715  crctcshwlkn0lem1  29839  crctcshwlkn0lem6  29844  0enwwlksnge1  29893  wspthsnonn0vne  29946  clwwlknwwlksn  30066  clwwlkinwwlk  30068  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  wwlksubclwwlk  30086  eucrctshift  30271  eucrct2eupth  30273  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  ipasslem4  30862  ipasslem5  30863  isarchi3  33176  oddpwdc  34335  eulerpartlemb  34349  fibp1  34382  subfacp1lem6  35169  subfaclim  35172  snmlff  35313  circum  35658  divcnvlin  35712  bcprod  35717  iprodgam  35721  faclim  35725  faclim2  35727  nn0prpwlem  36304  nndivsub  36439  knoppndvlem13  36506  poimirlem13  37619  poimirlem14  37620  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  facp2  42124  metakunt16  42201  metakunt30  42215  fac2xp3  42220  nnadd1com  42280  nnaddcom  42281  dvdsexpnn0  42347  renegmulnnass  42459  fimgmcyc  42520  dffltz  42620  irrapxlem1  42809  pellexlem1  42816  pellqrex  42866  2nn0ind  42933  jm2.17c  42950  acongrep  42968  jm2.18  42976  jm2.20nn  42985  jm2.16nn0  42992  proot1ex  43184  hashnzfzclim  44317  binomcxplemnotnn0  44351  nnsplit  45307  clim1fr1  45556  sumnnodd  45585  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  dirkerper  46051  dirkertrigeqlem1  46053  fouriersw  46186  nnfoctbdjlem  46410  deccarry  47260  subsubelfzo0  47275  submodlt  47289  sqrtpwpw2p  47462  fmtnodvds  47468  fmtnoprmfac1  47489  fmtnoprmfac2lem1  47490  fmtnoprmfac2  47491  lighneallem2  47530  lighneallem3  47531  lighneallem4  47534  nnennexALTV  47625  perfectALTV  47647  fppr2odd  47655  fpprwppr  47663  fpprwpprb  47664  tgoldbachlt  47740  gpgedgvtx0  47953  nnsgrp  48020  nnsgrpnmnd  48021  bcpascm1  48195  altgsumbcALT  48197  eluz2cnn0n1  48356  pw2m1lepw2m1  48365  mod0mul  48368  m1modmmod  48370  nnennex  48374  logbpw2m1  48416  blenpw2m1  48428  nnpw2blen  48429  nnpw2pmod  48432  blennnt2  48438  blennn0em1  48440  nn0digval  48449  dignn0fr  48450  dignn0ldlem  48451  dig0  48455  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470