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

Theorem nncn 11323
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 11319 . 2 ℕ ⊆ ℂ
21sseli 3805 1 (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cc 10228  cn 11314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-1cn 10288  ax-addcl 10290
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-ov 6886  df-om 7305  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-nn 11315
This theorem is referenced by:  nncni  11325  nn1m1nn  11336  nn1suc  11337  nnaddcl  11338  nnmulcl  11339  nnmulclOLD  11340  nnsub  11356  nndiv  11358  nndivtr  11359  nnnn0addcl  11608  nn0nnaddcl  11609  elnnnn0  11621  nn0sub  11628  nnnegz  11665  elz2  11679  zaddcl  11702  nnaddm1cl  11719  zdiv  11732  zdivadd  11733  zdivmul  11734  nneo  11746  peano5uzi  11751  elq  12028  qmulz  12029  qaddcl  12042  qnegcl  12043  qmulcl  12044  qreccl  12046  rpnnen1lem5  12056  nnledivrp  12175  nn0ledivnn  12176  fseq1m1p1  12657  ubmelm1fzo  12807  subfzo0  12833  quoremz  12897  quoremnn0ALT  12899  intfracq  12901  fldiv  12902  fldiv2  12903  modmulnn  12931  addmodid  12961  addmodidr  12962  modaddmodup  12976  modfzo0difsn  12985  modsumfzodifsn  12986  addmodlteq  12988  nn0ennn  13021  ser1const  13099  expneg  13110  expm1t  13130  nnsqcl  13175  nnlesq  13210  digit2  13239  digit1  13240  facdiv  13313  facndiv  13314  faclbnd  13316  faclbnd4lem1  13319  faclbnd4lem4  13322  bcn1  13339  bcm1k  13341  bcp1n  13342  bcval5  13344  bcn2m1  13350  swrdccatwrd  13711  cshwidxmod  13792  cshwidxm  13797  cshwidxn  13798  repswcshw  13801  isercoll2  14641  divcnv  14826  harmonic  14832  arisum  14833  arisum2  14834  expcnv  14837  geomulcvg  14848  mertenslem2  14857  ef0lem  15048  efexp  15070  ruclem12  15209  sqrt2irr  15218  nndivides  15232  modmulconst  15255  dvdsflip  15281  nn0enne  15333  nno  15337  pwp1fsum  15353  divalgmod  15368  ndvdsadd  15372  modgcd  15491  gcddiv  15506  gcdmultiple  15507  gcdmultiplez  15508  rpmulgcd  15513  rplpwr  15514  sqgcd  15516  lcmgcdlem  15557  qredeq  15608  qredeu  15609  cncongrcoprm  15621  prmind2  15635  isprm6  15662  divnumden  15692  divdenle  15693  nn0gcdsq  15696  hashgcdlem  15729  pythagtriplem1  15757  pythagtriplem2  15758  pythagtriplem6  15762  pythagtriplem7  15763  pythagtriplem12  15767  pythagtriplem14  15769  pythagtriplem15  15770  pythagtriplem16  15771  pythagtriplem17  15772  pythagtriplem19  15774  pcqcl  15797  pcexp  15800  pcneg  15814  fldivp1  15837  oddprmdvds  15843  prmpwdvds  15844  infpnlem2  15851  prmreclem1  15856  prmreclem6  15861  4sqlem19  15903  vdwapun  15914  vdwapid1  15915  prmonn2  15979  prmgaplem7  15997  mulgnegnn  17775  mulgnnass  17798  mulgmodid  17802  odmod  18185  cply1mul  19891  cnfldmulg  20005  prmirredlem  20068  znidomb  20136  znrrg  20140  chfacfscmul0  20896  chfacfscmulfsupp  20897  chfacfscmulgsum  20898  chfacfpmmul0  20900  chfacfpmmulfsupp  20901  chfacfpmmulgsum  20902  cayhamlem1  20904  cpmadugsumlemF  20914  ovolunlem1  23500  uniioombllem3  23588  vitali  23616  mbfi1fseqlem3  23720  dvexp  23952  dvexp3  23977  plyeq0lem  24202  dgrcolem1  24265  aaliou3lem2  24334  aaliou3lem7  24340  pserdv2  24420  abelthlem6  24426  logtayl  24642  logtaylsum  24643  logtayl2  24644  cxpexp  24650  cxproot  24672  root1id  24731  root1eq1  24732  cxpeq  24734  atantayl  24900  atantayl2  24901  birthdaylem2  24915  dfef2  24933  emcllem2  24959  emcllem3  24960  zetacvg  24977  lgam1  25026  gamfac  25029  basellem2  25044  basellem3  25045  basellem5  25047  basellem8  25050  mumul  25143  fsumdvdscom  25147  muinv  25155  chtublem  25172  perfect  25192  pcbcctr  25237  bclbnd  25241  bposlem1  25245  bposlem6  25250  lgssq2  25299  gausslemma2dlem1a  25326  gausslemma2dlem3  25329  2lgslem1a1  25350  2sqlem6  25384  2sqlem10  25389  rplogsumlem1  25409  dchrmusumlema  25418  dchrmusum2  25419  dchrvmasumiflem1  25426  dchrvmaeq0  25429  dchrisum0re  25438  logdivbnd  25481  cusgrsize2inds  26599  wlkdlem2  26830  crctcshwlkn0lem1  26953  crctcshwlkn0lem6  26958  0enwwlksnge1  27013  wspthsnonn0vne  27079  clwwlknwwlksn  27208  clwwlknwwlksnOLD  27209  clwwlkinwwlk  27211  clwwlkel  27217  clwwlkf  27218  clwwlkf1  27220  wwlksubclwwlk  27231  eucrctshift  27438  eucrct2eupth  27440  numclwwlk2lem1  27578  numclwlk2lem2f  27579  numclwlk2lem2f1o  27581  numclwwlk2lem1OLD  27585  numclwlk2lem2fOLD  27586  numclwlk2lem2f1oOLD  27588  ipasslem4  28039  ipasslem5  28040  isarchi3  30088  oddpwdc  30763  eulerpartlemb  30777  fibp1  30810  subfacp1lem6  31511  subfaclim  31514  snmlff  31655  circum  31911  divcnvlin  31961  bcprod  31967  iprodgam  31971  faclim  31975  faclim2  31977  nn0prpwlem  32659  nndivsub  32794  knoppndvlem13  32853  poimirlem13  33753  poimirlem14  33754  poimirlem29  33769  poimirlem30  33770  poimirlem31  33771  poimirlem32  33772  mblfinlem2  33778  ovoliunnfl  33782  voliunnfl  33784  irrapxlem1  37905  pellexlem1  37912  pellqrex  37962  2nn0ind  38028  jm2.17c  38047  acongrep  38065  jm2.18  38073  jm2.20nn  38082  jm2.16nn0  38089  proot1ex  38297  hashnzfzclim  39038  binomcxplemnotnn0  39072  nnsplit  40071  clim1fr1  40330  sumnnodd  40359  wallispilem4  40781  wallispilem5  40782  wallispi  40783  wallispi2lem1  40784  wallispi2lem2  40785  wallispi2  40786  stirlinglem1  40787  stirlinglem3  40789  stirlinglem4  40790  stirlinglem5  40791  stirlinglem6  40792  stirlinglem7  40793  stirlinglem8  40794  stirlinglem10  40796  stirlinglem11  40797  stirlinglem12  40798  stirlinglem13  40799  stirlinglem14  40800  stirlinglem15  40801  dirkerper  40809  dirkertrigeqlem1  40811  fouriersw  40944  nnfoctbdjlem  41168  deccarry  41913  subsubelfzo0  41928  sqrtpwpw2p  42042  fmtnodvds  42048  fmtnoprmfac1  42069  fmtnoprmfac2lem1  42070  fmtnoprmfac2  42071  pwdif  42093  lighneallem2  42115  lighneallem3  42116  lighneallem4  42119  perfectALTV  42224  tgoldbachlt  42296  nnsgrp  42402  nnsgrpnmnd  42403  bcpascm1  42714  altgsumbcALT  42716  eluz2cnn0n1  42886  pw2m1lepw2m1  42895  mod0mul  42899  m1modmmod  42901  logbpw2m1  42946  blenpw2m1  42958  nnpw2blen  42959  nnpw2pmod  42962  blennnt2  42968  blennn0em1  42970  nn0digval  42979  dignn0fr  42980  dignn0ldlem  42981  dig0  42985  nn0sumshdiglemA  42998  nn0sumshdiglemB  42999  nn0sumshdiglem1  43000
  Copyright terms: Public domain W3C validator