Theorem nncn 11911

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℕcn 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904

This theorem is referenced by:  nncni  11913  nn1m1nn  11924  nn1suc  11925  nnaddcl  11926  nnmulcl  11927  nnmtmip  11929  nnneneg  11938  nnsub  11947  nndiv  11949  nndivtr  11950  nnnn0addcl  12193  nn0nnaddcl  12194  elnnnn0  12206  nn0sub  12213  nnnegz  12252  elz2  12267  zaddcl  12290  nnaddm1cl  12307  zdiv  12320  zdivadd  12321  zdivmul  12322  nneo  12334  peano5uzi  12339  elq  12619  qmulz  12620  qaddcl  12634  qnegcl  12635  qmulcl  12636  qreccl  12638  rpnnen1lem5  12650  nnledivrp  12771  nn0ledivnn  12772  fseq1m1p1  13260  ubmelm1fzo  13411  subfzo0  13437  quoremz  13503  quoremnn0ALT  13505  intfracq  13507  fldiv  13508  fldiv2  13509  modmulnn  13537  addmodid  13567  addmodidr  13568  modaddmodup  13582  modfzo0difsn  13591  modsumfzodifsn  13592  addmodlteq  13594  nn0ennn  13627  ser1const  13707  expneg  13718  expm1t  13739  nnsqcl  13775  nnlesq  13850  digit2  13879  digit1  13880  expnngt1  13884  facdiv  13929  facndiv  13930  faclbnd  13932  faclbnd4lem1  13935  faclbnd4lem4  13938  bcn1  13955  bcm1k  13957  bcp1n  13958  bcval5  13960  bcn2m1  13966  cshwidxmod  14444  cshwidxm  14449  cshwidxn  14450  repswcshw  14453  isercoll2  15308  divcnv  15493  harmonic  15499  arisum  15500  arisum2  15501  expcnv  15504  pwdif  15508  geomulcvg  15516  mertenslem2  15525  ef0lem  15716  efexp  15738  ruclem12  15878  sqrt2irr  15886  nndivides  15901  modmulconst  15925  dvdsflip  15954  nn0enne  16014  nno  16019  pwp1fsum  16028  divalgmod  16043  ndvdsadd  16047  modgcd  16168  gcdmultiplez  16171  gcddiv  16187  gcdmultipleOLD  16188  gcdmultiplezOLD  16189  rpmulgcd  16194  rplpwr  16195  sqgcd  16198  lcmgcdlem  16239  qredeq  16290  qredeu  16291  cncongrcoprm  16303  prmind2  16318  isprm6  16347  divnumden  16380  divdenle  16381  nn0gcdsq  16384  hashgcdlem  16417  pythagtriplem1  16445  pythagtriplem2  16446  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem15  16458  pythagtriplem16  16459  pythagtriplem17  16460  pythagtriplem19  16462  pcqcl  16485  pcexp  16488  pcneg  16503  fldivp1  16526  oddprmdvds  16532  prmpwdvds  16533  infpnlem2  16540  prmreclem1  16545  prmreclem6  16550  4sqlem19  16592  vdwapun  16603  vdwapid1  16604  prmonn2  16668  prmgaplem7  16686  mulgnegnn  18629  mulgnnass  18653  mulgmodid  18657  odmod  19069  cnfldmulg  20542  prmirredlem  20606  znidomb  20681  znrrg  20685  cply1mul  21375  chfacfscmul0  21915  chfacfscmulfsupp  21916  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulfsupp  21920  chfacfpmmulgsum  21921  cayhamlem1  21923  cpmadugsumlemF  21933  ovolunlem1  24566  uniioombllem3  24654  vitali  24682  mbfi1fseqlem3  24787  dvexp  25022  dvexp3  25047  plyeq0lem  25276  dgrcolem1  25339  aaliou3lem2  25408  aaliou3lem7  25414  pserdv2  25494  abelthlem6  25500  logtayl  25720  logtaylsum  25721  logtayl2  25722  cxpexp  25728  cxproot  25750  root1id  25812  root1eq1  25813  cxpeq  25815  logbgcd1irr  25849  atantayl  25992  atantayl2  25993  birthdaylem2  26007  dfef2  26025  emcllem2  26051  emcllem3  26052  zetacvg  26069  lgam1  26118  gamfac  26121  basellem2  26136  basellem3  26137  basellem5  26139  basellem8  26142  mumul  26235  fsumdvdscom  26239  muinv  26247  chtublem  26264  perfect  26284  pcbcctr  26329  bclbnd  26333  bposlem1  26337  bposlem6  26342  lgssq2  26391  gausslemma2dlem1a  26418  gausslemma2dlem3  26421  2lgslem1a1  26442  2sqlem6  26476  2sqlem10  26481  2sqnn  26492  2sqreunnltlem  26503  rplogsumlem1  26537  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumiflem1  26554  dchrvmaeq0  26557  dchrisum0re  26566  logdivbnd  26609  cusgrsize2inds  27723  wlkdlem2  27953  crctcshwlkn0lem1  28076  crctcshwlkn0lem6  28081  0enwwlksnge1  28130  wspthsnonn0vne  28183  clwwlknwwlksn  28303  clwwlkinwwlk  28305  clwwlkel  28311  clwwlkf  28312  clwwlkf1  28314  wwlksubclwwlk  28323  eucrctshift  28508  eucrct2eupth  28510  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  ipasslem4  29097  ipasslem5  29098  isarchi3  31343  oddpwdc  32221  eulerpartlemb  32235  fibp1  32268  subfacp1lem6  33047  subfaclim  33050  snmlff  33191  circum  33532  divcnvlin  33604  bcprod  33610  iprodgam  33614  faclim  33618  faclim2  33620  nn0prpwlem  34438  nndivsub  34573  knoppndvlem13  34631  poimirlem13  35717  poimirlem14  35718  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  facp2  40027  metakunt16  40068  metakunt30  40082  fac2xp3  40088  nnadd1com  40218  nnaddcom  40219  expgcd  40255  nn0expgcd  40256  dvdsexpnn0  40262  dffltz  40387  irrapxlem1  40560  pellexlem1  40567  pellqrex  40617  2nn0ind  40683  jm2.17c  40700  acongrep  40718  jm2.18  40726  jm2.20nn  40735  jm2.16nn0  40742  proot1ex  40942  hashnzfzclim  41829  binomcxplemnotnn0  41863  nnsplit  42787  clim1fr1  43032  sumnnodd  43061  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  dirkerper  43527  dirkertrigeqlem1  43529  fouriersw  43662  nnfoctbdjlem  43883  deccarry  44691  subsubelfzo0  44706  sqrtpwpw2p  44878  fmtnodvds  44884  fmtnoprmfac1  44905  fmtnoprmfac2lem1  44906  fmtnoprmfac2  44907  lighneallem2  44946  lighneallem3  44947  lighneallem4  44950  nnennexALTV  45041  perfectALTV  45063  fppr2odd  45071  fpprwppr  45079  fpprwpprb  45080  tgoldbachlt  45156  nnsgrp  45259  nnsgrpnmnd  45260  bcpascm1  45575  altgsumbcALT  45577  eluz2cnn0n1  45740  pw2m1lepw2m1  45749  mod0mul  45753  m1modmmod  45755  nnennex  45759  logbpw2m1  45801  blenpw2m1  45813  nnpw2blen  45814  nnpw2pmod  45817  blennnt2  45823  blennn0em1  45825  nn0digval  45834  dignn0fr  45835  dignn0ldlem  45836  dig0  45840  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855