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

Theorem nncn 11635
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 11632 . 2 ℕ ⊆ ℂ
21sseli 3962 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cc 10524  cn 11627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584  ax-addcl 10586
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628
This theorem is referenced by:  nncni  11637  nn1m1nn  11647  nn1suc  11648  nnaddcl  11649  nnmulcl  11650  nnmtmip  11652  nnneneg  11661  nnsub  11670  nndiv  11672  nndivtr  11673  nnnn0addcl  11916  nn0nnaddcl  11917  elnnnn0  11929  nn0sub  11936  nnnegz  11973  elz2  11988  zaddcl  12011  nnaddm1cl  12028  zdiv  12041  zdivadd  12042  zdivmul  12043  nneo  12055  peano5uzi  12060  elq  12339  qmulz  12340  qaddcl  12354  qnegcl  12355  qmulcl  12356  qreccl  12358  rpnnen1lem5  12370  nnledivrp  12491  nn0ledivnn  12492  fseq1m1p1  12972  ubmelm1fzo  13123  subfzo0  13149  quoremz  13213  quoremnn0ALT  13215  intfracq  13217  fldiv  13218  fldiv2  13219  modmulnn  13247  addmodid  13277  addmodidr  13278  modaddmodup  13292  modfzo0difsn  13301  modsumfzodifsn  13302  addmodlteq  13304  nn0ennn  13337  ser1const  13416  expneg  13427  expm1t  13447  nnsqcl  13483  nnlesq  13558  digit2  13587  digit1  13588  expnngt1  13592  facdiv  13637  facndiv  13638  faclbnd  13640  faclbnd4lem1  13643  faclbnd4lem4  13646  bcn1  13663  bcm1k  13665  bcp1n  13666  bcval5  13668  bcn2m1  13674  cshwidxmod  14155  cshwidxm  14160  cshwidxn  14161  repswcshw  14164  isercoll2  15015  divcnv  15198  harmonic  15204  arisum  15205  arisum2  15206  expcnv  15209  pwdif  15213  geomulcvg  15222  mertenslem2  15231  ef0lem  15422  efexp  15444  ruclem12  15584  sqrt2irr  15592  nndivides  15607  modmulconst  15631  dvdsflip  15657  nn0enne  15718  nno  15723  pwp1fsum  15732  divalgmod  15747  ndvdsadd  15751  modgcd  15870  gcdmultiplez  15873  gcddiv  15889  gcdmultipleOLD  15890  gcdmultiplezOLD  15891  rpmulgcd  15896  rplpwr  15897  sqgcd  15899  lcmgcdlem  15940  qredeq  15991  qredeu  15992  cncongrcoprm  16004  prmind2  16019  isprm6  16048  divnumden  16078  divdenle  16079  nn0gcdsq  16082  hashgcdlem  16115  pythagtriplem1  16143  pythagtriplem2  16144  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem15  16156  pythagtriplem16  16157  pythagtriplem17  16158  pythagtriplem19  16160  pcqcl  16183  pcexp  16186  pcneg  16200  fldivp1  16223  oddprmdvds  16229  prmpwdvds  16230  infpnlem2  16237  prmreclem1  16242  prmreclem6  16247  4sqlem19  16289  vdwapun  16300  vdwapid1  16301  prmonn2  16365  prmgaplem7  16383  mulgnegnn  18178  mulgnnass  18202  mulgmodid  18206  odmod  18605  cply1mul  20392  cnfldmulg  20507  prmirredlem  20570  znidomb  20638  znrrg  20642  chfacfscmul0  21396  chfacfscmulfsupp  21397  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulfsupp  21401  chfacfpmmulgsum  21402  cayhamlem1  21404  cpmadugsumlemF  21414  ovolunlem1  24027  uniioombllem3  24115  vitali  24143  mbfi1fseqlem3  24247  dvexp  24479  dvexp3  24504  plyeq0lem  24729  dgrcolem1  24792  aaliou3lem2  24861  aaliou3lem7  24867  pserdv2  24947  abelthlem6  24953  logtayl  25170  logtaylsum  25171  logtayl2  25172  cxpexp  25178  cxproot  25200  root1id  25262  root1eq1  25263  cxpeq  25265  logbgcd1irr  25299  atantayl  25442  atantayl2  25443  birthdaylem2  25458  dfef2  25476  emcllem2  25502  emcllem3  25503  zetacvg  25520  lgam1  25569  gamfac  25572  basellem2  25587  basellem3  25588  basellem5  25590  basellem8  25593  mumul  25686  fsumdvdscom  25690  muinv  25698  chtublem  25715  perfect  25735  pcbcctr  25780  bclbnd  25784  bposlem1  25788  bposlem6  25793  lgssq2  25842  gausslemma2dlem1a  25869  gausslemma2dlem3  25872  2lgslem1a1  25893  2sqlem6  25927  2sqlem10  25932  2sqnn  25943  2sqreunnltlem  25954  rplogsumlem1  25988  dchrmusumlema  25997  dchrmusum2  25998  dchrvmasumiflem1  26005  dchrvmaeq0  26008  dchrisum0re  26017  logdivbnd  26060  cusgrsize2inds  27163  wlkdlem2  27393  crctcshwlkn0lem1  27516  crctcshwlkn0lem6  27521  0enwwlksnge1  27570  wspthsnonn0vne  27624  clwwlknwwlksn  27744  clwwlkinwwlk  27746  clwwlkel  27753  clwwlkf  27754  clwwlkf1  27756  wwlksubclwwlk  27765  eucrctshift  27950  eucrct2eupth  27952  numclwwlk2lem1  28083  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  ipasslem4  28539  ipasslem5  28540  isarchi3  30744  oddpwdc  31512  eulerpartlemb  31526  fibp1  31559  subfacp1lem6  32330  subfaclim  32333  snmlff  32474  circum  32815  divcnvlin  32862  bcprod  32868  iprodgam  32872  faclim  32876  faclim2  32878  nn0prpwlem  33568  nndivsub  33703  knoppndvlem13  33761  poimirlem13  34787  poimirlem14  34788  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  mblfinlem2  34812  ovoliunnfl  34816  voliunnfl  34818  nnadd1com  39040  nnaddcom  39041  expgcd  39063  nn0expgcd  39064  dffltz  39151  irrapxlem1  39299  pellexlem1  39306  pellqrex  39356  2nn0ind  39422  jm2.17c  39439  acongrep  39457  jm2.18  39465  jm2.20nn  39474  jm2.16nn0  39481  proot1ex  39681  hashnzfzclim  40534  binomcxplemnotnn0  40568  nnsplit  41506  clim1fr1  41762  sumnnodd  41791  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem8  42247  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  stirlinglem14  42253  stirlinglem15  42254  dirkerper  42262  dirkertrigeqlem1  42264  fouriersw  42397  nnfoctbdjlem  42618  deccarry  43392  subsubelfzo0  43407  sqrtpwpw2p  43547  fmtnodvds  43553  fmtnoprmfac1  43574  fmtnoprmfac2lem1  43575  fmtnoprmfac2  43576  lighneallem2  43618  lighneallem3  43619  lighneallem4  43622  nnennexALTV  43713  perfectALTV  43735  fppr2odd  43743  fpprwppr  43751  fpprwpprb  43752  tgoldbachlt  43828  nnsgrp  43931  nnsgrpnmnd  43932  bcpascm1  44297  altgsumbcALT  44299  eluz2cnn0n1  44464  pw2m1lepw2m1  44473  mod0mul  44477  m1modmmod  44479  nnennex  44483  logbpw2m1  44525  blenpw2m1  44537  nnpw2blen  44538  nnpw2pmod  44541  blennnt2  44547  blennn0em1  44549  nn0digval  44558  dignn0fr  44559  dignn0ldlem  44560  dig0  44564  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  nn0sumshdiglem1  44579
  Copyright terms: Public domain W3C validator