Theorem nncn 12173

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11027  ℕcn 12165

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166

This theorem is referenced by:  nncni  12175  nn1m1nn  12186  nn1suc  12187  nnaddcl  12188  nnmulcl  12189  nnadd1com  12191  nnaddcom  12192  nnmtmip  12194  nnneneg  12203  nnsub  12212  nndiv  12214  nndivtr  12215  nnnn0addcl  12458  nn0nnaddcl  12459  elnnnn0  12471  nn0sub  12478  nnnegz  12518  elz2  12533  zaddcl  12558  nnaddm1cl  12577  zdiv  12590  zdivadd  12591  zdivmul  12592  nneo  12604  peano5uzi  12609  elq  12891  qmulz  12892  qaddcl  12906  qnegcl  12907  qmulcl  12908  qreccl  12910  rpnnen1lem5  12922  nnledivrp  13047  nn0ledivnn  13048  fseq1m1p1  13544  ubmelm1fzo  13709  subfzo0  13738  quoremz  13805  quoremnn0ALT  13807  intfracq  13809  fldiv  13810  fldiv2  13811  modmulnn  13839  addmodid  13872  addmodidr  13873  modaddmodup  13887  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  nn0ennn  13932  ser1const  14011  expneg  14022  expm1t  14043  nnsqcl  14081  nnlesq  14158  digit2  14189  digit1  14190  expnngt1  14194  facdiv  14240  facndiv  14241  faclbnd  14243  faclbnd4lem1  14246  faclbnd4lem4  14249  bcn1  14266  bcm1k  14268  bcp1n  14269  bcval5  14271  bcn2m1  14277  cshwidxmod  14756  cshwidxm  14761  cshwidxn  14762  repswcshw  14765  isercoll2  15622  divcnv  15809  harmonic  15815  arisum  15816  arisum2  15817  expcnv  15820  pwdif  15824  geomulcvg  15832  mertenslem2  15841  ef0lem  16034  efexp  16059  ruclem12  16199  sqrt2irr  16207  nndivides  16222  modmulconst  16248  dvdsflip  16277  nn0enne  16337  nno  16342  pwp1fsum  16351  divalgmod  16366  ndvdsadd  16370  modgcd  16492  gcdmultiplez  16495  gcddiv  16511  rpmulgcd  16517  rplpwr  16518  sqgcd  16522  expgcd  16523  nn0expgcd  16524  lcmgcdlem  16566  qredeq  16617  qredeu  16618  cncongrcoprm  16630  prmind2  16645  isprm6  16675  divnumden  16709  divdenle  16710  nn0gcdsq  16713  hashgcdlem  16749  pythagtriplem1  16778  pythagtriplem2  16779  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem15  16791  pythagtriplem16  16792  pythagtriplem17  16793  pythagtriplem19  16795  pcqcl  16818  pcexp  16821  pcneg  16836  fldivp1  16859  oddprmdvds  16865  prmpwdvds  16866  infpnlem2  16873  prmreclem1  16878  prmreclem6  16883  4sqlem19  16925  vdwapun  16936  vdwapid1  16937  prmonn2  17001  prmgaplem7  17019  mulgnegnn  19051  mulgnnass  19076  mulgmodid  19080  odmod  19512  cnfldmulg  21393  prmirredlem  21462  znidomb  21551  znrrg  21555  cply1mul  22271  chfacfscmul0  22833  chfacfscmulfsupp  22834  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulfsupp  22838  chfacfpmmulgsum  22839  cayhamlem1  22841  cpmadugsumlemF  22851  ovolunlem1  25474  uniioombllem3  25562  vitali  25590  mbfi1fseqlem3  25694  dvexp  25930  dvexp3  25955  plyeq0lem  26185  dgrcolem1  26248  aaliou3lem2  26320  aaliou3lem7  26326  pserdv2  26408  abelthlem6  26414  logtayl  26637  logtaylsum  26638  logtayl2  26639  cxpexp  26645  cxproot  26667  root1id  26731  root1eq1  26732  cxpeq  26734  logbgcd1irr  26771  atantayl  26914  atantayl2  26915  birthdaylem2  26929  dfef2  26948  emcllem2  26974  emcllem3  26975  zetacvg  26992  lgam1  27041  gamfac  27044  basellem2  27059  basellem3  27060  basellem5  27062  basellem8  27065  mumul  27158  fsumdvdscom  27162  muinv  27170  chtublem  27188  perfect  27208  pcbcctr  27253  bclbnd  27257  bposlem1  27261  bposlem6  27266  lgssq2  27315  gausslemma2dlem1a  27342  gausslemma2dlem3  27345  2lgslem1a1  27366  2sqlem6  27400  2sqlem10  27405  2sqnn  27416  2sqreunnltlem  27427  rplogsumlem1  27461  dchrmusumlema  27470  dchrmusum2  27471  dchrvmasumiflem1  27478  dchrvmaeq0  27481  dchrisum0re  27490  logdivbnd  27533  cusgrsize2inds  29537  wlkdlem2  29765  crctcshwlkn0lem1  29893  crctcshwlkn0lem6  29898  0enwwlksnge1  29947  wspthsnonn0vne  30000  clwwlknwwlksn  30123  clwwlkinwwlk  30125  clwwlkel  30131  clwwlkf  30132  clwwlkf1  30134  wwlksubclwwlk  30143  eucrctshift  30328  eucrct2eupth  30330  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  ipasslem4  30920  ipasslem5  30921  isarchi3  33263  oddpwdc  34514  eulerpartlemb  34528  fibp1  34561  subfacp1lem6  35383  subfaclim  35386  snmlff  35527  circum  35872  divcnvlin  35931  bcprod  35936  iprodgam  35940  faclim  35944  faclim2  35946  nn0prpwlem  36520  nndivsub  36655  knoppndvlem13  36800  poimirlem13  37968  poimirlem14  37969  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  mblfinlem2  37993  ovoliunnfl  37997  voliunnfl  37999  facp2  42596  dvdsexpnn0  42780  renegmulnnass  42924  fimgmcyc  42993  dffltz  43081  irrapxlem1  43268  pellexlem1  43275  pellqrex  43325  2nn0ind  43391  jm2.17c  43408  acongrep  43426  jm2.18  43434  jm2.20nn  43443  jm2.16nn0  43450  proot1ex  43642  hashnzfzclim  44767  binomcxplemnotnn0  44801  nnsplit  45806  clim1fr1  46049  sumnnodd  46078  wallispilem4  46514  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem6  46525  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  stirlinglem14  46533  stirlinglem15  46534  dirkerper  46542  dirkertrigeqlem1  46544  fouriersw  46677  nnfoctbdjlem  46901  deccarry  47771  subsubelfzo0  47787  submodlt  47816  mod0mul  47822  m1modmmod  47824  modlt0b  47829  sqrtpwpw2p  48013  fmtnodvds  48019  fmtnoprmfac1  48040  fmtnoprmfac2lem1  48041  fmtnoprmfac2  48042  lighneallem2  48081  lighneallem3  48082  lighneallem4  48085  nnennexALTV  48189  perfectALTV  48211  fppr2odd  48219  fpprwppr  48227  fpprwpprb  48228  tgoldbachlt  48304  gpgedgvtx0  48549  gpg3kgrtriexlem2  48572  gpg3kgrtriexlem5  48575  gpg3kgrtriex  48577  nnsgrp  48665  nnsgrpnmnd  48666  bcpascm1  48839  altgsumbcALT  48841  eluz2cnn0n1  48999  pw2m1lepw2m1  49008  nnennex  49013  logbpw2m1  49055  blenpw2m1  49067  nnpw2blen  49068  nnpw2pmod  49071  blennnt2  49077  blennn0em1  49079  nn0digval  49088  dignn0fr  49089  dignn0ldlem  49090  dig0  49094  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  nn0sumshdiglem1  49109