MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nncn Structured version   Visualization version   GIF version

Theorem nncn 12119
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
Assertion
Ref Expression
nncn (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Proof of Theorem nncn
StepHypRef Expression
1 nnsscn 12116 . 2 ℕ ⊆ ℂ
21sseli 3938 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  cc 11007  cn 12111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7664  ax-1cn 11067  ax-addcl 11069
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7354  df-om 7795  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-nn 12112
This theorem is referenced by:  nncni  12121  nn1m1nn  12132  nn1suc  12133  nnaddcl  12134  nnmulcl  12135  nnmtmip  12137  nnneneg  12146  nnsub  12155  nndiv  12157  nndivtr  12158  nnnn0addcl  12401  nn0nnaddcl  12402  elnnnn0  12414  nn0sub  12421  nnnegz  12460  elz2  12475  zaddcl  12501  nnaddm1cl  12518  zdiv  12531  zdivadd  12532  zdivmul  12533  nneo  12545  peano5uzi  12550  elq  12829  qmulz  12830  qaddcl  12844  qnegcl  12845  qmulcl  12846  qreccl  12848  rpnnen1lem5  12860  nnledivrp  12981  nn0ledivnn  12982  fseq1m1p1  13470  ubmelm1fzo  13622  subfzo0  13648  quoremz  13714  quoremnn0ALT  13716  intfracq  13718  fldiv  13719  fldiv2  13720  modmulnn  13748  addmodid  13778  addmodidr  13779  modaddmodup  13793  modfzo0difsn  13802  modsumfzodifsn  13803  addmodlteq  13805  nn0ennn  13838  ser1const  13918  expneg  13929  expm1t  13950  nnsqcl  13987  nnlesq  14063  digit2  14093  digit1  14094  expnngt1  14098  facdiv  14141  facndiv  14142  faclbnd  14144  faclbnd4lem1  14147  faclbnd4lem4  14150  bcn1  14167  bcm1k  14169  bcp1n  14170  bcval5  14172  bcn2m1  14178  cshwidxmod  14649  cshwidxm  14654  cshwidxn  14655  repswcshw  14658  isercoll2  15513  divcnv  15698  harmonic  15704  arisum  15705  arisum2  15706  expcnv  15709  pwdif  15713  geomulcvg  15721  mertenslem2  15730  ef0lem  15921  efexp  15943  ruclem12  16083  sqrt2irr  16091  nndivides  16106  modmulconst  16130  dvdsflip  16159  nn0enne  16219  nno  16224  pwp1fsum  16233  divalgmod  16248  ndvdsadd  16252  modgcd  16373  gcdmultiplez  16376  gcddiv  16392  rpmulgcd  16397  rplpwr  16398  sqgcd  16401  lcmgcdlem  16442  qredeq  16493  qredeu  16494  cncongrcoprm  16506  prmind2  16521  isprm6  16550  divnumden  16583  divdenle  16584  nn0gcdsq  16587  hashgcdlem  16620  pythagtriplem1  16648  pythagtriplem2  16649  pythagtriplem6  16653  pythagtriplem7  16654  pythagtriplem12  16658  pythagtriplem14  16660  pythagtriplem15  16661  pythagtriplem16  16662  pythagtriplem17  16663  pythagtriplem19  16665  pcqcl  16688  pcexp  16691  pcneg  16706  fldivp1  16729  oddprmdvds  16735  prmpwdvds  16736  infpnlem2  16743  prmreclem1  16748  prmreclem6  16753  4sqlem19  16795  vdwapun  16806  vdwapid1  16807  prmonn2  16871  prmgaplem7  16889  mulgnegnn  18845  mulgnnass  18870  mulgmodid  18874  odmod  19287  cnfldmulg  20782  prmirredlem  20846  znidomb  20921  znrrg  20925  cply1mul  21617  chfacfscmul0  22159  chfacfscmulfsupp  22160  chfacfscmulgsum  22161  chfacfpmmul0  22163  chfacfpmmulfsupp  22164  chfacfpmmulgsum  22165  cayhamlem1  22167  cpmadugsumlemF  22177  ovolunlem1  24813  uniioombllem3  24901  vitali  24929  mbfi1fseqlem3  25034  dvexp  25269  dvexp3  25294  plyeq0lem  25523  dgrcolem1  25586  aaliou3lem2  25655  aaliou3lem7  25661  pserdv2  25741  abelthlem6  25747  logtayl  25967  logtaylsum  25968  logtayl2  25969  cxpexp  25975  cxproot  25997  root1id  26059  root1eq1  26060  cxpeq  26062  logbgcd1irr  26096  atantayl  26239  atantayl2  26240  birthdaylem2  26254  dfef2  26272  emcllem2  26298  emcllem3  26299  zetacvg  26316  lgam1  26365  gamfac  26368  basellem2  26383  basellem3  26384  basellem5  26386  basellem8  26389  mumul  26482  fsumdvdscom  26486  muinv  26494  chtublem  26511  perfect  26531  pcbcctr  26576  bclbnd  26580  bposlem1  26584  bposlem6  26589  lgssq2  26638  gausslemma2dlem1a  26665  gausslemma2dlem3  26668  2lgslem1a1  26689  2sqlem6  26723  2sqlem10  26728  2sqnn  26739  2sqreunnltlem  26750  rplogsumlem1  26784  dchrmusumlema  26793  dchrmusum2  26794  dchrvmasumiflem1  26801  dchrvmaeq0  26804  dchrisum0re  26813  logdivbnd  26856  cusgrsize2inds  28230  wlkdlem2  28460  crctcshwlkn0lem1  28584  crctcshwlkn0lem6  28589  0enwwlksnge1  28638  wspthsnonn0vne  28691  clwwlknwwlksn  28811  clwwlkinwwlk  28813  clwwlkel  28819  clwwlkf  28820  clwwlkf1  28822  wwlksubclwwlk  28831  eucrctshift  29016  eucrct2eupth  29018  numclwwlk2lem1  29149  numclwlk2lem2f  29150  numclwlk2lem2f1o  29152  ipasslem4  29605  ipasslem5  29606  isarchi3  31849  oddpwdc  32766  eulerpartlemb  32780  fibp1  32813  subfacp1lem6  33591  subfaclim  33594  snmlff  33735  circum  34074  divcnvlin  34121  bcprod  34127  iprodgam  34131  faclim  34135  faclim2  34137  nn0prpwlem  34732  nndivsub  34867  knoppndvlem13  34925  poimirlem13  36029  poimirlem14  36030  poimirlem29  36045  poimirlem30  36046  poimirlem31  36047  poimirlem32  36048  mblfinlem2  36054  ovoliunnfl  36058  voliunnfl  36060  facp2  40489  metakunt16  40530  metakunt30  40544  fac2xp3  40550  nnadd1com  40692  nnaddcom  40693  expgcd  40729  nn0expgcd  40730  dvdsexpnn0  40736  renegmulnnass  40831  dffltz  40881  irrapxlem1  41054  pellexlem1  41061  pellqrex  41111  2nn0ind  41178  jm2.17c  41195  acongrep  41213  jm2.18  41221  jm2.20nn  41230  jm2.16nn0  41237  proot1ex  41437  hashnzfzclim  42513  binomcxplemnotnn0  42547  nnsplit  43497  clim1fr1  43743  sumnnodd  43772  wallispilem4  44210  wallispilem5  44211  wallispi  44212  wallispi2lem1  44213  wallispi2lem2  44214  wallispi2  44215  stirlinglem1  44216  stirlinglem3  44218  stirlinglem4  44219  stirlinglem5  44220  stirlinglem6  44221  stirlinglem7  44222  stirlinglem8  44223  stirlinglem10  44225  stirlinglem11  44226  stirlinglem12  44227  stirlinglem13  44228  stirlinglem14  44229  stirlinglem15  44230  dirkerper  44238  dirkertrigeqlem1  44240  fouriersw  44373  nnfoctbdjlem  44597  deccarry  45444  subsubelfzo0  45459  sqrtpwpw2p  45631  fmtnodvds  45637  fmtnoprmfac1  45658  fmtnoprmfac2lem1  45659  fmtnoprmfac2  45660  lighneallem2  45699  lighneallem3  45700  lighneallem4  45703  nnennexALTV  45794  perfectALTV  45816  fppr2odd  45824  fpprwppr  45832  fpprwpprb  45833  tgoldbachlt  45909  nnsgrp  46012  nnsgrpnmnd  46013  bcpascm1  46328  altgsumbcALT  46330  eluz2cnn0n1  46493  pw2m1lepw2m1  46502  mod0mul  46506  m1modmmod  46508  nnennex  46512  logbpw2m1  46554  blenpw2m1  46566  nnpw2blen  46567  nnpw2pmod  46570  blennnt2  46576  blennn0em1  46578  nn0digval  46587  dignn0fr  46588  dignn0ldlem  46589  dig0  46593  nn0sumshdiglemA  46606  nn0sumshdiglemB  46607  nn0sumshdiglem1  46608
  Copyright terms: Public domain W3C validator