Theorem nncn 12180

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11034  ℕcn 12172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-addcl 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-nn 12173

This theorem is referenced by:  nncni  12182  nn1m1nn  12193  nn1suc  12194  nnaddcl  12195  nnmulcl  12196  nnadd1com  12198  nnaddcom  12199  nnmtmip  12201  nnneneg  12210  nnsub  12219  nndiv  12221  nndivtr  12222  nnnn0addcl  12465  nn0nnaddcl  12466  elnnnn0  12478  nn0sub  12485  nnnegz  12525  elz2  12540  zaddcl  12565  nnaddm1cl  12584  zdiv  12597  zdivadd  12598  zdivmul  12599  nneo  12611  peano5uzi  12616  elq  12898  qmulz  12899  qaddcl  12913  qnegcl  12914  qmulcl  12915  qreccl  12917  rpnnen1lem5  12929  nnledivrp  13054  nn0ledivnn  13055  fseq1m1p1  13551  ubmelm1fzo  13716  subfzo0  13745  quoremz  13812  quoremnn0ALT  13814  intfracq  13816  fldiv  13817  fldiv2  13818  modmulnn  13846  addmodid  13879  addmodidr  13880  modaddmodup  13894  modfzo0difsn  13903  modsumfzodifsn  13904  addmodlteq  13906  nn0ennn  13939  ser1const  14018  expneg  14029  expm1t  14050  nnsqcl  14088  nnlesq  14165  digit2  14196  digit1  14197  expnngt1  14201  facdiv  14247  facndiv  14248  faclbnd  14250  faclbnd4lem1  14253  faclbnd4lem4  14256  bcn1  14273  bcm1k  14275  bcp1n  14276  bcval5  14278  bcn2m1  14284  cshwidxmod  14763  cshwidxm  14768  cshwidxn  14769  repswcshw  14772  isercoll2  15629  divcnv  15816  harmonic  15822  arisum  15823  arisum2  15824  expcnv  15827  pwdif  15831  geomulcvg  15839  mertenslem2  15848  ef0lem  16041  efexp  16066  ruclem12  16206  sqrt2irr  16214  nndivides  16229  modmulconst  16255  dvdsflip  16284  nn0enne  16344  nno  16349  pwp1fsum  16358  divalgmod  16373  ndvdsadd  16377  modgcd  16499  gcdmultiplez  16502  gcddiv  16518  rpmulgcd  16524  rplpwr  16525  sqgcd  16529  expgcd  16530  nn0expgcd  16531  lcmgcdlem  16573  qredeq  16624  qredeu  16625  cncongrcoprm  16637  prmind2  16652  isprm6  16682  divnumden  16716  divdenle  16717  nn0gcdsq  16720  hashgcdlem  16756  pythagtriplem1  16785  pythagtriplem2  16786  pythagtriplem6  16790  pythagtriplem7  16791  pythagtriplem12  16795  pythagtriplem14  16797  pythagtriplem15  16798  pythagtriplem16  16799  pythagtriplem17  16800  pythagtriplem19  16802  pcqcl  16825  pcexp  16828  pcneg  16843  fldivp1  16866  oddprmdvds  16872  prmpwdvds  16873  infpnlem2  16880  prmreclem1  16885  prmreclem6  16890  4sqlem19  16932  vdwapun  16943  vdwapid1  16944  prmonn2  17008  prmgaplem7  17026  mulgnegnn  19058  mulgnnass  19083  mulgmodid  19087  odmod  19519  cnfldmulg  21386  prmirredlem  21454  znidomb  21543  znrrg  21547  cply1mul  22289  chfacfscmul0  22848  chfacfscmulfsupp  22849  chfacfscmulgsum  22850  chfacfpmmul0  22852  chfacfpmmulfsupp  22853  chfacfpmmulgsum  22854  cayhamlem1  22856  cpmadugsumlemF  22866  ovolunlem1  25489  uniioombllem3  25577  vitali  25605  mbfi1fseqlem3  25709  dvexp  25945  dvexp3  25970  plyeq0lem  26200  dgrcolem1  26263  aaliou3lem2  26334  aaliou3lem7  26340  pserdv2  26420  abelthlem6  26426  logtayl  26649  logtaylsum  26650  logtayl2  26651  cxpexp  26657  cxproot  26679  root1id  26743  root1eq1  26744  cxpeq  26746  logbgcd1irr  26783  atantayl  26926  atantayl2  26927  birthdaylem2  26941  dfef2  26959  emcllem2  26985  emcllem3  26986  zetacvg  27003  lgam1  27052  gamfac  27055  basellem2  27070  basellem3  27071  basellem5  27073  basellem8  27076  mumul  27169  fsumdvdscom  27173  muinv  27181  chtublem  27199  perfect  27219  pcbcctr  27264  bclbnd  27268  bposlem1  27272  bposlem6  27277  lgssq2  27326  gausslemma2dlem1a  27353  gausslemma2dlem3  27356  2lgslem1a1  27377  2sqlem6  27411  2sqlem10  27416  2sqnn  27427  2sqreunnltlem  27438  rplogsumlem1  27472  dchrmusumlema  27481  dchrmusum2  27482  dchrvmasumiflem1  27489  dchrvmaeq0  27492  dchrisum0re  27501  logdivbnd  27544  cusgrsize2inds  29547  wlkdlem2  29775  crctcshwlkn0lem1  29903  crctcshwlkn0lem6  29908  0enwwlksnge1  29957  wspthsnonn0vne  30010  clwwlknwwlksn  30133  clwwlkinwwlk  30135  clwwlkel  30141  clwwlkf  30142  clwwlkf1  30144  wwlksubclwwlk  30153  eucrctshift  30338  eucrct2eupth  30340  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  ipasslem4  30930  ipasslem5  30931  isarchi3  33275  oddpwdc  34545  eulerpartlemb  34559  fibp1  34592  subfacp1lem6  35420  subfaclim  35423  snmlff  35564  circum  35909  divcnvlin  35968  bcprod  35973  iprodgam  35977  faclim  35981  faclim2  35983  nn0prpwlem  36557  nndivsub  36692  knoppndvlem13  36837  poimirlem13  38007  poimirlem14  38008  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  mblfinlem2  38032  ovoliunnfl  38036  voliunnfl  38038  facp2  42635  dvdsexpnn0  42818  renegmulnnass  42962  fimgmcyc  43027  dffltz  43091  irrapxlem1  43274  pellexlem1  43281  pellqrex  43331  2nn0ind  43397  jm2.17c  43414  acongrep  43432  jm2.18  43440  jm2.20nn  43449  jm2.16nn0  43456  proot1ex  43648  hashnzfzclim  44773  binomcxplemnotnn0  44807  nnsplit  45810  clim1fr1  46053  sumnnodd  46082  wallispilem4  46518  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  wallispi2lem2  46522  wallispi2  46523  stirlinglem1  46524  stirlinglem3  46526  stirlinglem4  46527  stirlinglem5  46528  stirlinglem6  46529  stirlinglem7  46530  stirlinglem8  46531  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  stirlinglem13  46536  stirlinglem14  46537  stirlinglem15  46538  dirkerper  46546  dirkertrigeqlem1  46548  fouriersw  46681  nnfoctbdjlem  46905  deccarry  47781  subsubelfzo0  47797  submodlt  47826  mod0mul  47832  m1modmmod  47834  modlt0b  47839  sqrtpwpw2p  48023  fmtnodvds  48029  fmtnoprmfac1  48050  fmtnoprmfac2lem1  48051  fmtnoprmfac2  48052  lighneallem2  48091  lighneallem3  48092  lighneallem4  48095  nnennexALTV  48199  perfectALTV  48221  fppr2odd  48229  fpprwppr  48237  fpprwpprb  48238  tgoldbachlt  48314  gpgedgvtx0  48559  gpg3kgrtriexlem2  48582  gpg3kgrtriexlem5  48585  gpg3kgrtriex  48587  nnsgrp  48675  nnsgrpnmnd  48676  bcpascm1  48849  altgsumbcALT  48851  eluz2cnn0n1  49009  pw2m1lepw2m1  49018  nnennex  49023  logbpw2m1  49065  blenpw2m1  49077  nnpw2blen  49078  nnpw2pmod  49081  blennnt2  49087  blennn0em1  49089  nn0digval  49098  dignn0fr  49099  dignn0ldlem  49100  dig0  49104  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  nn0sumshdiglem1  49119