Theorem nncn 12194

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℕcn 12186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187

This theorem is referenced by:  nncni  12196  nn1m1nn  12207  nn1suc  12208  nnaddcl  12209  nnmulcl  12210  nnmtmip  12212  nnneneg  12221  nnsub  12230  nndiv  12232  nndivtr  12233  nnnn0addcl  12472  nn0nnaddcl  12473  elnnnn0  12485  nn0sub  12492  nnnegz  12532  elz2  12547  zaddcl  12573  nnaddm1cl  12591  zdiv  12604  zdivadd  12605  zdivmul  12606  nneo  12618  peano5uzi  12623  elq  12909  qmulz  12910  qaddcl  12924  qnegcl  12925  qmulcl  12926  qreccl  12928  rpnnen1lem5  12940  nnledivrp  13065  nn0ledivnn  13066  fseq1m1p1  13560  ubmelm1fzo  13724  subfzo0  13750  quoremz  13817  quoremnn0ALT  13819  intfracq  13821  fldiv  13822  fldiv2  13823  modmulnn  13851  addmodid  13884  addmodidr  13885  modaddmodup  13899  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  nn0ennn  13944  ser1const  14023  expneg  14034  expm1t  14055  nnsqcl  14093  nnlesq  14170  digit2  14201  digit1  14202  expnngt1  14206  facdiv  14252  facndiv  14253  faclbnd  14255  faclbnd4lem1  14258  faclbnd4lem4  14261  bcn1  14278  bcm1k  14280  bcp1n  14281  bcval5  14283  bcn2m1  14289  cshwidxmod  14768  cshwidxm  14773  cshwidxn  14774  repswcshw  14777  isercoll2  15635  divcnv  15819  harmonic  15825  arisum  15826  arisum2  15827  expcnv  15830  pwdif  15834  geomulcvg  15842  mertenslem2  15851  ef0lem  16044  efexp  16069  ruclem12  16209  sqrt2irr  16217  nndivides  16232  modmulconst  16258  dvdsflip  16287  nn0enne  16347  nno  16352  pwp1fsum  16361  divalgmod  16376  ndvdsadd  16380  modgcd  16502  gcdmultiplez  16505  gcddiv  16521  rpmulgcd  16527  rplpwr  16528  sqgcd  16532  expgcd  16533  nn0expgcd  16534  lcmgcdlem  16576  qredeq  16627  qredeu  16628  cncongrcoprm  16640  prmind2  16655  isprm6  16684  divnumden  16718  divdenle  16719  nn0gcdsq  16722  hashgcdlem  16758  pythagtriplem1  16787  pythagtriplem2  16788  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem16  16801  pythagtriplem17  16802  pythagtriplem19  16804  pcqcl  16827  pcexp  16830  pcneg  16845  fldivp1  16868  oddprmdvds  16874  prmpwdvds  16875  infpnlem2  16882  prmreclem1  16887  prmreclem6  16892  4sqlem19  16934  vdwapun  16945  vdwapid1  16946  prmonn2  17010  prmgaplem7  17028  mulgnegnn  19016  mulgnnass  19041  mulgmodid  19045  odmod  19476  cnfldmulg  21315  prmirredlem  21382  znidomb  21471  znrrg  21475  cply1mul  22183  chfacfscmul0  22745  chfacfscmulfsupp  22746  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulfsupp  22750  chfacfpmmulgsum  22751  cayhamlem1  22753  cpmadugsumlemF  22763  ovolunlem1  25398  uniioombllem3  25486  vitali  25514  mbfi1fseqlem3  25618  dvexp  25857  dvexp3  25882  plyeq0lem  26115  dgrcolem1  26179  aaliou3lem2  26251  aaliou3lem7  26257  pserdv2  26340  abelthlem6  26346  logtayl  26569  logtaylsum  26570  logtayl2  26571  cxpexp  26577  cxproot  26599  root1id  26664  root1eq1  26665  cxpeq  26667  logbgcd1irr  26704  atantayl  26847  atantayl2  26848  birthdaylem2  26862  dfef2  26881  emcllem2  26907  emcllem3  26908  zetacvg  26925  lgam1  26974  gamfac  26977  basellem2  26992  basellem3  26993  basellem5  26995  basellem8  26998  mumul  27091  fsumdvdscom  27095  muinv  27103  chtublem  27122  perfect  27142  pcbcctr  27187  bclbnd  27191  bposlem1  27195  bposlem6  27200  lgssq2  27249  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  2lgslem1a1  27300  2sqlem6  27334  2sqlem10  27339  2sqnn  27350  2sqreunnltlem  27361  rplogsumlem1  27395  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumiflem1  27412  dchrvmaeq0  27415  dchrisum0re  27424  logdivbnd  27467  cusgrsize2inds  29381  wlkdlem2  29611  crctcshwlkn0lem1  29740  crctcshwlkn0lem6  29745  0enwwlksnge1  29794  wspthsnonn0vne  29847  clwwlknwwlksn  29967  clwwlkinwwlk  29969  clwwlkel  29975  clwwlkf  29976  clwwlkf1  29978  wwlksubclwwlk  29987  eucrctshift  30172  eucrct2eupth  30174  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  ipasslem4  30763  ipasslem5  30764  isarchi3  33141  oddpwdc  34345  eulerpartlemb  34359  fibp1  34392  subfacp1lem6  35172  subfaclim  35175  snmlff  35316  circum  35661  divcnvlin  35720  bcprod  35725  iprodgam  35729  faclim  35733  faclim2  35735  nn0prpwlem  36310  nndivsub  36445  knoppndvlem13  36512  poimirlem13  37627  poimirlem14  37628  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  facp2  42131  nnadd1com  42255  nnaddcom  42256  dvdsexpnn0  42322  renegmulnnass  42453  fimgmcyc  42522  dffltz  42622  irrapxlem1  42810  pellexlem1  42817  pellqrex  42867  2nn0ind  42934  jm2.17c  42951  acongrep  42969  jm2.18  42977  jm2.20nn  42986  jm2.16nn0  42993  proot1ex  43185  hashnzfzclim  44311  binomcxplemnotnn0  44345  nnsplit  45354  clim1fr1  45599  sumnnodd  45628  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  dirkerper  46094  dirkertrigeqlem1  46096  fouriersw  46229  nnfoctbdjlem  46453  deccarry  47312  subsubelfzo0  47327  submodlt  47351  mod0mul  47357  m1modmmod  47359  modlt0b  47364  sqrtpwpw2p  47539  fmtnodvds  47545  fmtnoprmfac1  47566  fmtnoprmfac2lem1  47567  fmtnoprmfac2  47568  lighneallem2  47607  lighneallem3  47608  lighneallem4  47611  nnennexALTV  47702  perfectALTV  47724  fppr2odd  47732  fpprwppr  47740  fpprwpprb  47741  tgoldbachlt  47817  gpgedgvtx0  48052  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem5  48078  gpg3kgrtriex  48080  nnsgrp  48165  nnsgrpnmnd  48166  bcpascm1  48339  altgsumbcALT  48341  eluz2cnn0n1  48500  pw2m1lepw2m1  48509  nnennex  48514  logbpw2m1  48556  blenpw2m1  48568  nnpw2blen  48569  nnpw2pmod  48572  blennnt2  48578  blennn0em1  48580  nn0digval  48589  dignn0fr  48590  dignn0ldlem  48591  dig0  48595  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610