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

Theorem nncn 10877
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 10874 . 2 ℕ ⊆ ℂ
21sseli 3563 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9790  cn 10869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-ov 6529  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-nn 10870
This theorem is referenced by:  nn1m1nn  10889  nn1suc  10890  nnaddcl  10891  nnmulcl  10892  nnsub  10908  nndiv  10910  nndivtr  10911  nnnn0addcl  11172  nn0nnaddcl  11173  elnnnn0  11185  nn0sub  11192  nnnegz  11215  elz2  11229  zaddcl  11252  nnaddm1cl  11269  zdiv  11281  zdivadd  11282  zdivmul  11283  nneo  11295  peano5uzi  11300  elq  11624  qmulz  11625  qaddcl  11638  qnegcl  11639  qmulcl  11640  qreccl  11642  rpnnen1lem5  11652  rpnnen1lem5OLD  11658  nnledivrp  11774  nn0ledivnn  11775  fseq1m1p1  12241  ubmelm1fzo  12387  subfzo0  12409  quoremz  12473  quoremnn0ALT  12475  intfracq  12477  fldiv  12478  fldiv2  12479  modmulnn  12507  addmodid  12537  addmodidr  12538  modaddmodup  12552  modfzo0difsn  12561  modsumfzodifsn  12562  addmodlteq  12564  nn0ennn  12597  ser1const  12676  expneg  12687  expm1t  12707  nnsqcl  12752  nnlesq  12787  digit2  12816  digit1  12817  facdiv  12893  facndiv  12894  faclbnd  12896  faclbnd4lem1  12899  faclbnd4lem4  12902  bcn1  12919  bcm1k  12921  bcp1n  12922  bcval5  12924  bcn2m1  12930  swrdccatwrd  13268  cshwidxmod  13348  cshwidxm  13353  cshwidxn  13354  repswcshw  13357  isercoll2  14195  divcnv  14372  harmonic  14378  arisum  14379  arisum2  14380  expcnv  14383  geomulcvg  14394  mertenslem2  14404  ef0lem  14596  efexp  14618  ruclem12  14757  sqrt2irr  14765  nndivides  14776  modmulconst  14799  dvdsflip  14825  nn0enne  14880  nno  14884  pwp1fsum  14900  divalgmod  14915  divalgmodOLD  14916  ndvdsadd  14920  modgcd  15039  gcddiv  15054  gcdmultiple  15055  gcdmultiplez  15056  rpmulgcd  15061  rplpwr  15062  sqgcd  15064  lcmgcdlem  15105  qredeq  15157  qredeu  15158  cncongrcoprm  15170  prmind2  15184  isprm6  15212  divnumden  15242  divdenle  15243  nn0gcdsq  15246  hashgcdlem  15279  pythagtriplem1  15307  pythagtriplem2  15308  pythagtriplem6  15312  pythagtriplem7  15313  pythagtriplem12  15317  pythagtriplem14  15319  pythagtriplem15  15320  pythagtriplem16  15321  pythagtriplem17  15322  pythagtriplem19  15324  pcqcl  15347  pcexp  15350  pcneg  15364  fldivp1  15387  oddprmdvds  15393  prmpwdvds  15394  infpnlem2  15401  prmreclem1  15406  prmreclem6  15411  4sqlem19  15453  vdwapun  15464  vdwapid1  15465  prmonn2  15529  prmgaplem7  15547  mulgnegnn  17322  mulgnnass  17347  mulgnnassOLD  17348  mulgmodid  17352  odmod  17736  cply1mul  19433  cnfldmulg  19545  prmirredlem  19607  znidomb  19676  znrrg  19680  chfacfscmul0  20429  chfacfscmulfsupp  20430  chfacfscmulgsum  20431  chfacfpmmul0  20433  chfacfpmmulfsupp  20434  chfacfpmmulgsum  20435  cayhamlem1  20437  cpmadugsumlemF  20447  ovolunlem1  23016  uniioombllem3  23103  vitali  23132  mbfi1fseqlem3  23234  dvexp  23466  dvexp3  23489  plyeq0lem  23714  dgrcolem1  23777  aaliou3lem2  23846  aaliou3lem7  23852  pserdv2  23932  abelthlem6  23938  logtayl  24150  logtaylsum  24151  logtayl2  24152  cxpexp  24158  cxproot  24180  root1id  24239  root1eq1  24240  cxpeq  24242  atantayl  24408  atantayl2  24409  birthdaylem2  24423  dfef2  24441  emcllem2  24467  emcllem3  24468  zetacvg  24485  lgam1  24534  gamfac  24537  basellem2  24552  basellem3  24553  basellem5  24555  basellem8  24558  mumul  24651  fsumdvdscom  24655  muinv  24663  chtublem  24680  perfect  24700  pcbcctr  24745  bclbnd  24749  bposlem1  24753  bposlem6  24758  lgssq2  24807  gausslemma2dlem1a  24834  gausslemma2dlem3  24837  2lgslem1a1  24858  2sqlem6  24892  2sqlem10  24897  rplogsumlem1  24917  dchrmusumlema  24926  dchrmusum2  24927  dchrvmasumiflem1  24934  dchrvmaeq0  24937  dchrisum0re  24946  logdivbnd  24989  cusgrasize2inds  25798  clwwlkel  26114  clwwlkf  26115  clwwlkf1  26117  wwlksubclwwlk  26125  rusgra0edg  26275  clwwlkextfrlem1  26396  numclwwlk2lem1  26422  numclwlk2lem2f  26423  numclwlk2lem2f1o  26425  ipasslem4  26866  ipasslem5  26867  isarchi3  28865  oddpwdc  29536  eulerpartlemb  29550  fibp1  29583  subfacp1lem6  30214  subfaclim  30217  snmlff  30358  circum  30615  divcnvlin  30664  bcprod  30670  iprodgam  30674  faclim  30678  faclim2  30680  nn0prpwlem  31280  nndivsub  31419  knoppndvlem13  31478  poimirlem13  32375  poimirlem14  32376  poimirlem29  32391  poimirlem30  32392  poimirlem31  32393  poimirlem32  32394  mblfinlem2  32400  ovoliunnfl  32404  voliunnfl  32406  irrapxlem1  36187  pellexlem1  36194  pellqrex  36244  2nn0ind  36311  jm2.17c  36330  acongrep  36348  jm2.18  36356  jm2.20nn  36365  jm2.16nn0  36372  proot1ex  36581  hashnzfzclim  37326  binomcxplemnotnn0  37360  nnsplit  38298  clim1fr1  38451  sumnnodd  38480  wallispilem4  38744  wallispilem5  38745  wallispi  38746  wallispi2lem1  38747  wallispi2lem2  38748  wallispi2  38749  stirlinglem1  38750  stirlinglem3  38752  stirlinglem4  38753  stirlinglem5  38754  stirlinglem6  38755  stirlinglem7  38756  stirlinglem8  38757  stirlinglem10  38759  stirlinglem11  38760  stirlinglem12  38761  stirlinglem13  38762  stirlinglem14  38763  stirlinglem15  38764  dirkerper  38772  dirkertrigeqlem1  38774  fouriersw  38907  nnfoctbdjlem  39131  deccarry  39725  sqrtpwpw2p  39772  fmtnodvds  39778  fmtnoprmfac1  39799  fmtnoprmfac2lem1  39800  fmtnoprmfac2  39801  pwdif  39823  lighneallem2  39845  lighneallem3  39846  lighneallem4  39849  perfectALTV  39950  tgoldbachlt  40014  tgoldbachltOLD  40021  subsubelfzo0  40165  cusgrsize2inds  40650  1wlkdlem2  40873  crctcsh1wlkn0lem1  40994  crctcsh1wlkn0lem6  40999  0enwwlksnge1  41041  wspthsnonn0vne  41105  clwwlksel  41202  clwwlksf  41203  clwwlksf1  41205  wwlksubclwwlks  41213  eucrctshift  41392  eucrct2eupth  41394  av-numclwwlk2lem1  41513  av-numclwlk2lem2f  41514  av-numclwlk2lem2f1o  41516  nnsgrp  41588  nnsgrpnmnd  41589  bcpascm1  41903  altgsumbcALT  41905  eluz2cnn0n1  42076  pw2m1lepw2m1  42085  mod0mul  42089  m1modmmod  42091  logbpw2m1  42140  blenpw2m1  42152  nnpw2blen  42153  nnpw2pmod  42156  blennnt2  42162  blennn0em1  42164  nn0digval  42173  dignn0fr  42174  dignn0ldlem  42175  dig0  42179  nn0sumshdiglemA  42192  nn0sumshdiglemB  42193  nn0sumshdiglem1  42194
  Copyright terms: Public domain W3C validator