Theorem nncn 11682

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 10573  ℕcn 11674

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459  ax-1cn 10633  ax-addcl 10635

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-ov 7153  df-om 7580  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-nn 11675

This theorem is referenced by:  nncni  11684  nn1m1nn  11695  nn1suc  11696  nnaddcl  11697  nnmulcl  11698  nnmtmip  11700  nnneneg  11709  nnsub  11718  nndiv  11720  nndivtr  11721  nnnn0addcl  11964  nn0nnaddcl  11965  elnnnn0  11977  nn0sub  11984  nnnegz  12023  elz2  12038  zaddcl  12061  nnaddm1cl  12078  zdiv  12091  zdivadd  12092  zdivmul  12093  nneo  12105  peano5uzi  12110  elq  12390  qmulz  12391  qaddcl  12405  qnegcl  12406  qmulcl  12407  qreccl  12409  rpnnen1lem5  12421  nnledivrp  12542  nn0ledivnn  12543  fseq1m1p1  13031  ubmelm1fzo  13182  subfzo0  13208  quoremz  13272  quoremnn0ALT  13274  intfracq  13276  fldiv  13277  fldiv2  13278  modmulnn  13306  addmodid  13336  addmodidr  13337  modaddmodup  13351  modfzo0difsn  13360  modsumfzodifsn  13361  addmodlteq  13363  nn0ennn  13396  ser1const  13476  expneg  13487  expm1t  13507  nnsqcl  13543  nnlesq  13618  digit2  13647  digit1  13648  expnngt1  13652  facdiv  13697  facndiv  13698  faclbnd  13700  faclbnd4lem1  13703  faclbnd4lem4  13706  bcn1  13723  bcm1k  13725  bcp1n  13726  bcval5  13728  bcn2m1  13734  cshwidxmod  14212  cshwidxm  14217  cshwidxn  14218  repswcshw  14221  isercoll2  15073  divcnv  15256  harmonic  15262  arisum  15263  arisum2  15264  expcnv  15267  pwdif  15271  geomulcvg  15280  mertenslem2  15289  ef0lem  15480  efexp  15502  ruclem12  15642  sqrt2irr  15650  nndivides  15665  modmulconst  15689  dvdsflip  15718  nn0enne  15778  nno  15783  pwp1fsum  15792  divalgmod  15807  ndvdsadd  15811  modgcd  15931  gcdmultiplez  15934  gcddiv  15950  gcdmultipleOLD  15951  gcdmultiplezOLD  15952  rpmulgcd  15957  rplpwr  15958  sqgcd  15961  lcmgcdlem  16002  qredeq  16053  qredeu  16054  cncongrcoprm  16066  prmind2  16081  isprm6  16110  divnumden  16143  divdenle  16144  nn0gcdsq  16147  hashgcdlem  16180  pythagtriplem1  16208  pythagtriplem2  16209  pythagtriplem6  16213  pythagtriplem7  16214  pythagtriplem12  16218  pythagtriplem14  16220  pythagtriplem15  16221  pythagtriplem16  16222  pythagtriplem17  16223  pythagtriplem19  16225  pcqcl  16248  pcexp  16251  pcneg  16265  fldivp1  16288  oddprmdvds  16294  prmpwdvds  16295  infpnlem2  16302  prmreclem1  16307  prmreclem6  16312  4sqlem19  16354  vdwapun  16365  vdwapid1  16366  prmonn2  16430  prmgaplem7  16448  mulgnegnn  18305  mulgnnass  18329  mulgmodid  18333  odmod  18741  cnfldmulg  20198  prmirredlem  20262  znidomb  20329  znrrg  20333  cply1mul  21018  chfacfscmul0  21558  chfacfscmulfsupp  21559  chfacfscmulgsum  21560  chfacfpmmul0  21562  chfacfpmmulfsupp  21563  chfacfpmmulgsum  21564  cayhamlem1  21566  cpmadugsumlemF  21576  ovolunlem1  24197  uniioombllem3  24285  vitali  24313  mbfi1fseqlem3  24417  dvexp  24652  dvexp3  24677  plyeq0lem  24906  dgrcolem1  24969  aaliou3lem2  25038  aaliou3lem7  25044  pserdv2  25124  abelthlem6  25130  logtayl  25350  logtaylsum  25351  logtayl2  25352  cxpexp  25358  cxproot  25380  root1id  25442  root1eq1  25443  cxpeq  25445  logbgcd1irr  25479  atantayl  25622  atantayl2  25623  birthdaylem2  25637  dfef2  25655  emcllem2  25681  emcllem3  25682  zetacvg  25699  lgam1  25748  gamfac  25751  basellem2  25766  basellem3  25767  basellem5  25769  basellem8  25772  mumul  25865  fsumdvdscom  25869  muinv  25877  chtublem  25894  perfect  25914  pcbcctr  25959  bclbnd  25963  bposlem1  25967  bposlem6  25972  lgssq2  26021  gausslemma2dlem1a  26048  gausslemma2dlem3  26051  2lgslem1a1  26072  2sqlem6  26106  2sqlem10  26111  2sqnn  26122  2sqreunnltlem  26133  rplogsumlem1  26167  dchrmusumlema  26176  dchrmusum2  26177  dchrvmasumiflem1  26184  dchrvmaeq0  26187  dchrisum0re  26196  logdivbnd  26239  cusgrsize2inds  27342  wlkdlem2  27572  crctcshwlkn0lem1  27695  crctcshwlkn0lem6  27700  0enwwlksnge1  27749  wspthsnonn0vne  27802  clwwlknwwlksn  27922  clwwlkinwwlk  27924  clwwlkel  27930  clwwlkf  27931  clwwlkf1  27933  wwlksubclwwlk  27942  eucrctshift  28127  eucrct2eupth  28129  numclwwlk2lem1  28260  numclwlk2lem2f  28261  numclwlk2lem2f1o  28263  ipasslem4  28716  ipasslem5  28717  isarchi3  30967  oddpwdc  31840  eulerpartlemb  31854  fibp1  31887  subfacp1lem6  32663  subfaclim  32666  snmlff  32807  circum  33148  divcnvlin  33213  bcprod  33219  iprodgam  33223  faclim  33227  faclim2  33229  nn0prpwlem  34060  nndivsub  34195  knoppndvlem13  34253  poimirlem13  35350  poimirlem14  35351  poimirlem29  35366  poimirlem30  35367  poimirlem31  35368  poimirlem32  35369  mblfinlem2  35375  ovoliunnfl  35379  voliunnfl  35381  facp2  39644  metakunt16  39662  metakunt30  39676  fac2xp3  39682  nnadd1com  39799  nnaddcom  39800  expgcd  39831  nn0expgcd  39832  dffltz  39963  irrapxlem1  40136  pellexlem1  40143  pellqrex  40193  2nn0ind  40259  jm2.17c  40276  acongrep  40294  jm2.18  40302  jm2.20nn  40311  jm2.16nn0  40318  proot1ex  40518  hashnzfzclim  41399  binomcxplemnotnn0  41433  nnsplit  42358  clim1fr1  42609  sumnnodd  42638  wallispilem4  43076  wallispilem5  43077  wallispi  43078  wallispi2lem1  43079  wallispi2lem2  43080  wallispi2  43081  stirlinglem1  43082  stirlinglem3  43084  stirlinglem4  43085  stirlinglem5  43086  stirlinglem6  43087  stirlinglem7  43088  stirlinglem8  43089  stirlinglem10  43091  stirlinglem11  43092  stirlinglem12  43093  stirlinglem13  43094  stirlinglem14  43095  stirlinglem15  43096  dirkerper  43104  dirkertrigeqlem1  43106  fouriersw  43239  nnfoctbdjlem  43460  deccarry  44236  subsubelfzo0  44251  sqrtpwpw2p  44423  fmtnodvds  44429  fmtnoprmfac1  44450  fmtnoprmfac2lem1  44451  fmtnoprmfac2  44452  lighneallem2  44491  lighneallem3  44492  lighneallem4  44495  nnennexALTV  44586  perfectALTV  44608  fppr2odd  44616  fpprwppr  44624  fpprwpprb  44625  tgoldbachlt  44701  nnsgrp  44804  nnsgrpnmnd  44805  bcpascm1  45120  altgsumbcALT  45122  eluz2cnn0n1  45285  pw2m1lepw2m1  45294  mod0mul  45298  m1modmmod  45300  nnennex  45304  logbpw2m1  45346  blenpw2m1  45358  nnpw2blen  45359  nnpw2pmod  45362  blennnt2  45368  blennn0em1  45370  nn0digval  45379  dignn0fr  45380  dignn0ldlem  45381  dig0  45385  nn0sumshdiglemA  45398  nn0sumshdiglemB  45399  nn0sumshdiglem1  45400