Theorem nncn 10586

Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nncn	|- ( A e. NN -> A e. CC )

Proof of Theorem nncn

Step	Hyp	Ref	Expression
1		nnsscn 10583	. 2 |- NN C_ CC
2	1	sseli 3440	1 |- ( A e. NN -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1844   CCcc 9522   NNcn 10578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-i2m1 9592  ax-1ne0 9593  ax-rrecex 9596  ax-cnre 9597

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-ov 6283  df-om 6686  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-nn 10579

This theorem is referenced by:  nn1m1nn  10598  nn1suc  10599  nnaddcl  10600  nnmulcl  10601  nnsub  10617  nndiv  10619  nndivtr  10620  nnnn0addcl  10869  nn0nnaddcl  10870  elnnnn0  10882  nn0sub  10889  nnnegz  10910  elz2  10924  zaddcl  10947  nnaddm1cl  10963  zdiv  10976  zdivadd  10977  zdivmul  10978  nneo  10989  peano5uzi  10994  elq  11231  qmulz  11232  qaddcl  11245  qnegcl  11246  qmulcl  11247  qreccl  11249  rpnnen1lem5  11259  fseq1m1p1  11810  ubmelm1fzo  11947  quoremz  12022  quoremnn0ALT  12024  intfracq  12026  fldiv  12027  fldiv2  12028  modmulnn  12054  modidmul0OLD  12063  addmodid  12079  modaddmodup  12093  nn0ennn  12132  ser1const  12209  expneg  12220  expm1t  12240  nnsqcl  12284  nnlesq  12318  digit2  12345  digit1  12346  facdiv  12411  facndiv  12412  faclbnd  12414  faclbnd4lem1  12417  faclbnd4lem4  12420  bcn1  12437  bcm1k  12439  bcp1n  12440  bcval5  12442  bcn2m1  12448  swrdccatwrd  12751  cshwidxmod  12832  cshwidxm  12836  cshwidxn  12837  repswcshw  12838  isercoll2  13642  divcnv  13818  harmonic  13824  arisum  13825  arisum2  13826  expcnv  13829  geomulcvg  13839  mertenslem2  13848  ef0lem  14025  efexp  14047  ruclem12  14185  sqrt2irr  14193  divalgmod  14275  ndvdsadd  14277  modgcd  14385  gcddiv  14398  gcdmultiple  14399  gcdmultiplez  14400  rpmulgcd  14404  rplpwr  14405  sqgcd  14407  prmind2  14439  qredeq  14458  qredeu  14459  isprm6  14461  divnumden  14492  divdenle  14493  nn0gcdsq  14496  pythagtriplem1  14551  pythagtriplem2  14552  pythagtriplem6  14556  pythagtriplem7  14557  pythagtriplem12  14561  pythagtriplem14  14563  pythagtriplem15  14564  pythagtriplem16  14565  pythagtriplem17  14566  pythagtriplem19  14568  pcqcl  14591  pcexp  14594  pcneg  14608  fldivp1  14627  prmpwdvds  14633  infpnlem2  14640  prmreclem1  14645  prmreclem6  14650  4sqlem19  14692  vdwapun  14703  vdwapid1  14704  mulgnegnn  16478  mulgnnass  16496  odmod  16896  cply1mul  18657  cnfldmulg  18772  prmirredlem  18832  znidomb  18900  znrrg  18904  chfacfscmul0  19653  chfacfscmulfsupp  19654  chfacfscmulgsum  19655  chfacfpmmul0  19657  chfacfpmmulfsupp  19658  chfacfpmmulgsum  19659  cayhamlem1  19661  cpmadugsumlemF  19671  ovolunlem1  22202  uniioombllem3  22288  vitali  22316  mbfi1fseqlem3  22418  dvexp  22650  dvexp3  22673  plyeq0lem  22901  dgrcolem1  22964  aaliou3lem2  23033  aaliou3lem7  23039  pserdv2  23119  abelthlem6  23125  logtayl  23337  logtaylsum  23338  logtayl2  23339  cxpexp  23345  cxproot  23367  root1id  23426  root1eq1  23427  cxpeq  23429  atantayl  23595  atantayl2  23596  birthdaylem2  23610  dfef2  23628  emcllem2  23654  emcllem3  23655  zetacvg  23672  lgam1  23721  gamfac  23724  basellem2  23738  basellem3  23739  basellem5  23741  basellem8  23744  mumul  23838  dvdsdivcl  23840  dvdsflip  23841  fsumdvdscom  23844  muinv  23852  chtublem  23869  perfect  23889  pcbcctr  23934  bclbnd  23938  bposlem1  23942  bposlem6  23947  lgssq  23993  lgssq2  23994  2sqlem6  24027  2sqlem10  24032  rplogsumlem1  24052  dchrmusumlema  24061  dchrmusum2  24062  dchrvmasumiflem1  24069  dchrvmaeq0  24072  dchrisum0re  24081  logdivbnd  24124  cusgrasize2inds  24906  clwwlkel  25222  clwwlkf  25223  clwwlkf1  25225  wwlksubclwwlk  25233  rusgra0edg  25384  clwwlkextfrlem1  25505  numclwwlk2lem1  25531  numclwlk2lem2f  25532  numclwlk2lem2f1o  25534  gxnn0neg  25692  ipasslem4  26176  ipasslem5  26177  isarchi3  28196  oddpwdc  28812  eulerpartlemb  28826  fibp1  28859  subfacp1lem6  29495  subfaclim  29498  snmlff  29639  circum  29905  divcnvlin  29953  bcprod  29960  iprodgam  29964  faclim  29968  faclim2  29970  nn0prpwlem  30563  nndivsub  30702  mblfinlem2  31437  ovoliunnfl  31441  voliunnfl  31443  irrapxlem1  35132  pellexlem1  35139  pellqrex  35189  2nn0ind  35255  jm2.17c  35274  acongrep  35292  jm2.18  35305  jm2.20nn  35314  jm2.16nn0  35321  hashgcdlem  35534  proot1ex  35538  lcmgcdlem  36073  hashnzfzclim  36088  binomcxplemnotnn0  36122  clim1fr1  36988  sumnnodd  37017  wallispilem4  37231  wallispilem5  37232  wallispi  37233  wallispi2lem1  37234  wallispi2lem2  37235  wallispi2  37236  stirlinglem1  37237  stirlinglem3  37239  stirlinglem4  37240  stirlinglem5  37241  stirlinglem6  37242  stirlinglem7  37243  stirlinglem8  37244  stirlinglem10  37246  stirlinglem11  37247  stirlinglem12  37248  stirlinglem13  37249  stirlinglem14  37250  stirlinglem15  37251  dirkerper  37259  dirkertrigeqlem1  37261  fouriersw  37395  deccarry  37679  perfectALTV  37811  subsubelfzo0  37983  nnsgrp  38147  nnsgrpnmnd  38148  bcpascm1  38464  altgsumbcALT  38466  eluz2cnn0n1  38639  pw2m1lepw2m1  38651  mod0mul  38655  m1modmmod  38657  nn0enne  38659  nno  38661  logbpw2m1  38711  blenpw2m1  38723  nnpw2blen  38724  nnpw2pmod  38727  blennnt2  38733  blennn0em1  38735  nn0digval  38744  dignn0fr  38745  dignn0ldlem  38746  dig0  38750  nn0sumshdiglemA  38763  nn0sumshdiglemB  38764  nn0sumshdiglem1  38765