Theorem nncn 12253

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11132  ℕcn 12245

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734  ax-1cn 11192  ax-addcl 11194

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-nn 12246

This theorem is referenced by:  nncni  12255  nn1m1nn  12266  nn1suc  12267  nnaddcl  12268  nnmulcl  12269  nnmtmip  12271  nnneneg  12280  nnsub  12289  nndiv  12291  nndivtr  12292  nnnn0addcl  12536  nn0nnaddcl  12537  elnnnn0  12549  nn0sub  12556  nnnegz  12596  elz2  12611  zaddcl  12637  nnaddm1cl  12655  zdiv  12668  zdivadd  12669  zdivmul  12670  nneo  12682  peano5uzi  12687  elq  12971  qmulz  12972  qaddcl  12986  qnegcl  12987  qmulcl  12988  qreccl  12990  rpnnen1lem5  13002  nnledivrp  13126  nn0ledivnn  13127  fseq1m1p1  13621  ubmelm1fzo  13784  subfzo0  13810  quoremz  13877  quoremnn0ALT  13879  intfracq  13881  fldiv  13882  fldiv2  13883  modmulnn  13911  addmodid  13942  addmodidr  13943  modaddmodup  13957  modfzo0difsn  13966  modsumfzodifsn  13967  addmodlteq  13969  nn0ennn  14002  ser1const  14081  expneg  14092  expm1t  14113  nnsqcl  14151  nnlesq  14228  digit2  14259  digit1  14260  expnngt1  14264  facdiv  14310  facndiv  14311  faclbnd  14313  faclbnd4lem1  14316  faclbnd4lem4  14319  bcn1  14336  bcm1k  14338  bcp1n  14339  bcval5  14341  bcn2m1  14347  cshwidxmod  14826  cshwidxm  14831  cshwidxn  14832  repswcshw  14835  isercoll2  15690  divcnv  15874  harmonic  15880  arisum  15881  arisum2  15882  expcnv  15885  pwdif  15889  geomulcvg  15897  mertenslem2  15906  ef0lem  16099  efexp  16124  ruclem12  16264  sqrt2irr  16272  nndivides  16287  modmulconst  16312  dvdsflip  16341  nn0enne  16401  nno  16406  pwp1fsum  16415  divalgmod  16430  ndvdsadd  16434  modgcd  16556  gcdmultiplez  16559  gcddiv  16575  rpmulgcd  16581  rplpwr  16582  sqgcd  16586  expgcd  16587  nn0expgcd  16588  lcmgcdlem  16630  qredeq  16681  qredeu  16682  cncongrcoprm  16694  prmind2  16709  isprm6  16738  divnumden  16772  divdenle  16773  nn0gcdsq  16776  hashgcdlem  16812  pythagtriplem1  16841  pythagtriplem2  16842  pythagtriplem6  16846  pythagtriplem7  16847  pythagtriplem12  16851  pythagtriplem14  16853  pythagtriplem15  16854  pythagtriplem16  16855  pythagtriplem17  16856  pythagtriplem19  16858  pcqcl  16881  pcexp  16884  pcneg  16899  fldivp1  16922  oddprmdvds  16928  prmpwdvds  16929  infpnlem2  16936  prmreclem1  16941  prmreclem6  16946  4sqlem19  16988  vdwapun  16999  vdwapid1  17000  prmonn2  17064  prmgaplem7  17082  mulgnegnn  19072  mulgnnass  19097  mulgmodid  19101  odmod  19532  cnfldmulg  21371  prmirredlem  21438  znidomb  21527  znrrg  21531  cply1mul  22239  chfacfscmul0  22801  chfacfscmulfsupp  22802  chfacfscmulgsum  22803  chfacfpmmul0  22805  chfacfpmmulfsupp  22806  chfacfpmmulgsum  22807  cayhamlem1  22809  cpmadugsumlemF  22819  ovolunlem1  25455  uniioombllem3  25543  vitali  25571  mbfi1fseqlem3  25675  dvexp  25914  dvexp3  25939  plyeq0lem  26172  dgrcolem1  26236  aaliou3lem2  26308  aaliou3lem7  26314  pserdv2  26397  abelthlem6  26403  logtayl  26626  logtaylsum  26627  logtayl2  26628  cxpexp  26634  cxproot  26656  root1id  26721  root1eq1  26722  cxpeq  26724  logbgcd1irr  26761  atantayl  26904  atantayl2  26905  birthdaylem2  26919  dfef2  26938  emcllem2  26964  emcllem3  26965  zetacvg  26982  lgam1  27031  gamfac  27034  basellem2  27049  basellem3  27050  basellem5  27052  basellem8  27055  mumul  27148  fsumdvdscom  27152  muinv  27160  chtublem  27179  perfect  27199  pcbcctr  27244  bclbnd  27248  bposlem1  27252  bposlem6  27257  lgssq2  27306  gausslemma2dlem1a  27333  gausslemma2dlem3  27336  2lgslem1a1  27357  2sqlem6  27391  2sqlem10  27396  2sqnn  27407  2sqreunnltlem  27418  rplogsumlem1  27452  dchrmusumlema  27461  dchrmusum2  27462  dchrvmasumiflem1  27469  dchrvmaeq0  27472  dchrisum0re  27481  logdivbnd  27524  cusgrsize2inds  29438  wlkdlem2  29668  crctcshwlkn0lem1  29797  crctcshwlkn0lem6  29802  0enwwlksnge1  29851  wspthsnonn0vne  29904  clwwlknwwlksn  30024  clwwlkinwwlk  30026  clwwlkel  30032  clwwlkf  30033  clwwlkf1  30035  wwlksubclwwlk  30044  eucrctshift  30229  eucrct2eupth  30231  numclwwlk2lem1  30362  numclwlk2lem2f  30363  numclwlk2lem2f1o  30365  ipasslem4  30820  ipasslem5  30821  isarchi3  33190  oddpwdc  34391  eulerpartlemb  34405  fibp1  34438  subfacp1lem6  35212  subfaclim  35215  snmlff  35356  circum  35701  divcnvlin  35755  bcprod  35760  iprodgam  35764  faclim  35768  faclim2  35770  nn0prpwlem  36345  nndivsub  36480  knoppndvlem13  36547  poimirlem13  37662  poimirlem14  37663  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimirlem32  37681  mblfinlem2  37687  ovoliunnfl  37691  voliunnfl  37693  facp2  42161  nnadd1com  42285  nnaddcom  42286  dvdsexpnn0  42352  renegmulnnass  42471  fimgmcyc  42532  dffltz  42632  irrapxlem1  42820  pellexlem1  42827  pellqrex  42877  2nn0ind  42944  jm2.17c  42961  acongrep  42979  jm2.18  42987  jm2.20nn  42996  jm2.16nn0  43003  proot1ex  43195  hashnzfzclim  44321  binomcxplemnotnn0  44355  nnsplit  45365  clim1fr1  45610  sumnnodd  45639  wallispilem4  46077  wallispilem5  46078  wallispi  46079  wallispi2lem1  46080  wallispi2lem2  46081  wallispi2  46082  stirlinglem1  46083  stirlinglem3  46085  stirlinglem4  46086  stirlinglem5  46087  stirlinglem6  46088  stirlinglem7  46089  stirlinglem8  46090  stirlinglem10  46092  stirlinglem11  46093  stirlinglem12  46094  stirlinglem13  46095  stirlinglem14  46096  stirlinglem15  46097  dirkerper  46105  dirkertrigeqlem1  46107  fouriersw  46240  nnfoctbdjlem  46464  deccarry  47320  subsubelfzo0  47335  submodlt  47359  sqrtpwpw2p  47532  fmtnodvds  47538  fmtnoprmfac1  47559  fmtnoprmfac2lem1  47560  fmtnoprmfac2  47561  lighneallem2  47600  lighneallem3  47601  lighneallem4  47604  nnennexALTV  47695  perfectALTV  47717  fppr2odd  47725  fpprwppr  47733  fpprwpprb  47734  tgoldbachlt  47810  gpgedgvtx0  48045  gpg3kgrtriexlem2  48066  gpg3kgrtriexlem5  48069  gpg3kgrtriex  48071  nnsgrp  48132  nnsgrpnmnd  48133  bcpascm1  48306  altgsumbcALT  48308  eluz2cnn0n1  48467  pw2m1lepw2m1  48476  mod0mul  48479  m1modmmod  48481  nnennex  48485  logbpw2m1  48527  blenpw2m1  48539  nnpw2blen  48540  nnpw2pmod  48543  blennnt2  48549  blennn0em1  48551  nn0digval  48560  dignn0fr  48561  dignn0ldlem  48562  dig0  48566  nn0sumshdiglemA  48579  nn0sumshdiglemB  48580  nn0sumshdiglem1  48581