Theorem nncn 11990

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10878  ℕcn 11982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-1cn 10938  ax-addcl 10940

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-nn 11983

This theorem is referenced by:  nncni  11992  nn1m1nn  12003  nn1suc  12004  nnaddcl  12005  nnmulcl  12006  nnmtmip  12008  nnneneg  12017  nnsub  12026  nndiv  12028  nndivtr  12029  nnnn0addcl  12272  nn0nnaddcl  12273  elnnnn0  12285  nn0sub  12292  nnnegz  12331  elz2  12346  zaddcl  12369  nnaddm1cl  12386  zdiv  12399  zdivadd  12400  zdivmul  12401  nneo  12413  peano5uzi  12418  elq  12699  qmulz  12700  qaddcl  12714  qnegcl  12715  qmulcl  12716  qreccl  12718  rpnnen1lem5  12730  nnledivrp  12851  nn0ledivnn  12852  fseq1m1p1  13340  ubmelm1fzo  13492  subfzo0  13518  quoremz  13584  quoremnn0ALT  13586  intfracq  13588  fldiv  13589  fldiv2  13590  modmulnn  13618  addmodid  13648  addmodidr  13649  modaddmodup  13663  modfzo0difsn  13672  modsumfzodifsn  13673  addmodlteq  13675  nn0ennn  13708  ser1const  13788  expneg  13799  expm1t  13820  nnsqcl  13856  nnlesq  13931  digit2  13960  digit1  13961  expnngt1  13965  facdiv  14010  facndiv  14011  faclbnd  14013  faclbnd4lem1  14016  faclbnd4lem4  14019  bcn1  14036  bcm1k  14038  bcp1n  14039  bcval5  14041  bcn2m1  14047  cshwidxmod  14525  cshwidxm  14530  cshwidxn  14531  repswcshw  14534  isercoll2  15389  divcnv  15574  harmonic  15580  arisum  15581  arisum2  15582  expcnv  15585  pwdif  15589  geomulcvg  15597  mertenslem2  15606  ef0lem  15797  efexp  15819  ruclem12  15959  sqrt2irr  15967  nndivides  15982  modmulconst  16006  dvdsflip  16035  nn0enne  16095  nno  16100  pwp1fsum  16109  divalgmod  16124  ndvdsadd  16128  modgcd  16249  gcdmultiplez  16252  gcddiv  16268  gcdmultipleOLD  16269  gcdmultiplezOLD  16270  rpmulgcd  16275  rplpwr  16276  sqgcd  16279  lcmgcdlem  16320  qredeq  16371  qredeu  16372  cncongrcoprm  16384  prmind2  16399  isprm6  16428  divnumden  16461  divdenle  16462  nn0gcdsq  16465  hashgcdlem  16498  pythagtriplem1  16526  pythagtriplem2  16527  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem15  16539  pythagtriplem16  16540  pythagtriplem17  16541  pythagtriplem19  16543  pcqcl  16566  pcexp  16569  pcneg  16584  fldivp1  16607  oddprmdvds  16613  prmpwdvds  16614  infpnlem2  16621  prmreclem1  16626  prmreclem6  16631  4sqlem19  16673  vdwapun  16684  vdwapid1  16685  prmonn2  16749  prmgaplem7  16767  mulgnegnn  18723  mulgnnass  18747  mulgmodid  18751  odmod  19163  cnfldmulg  20639  prmirredlem  20703  znidomb  20778  znrrg  20782  cply1mul  21474  chfacfscmul0  22016  chfacfscmulfsupp  22017  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulfsupp  22021  chfacfpmmulgsum  22022  cayhamlem1  22024  cpmadugsumlemF  22034  ovolunlem1  24670  uniioombllem3  24758  vitali  24786  mbfi1fseqlem3  24891  dvexp  25126  dvexp3  25151  plyeq0lem  25380  dgrcolem1  25443  aaliou3lem2  25512  aaliou3lem7  25518  pserdv2  25598  abelthlem6  25604  logtayl  25824  logtaylsum  25825  logtayl2  25826  cxpexp  25832  cxproot  25854  root1id  25916  root1eq1  25917  cxpeq  25919  logbgcd1irr  25953  atantayl  26096  atantayl2  26097  birthdaylem2  26111  dfef2  26129  emcllem2  26155  emcllem3  26156  zetacvg  26173  lgam1  26222  gamfac  26225  basellem2  26240  basellem3  26241  basellem5  26243  basellem8  26246  mumul  26339  fsumdvdscom  26343  muinv  26351  chtublem  26368  perfect  26388  pcbcctr  26433  bclbnd  26437  bposlem1  26441  bposlem6  26446  lgssq2  26495  gausslemma2dlem1a  26522  gausslemma2dlem3  26525  2lgslem1a1  26546  2sqlem6  26580  2sqlem10  26585  2sqnn  26596  2sqreunnltlem  26607  rplogsumlem1  26641  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumiflem1  26658  dchrvmaeq0  26661  dchrisum0re  26670  logdivbnd  26713  cusgrsize2inds  27829  wlkdlem2  28060  crctcshwlkn0lem1  28184  crctcshwlkn0lem6  28189  0enwwlksnge1  28238  wspthsnonn0vne  28291  clwwlknwwlksn  28411  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf  28420  clwwlkf1  28422  wwlksubclwwlk  28431  eucrctshift  28616  eucrct2eupth  28618  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  ipasslem4  29205  ipasslem5  29206  isarchi3  31450  oddpwdc  32330  eulerpartlemb  32344  fibp1  32377  subfacp1lem6  33156  subfaclim  33159  snmlff  33300  circum  33641  divcnvlin  33707  bcprod  33713  iprodgam  33717  faclim  33721  faclim2  33723  nn0prpwlem  34520  nndivsub  34655  knoppndvlem13  34713  poimirlem13  35799  poimirlem14  35800  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  facp2  40106  metakunt16  40147  metakunt30  40161  fac2xp3  40167  nnadd1com  40304  nnaddcom  40305  expgcd  40341  nn0expgcd  40342  dvdsexpnn0  40348  dffltz  40478  irrapxlem1  40651  pellexlem1  40658  pellqrex  40708  2nn0ind  40774  jm2.17c  40791  acongrep  40809  jm2.18  40817  jm2.20nn  40826  jm2.16nn0  40833  proot1ex  41033  hashnzfzclim  41947  binomcxplemnotnn0  41981  nnsplit  42904  clim1fr1  43149  sumnnodd  43178  wallispilem4  43616  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  dirkerper  43644  dirkertrigeqlem1  43646  fouriersw  43779  nnfoctbdjlem  44000  deccarry  44814  subsubelfzo0  44829  sqrtpwpw2p  45001  fmtnodvds  45007  fmtnoprmfac1  45028  fmtnoprmfac2lem1  45029  fmtnoprmfac2  45030  lighneallem2  45069  lighneallem3  45070  lighneallem4  45073  nnennexALTV  45164  perfectALTV  45186  fppr2odd  45194  fpprwppr  45202  fpprwpprb  45203  tgoldbachlt  45279  nnsgrp  45382  nnsgrpnmnd  45383  bcpascm1  45698  altgsumbcALT  45700  eluz2cnn0n1  45863  pw2m1lepw2m1  45872  mod0mul  45876  m1modmmod  45878  nnennex  45882  logbpw2m1  45924  blenpw2m1  45936  nnpw2blen  45937  nnpw2pmod  45940  blennnt2  45946  blennn0em1  45948  nn0digval  45957  dignn0fr  45958  dignn0ldlem  45959  dig0  45963  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978