Theorem nncn 12125

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10996  ℕcn 12117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-1cn 11056  ax-addcl 11058

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-nn 12118

This theorem is referenced by:  nncni  12127  nn1m1nn  12138  nn1suc  12139  nnaddcl  12140  nnmulcl  12141  nnmtmip  12143  nnneneg  12152  nnsub  12161  nndiv  12163  nndivtr  12164  nnnn0addcl  12403  nn0nnaddcl  12404  elnnnn0  12416  nn0sub  12423  nnnegz  12463  elz2  12478  zaddcl  12504  nnaddm1cl  12522  zdiv  12535  zdivadd  12536  zdivmul  12537  nneo  12549  peano5uzi  12554  elq  12840  qmulz  12841  qaddcl  12855  qnegcl  12856  qmulcl  12857  qreccl  12859  rpnnen1lem5  12871  nnledivrp  12996  nn0ledivnn  12997  fseq1m1p1  13491  ubmelm1fzo  13655  subfzo0  13684  quoremz  13751  quoremnn0ALT  13753  intfracq  13755  fldiv  13756  fldiv2  13757  modmulnn  13785  addmodid  13818  addmodidr  13819  modaddmodup  13833  modfzo0difsn  13842  modsumfzodifsn  13843  addmodlteq  13845  nn0ennn  13878  ser1const  13957  expneg  13968  expm1t  13989  nnsqcl  14027  nnlesq  14104  digit2  14135  digit1  14136  expnngt1  14140  facdiv  14186  facndiv  14187  faclbnd  14189  faclbnd4lem1  14192  faclbnd4lem4  14195  bcn1  14212  bcm1k  14214  bcp1n  14215  bcval5  14217  bcn2m1  14223  cshwidxmod  14702  cshwidxm  14707  cshwidxn  14708  repswcshw  14711  isercoll2  15568  divcnv  15752  harmonic  15758  arisum  15759  arisum2  15760  expcnv  15763  pwdif  15767  geomulcvg  15775  mertenslem2  15784  ef0lem  15977  efexp  16002  ruclem12  16142  sqrt2irr  16150  nndivides  16165  modmulconst  16191  dvdsflip  16220  nn0enne  16280  nno  16285  pwp1fsum  16294  divalgmod  16309  ndvdsadd  16313  modgcd  16435  gcdmultiplez  16438  gcddiv  16454  rpmulgcd  16460  rplpwr  16461  sqgcd  16465  expgcd  16466  nn0expgcd  16467  lcmgcdlem  16509  qredeq  16560  qredeu  16561  cncongrcoprm  16573  prmind2  16588  isprm6  16617  divnumden  16651  divdenle  16652  nn0gcdsq  16655  hashgcdlem  16691  pythagtriplem1  16720  pythagtriplem2  16721  pythagtriplem6  16725  pythagtriplem7  16726  pythagtriplem12  16730  pythagtriplem14  16732  pythagtriplem15  16733  pythagtriplem16  16734  pythagtriplem17  16735  pythagtriplem19  16737  pcqcl  16760  pcexp  16763  pcneg  16778  fldivp1  16801  oddprmdvds  16807  prmpwdvds  16808  infpnlem2  16815  prmreclem1  16820  prmreclem6  16825  4sqlem19  16867  vdwapun  16878  vdwapid1  16879  prmonn2  16943  prmgaplem7  16961  mulgnegnn  18989  mulgnnass  19014  mulgmodid  19018  odmod  19451  cnfldmulg  21333  prmirredlem  21402  znidomb  21491  znrrg  21495  cply1mul  22204  chfacfscmul0  22766  chfacfscmulfsupp  22767  chfacfscmulgsum  22768  chfacfpmmul0  22770  chfacfpmmulfsupp  22771  chfacfpmmulgsum  22772  cayhamlem1  22774  cpmadugsumlemF  22784  ovolunlem1  25418  uniioombllem3  25506  vitali  25534  mbfi1fseqlem3  25638  dvexp  25877  dvexp3  25902  plyeq0lem  26135  dgrcolem1  26199  aaliou3lem2  26271  aaliou3lem7  26277  pserdv2  26360  abelthlem6  26366  logtayl  26589  logtaylsum  26590  logtayl2  26591  cxpexp  26597  cxproot  26619  root1id  26684  root1eq1  26685  cxpeq  26687  logbgcd1irr  26724  atantayl  26867  atantayl2  26868  birthdaylem2  26882  dfef2  26901  emcllem2  26927  emcllem3  26928  zetacvg  26945  lgam1  26994  gamfac  26997  basellem2  27012  basellem3  27013  basellem5  27015  basellem8  27018  mumul  27111  fsumdvdscom  27115  muinv  27123  chtublem  27142  perfect  27162  pcbcctr  27207  bclbnd  27211  bposlem1  27215  bposlem6  27220  lgssq2  27269  gausslemma2dlem1a  27296  gausslemma2dlem3  27299  2lgslem1a1  27320  2sqlem6  27354  2sqlem10  27359  2sqnn  27370  2sqreunnltlem  27381  rplogsumlem1  27415  dchrmusumlema  27424  dchrmusum2  27425  dchrvmasumiflem1  27432  dchrvmaeq0  27435  dchrisum0re  27444  logdivbnd  27487  cusgrsize2inds  29425  wlkdlem2  29653  crctcshwlkn0lem1  29781  crctcshwlkn0lem6  29786  0enwwlksnge1  29835  wspthsnonn0vne  29888  clwwlknwwlksn  30008  clwwlkinwwlk  30010  clwwlkel  30016  clwwlkf  30017  clwwlkf1  30019  wwlksubclwwlk  30028  eucrctshift  30213  eucrct2eupth  30215  numclwwlk2lem1  30346  numclwlk2lem2f  30347  numclwlk2lem2f1o  30349  ipasslem4  30804  ipasslem5  30805  isarchi3  33146  oddpwdc  34357  eulerpartlemb  34371  fibp1  34404  subfacp1lem6  35197  subfaclim  35200  snmlff  35341  circum  35686  divcnvlin  35745  bcprod  35750  iprodgam  35754  faclim  35758  faclim2  35760  nn0prpwlem  36335  nndivsub  36470  knoppndvlem13  36537  poimirlem13  37652  poimirlem14  37653  poimirlem29  37668  poimirlem30  37669  poimirlem31  37670  poimirlem32  37671  mblfinlem2  37677  ovoliunnfl  37681  voliunnfl  37683  facp2  42155  nnadd1com  42279  nnaddcom  42280  dvdsexpnn0  42346  renegmulnnass  42477  fimgmcyc  42546  dffltz  42646  irrapxlem1  42834  pellexlem1  42841  pellqrex  42891  2nn0ind  42957  jm2.17c  42974  acongrep  42992  jm2.18  43000  jm2.20nn  43009  jm2.16nn0  43016  proot1ex  43208  hashnzfzclim  44334  binomcxplemnotnn0  44368  nnsplit  45376  clim1fr1  45620  sumnnodd  45649  wallispilem4  46085  wallispilem5  46086  wallispi  46087  wallispi2lem1  46088  wallispi2lem2  46089  wallispi2  46090  stirlinglem1  46091  stirlinglem3  46093  stirlinglem4  46094  stirlinglem5  46095  stirlinglem6  46096  stirlinglem7  46097  stirlinglem8  46098  stirlinglem10  46100  stirlinglem11  46101  stirlinglem12  46102  stirlinglem13  46103  stirlinglem14  46104  stirlinglem15  46105  dirkerper  46113  dirkertrigeqlem1  46115  fouriersw  46248  nnfoctbdjlem  46472  deccarry  47321  subsubelfzo0  47336  submodlt  47360  mod0mul  47366  m1modmmod  47368  modlt0b  47373  sqrtpwpw2p  47548  fmtnodvds  47554  fmtnoprmfac1  47575  fmtnoprmfac2lem1  47576  fmtnoprmfac2  47577  lighneallem2  47616  lighneallem3  47617  lighneallem4  47620  nnennexALTV  47711  perfectALTV  47733  fppr2odd  47741  fpprwppr  47749  fpprwpprb  47750  tgoldbachlt  47826  gpgedgvtx0  48071  gpg3kgrtriexlem2  48094  gpg3kgrtriexlem5  48097  gpg3kgrtriex  48099  nnsgrp  48187  nnsgrpnmnd  48188  bcpascm1  48361  altgsumbcALT  48363  eluz2cnn0n1  48522  pw2m1lepw2m1  48531  nnennex  48536  logbpw2m1  48578  blenpw2m1  48590  nnpw2blen  48591  nnpw2pmod  48594  blennnt2  48600  blennn0em1  48602  nn0digval  48611  dignn0fr  48612  dignn0ldlem  48613  dig0  48617  nn0sumshdiglemA  48630  nn0sumshdiglemB  48631  nn0sumshdiglem1  48632