Theorem nncn 10317

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 10314	. 2 |- NN C_ CC
2	1	sseli 3340	1 |- ( A e. NN -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1755   CCcc 9267   NNcn 10309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-i2m1 9337  ax-1ne0 9338  ax-rrecex 9341  ax-cnre 9342

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10310

This theorem is referenced by:  nn1m1nn  10329  nn1suc  10330  nnaddcl  10331  nnmulcl  10332  nnsub  10347  nndiv  10349  nndivtr  10350  nnnn0addcl  10597  nn0nnaddcl  10598  elnnnn0  10610  nn0sub  10617  nnnegz  10636  elz2  10650  zaddcl  10672  nnaddm1cl  10688  zdiv  10699  zdivadd  10700  zdivmul  10701  nneo  10712  peano5uzi  10717  uzindOLD  10723  elq  10942  qmulz  10943  qaddcl  10956  qnegcl  10957  qmulcl  10958  qreccl  10960  rpnnen1lem5  10970  fseq1m1p1  11518  ubmelm1fzo  11606  quoremz  11677  quoremnn0ALT  11679  intfracq  11681  fldiv  11682  fldiv2  11683  modmulnn  11708  modidmul0  11717  modaddmodup  11745  nn0ennn  11784  ser1const  11845  expneg  11856  expm1t  11875  nnsqcl  11918  nnlesq  11952  digit2  11980  digit1  11981  facdiv  12046  facndiv  12047  faclbnd  12049  faclbnd4lem1  12052  faclbnd4lem4  12055  bcn1  12072  bcm1k  12074  bcp1n  12075  bcval5  12077  bcn2m1  12083  swrdccatwrd  12345  cshwidxmod  12423  cshwidxm  12427  cshwidxn  12428  repswcshw  12429  isercoll2  13129  divcnv  13298  harmonic  13303  arisum  13304  arisum2  13305  expcnv  13308  geomulcvg  13318  mertenslem2  13327  ef0lem  13346  efexp  13367  ruclem12  13505  sqr2irr  13513  divalgmod  13592  ndvdsadd  13594  modgcd  13702  gcddiv  13715  gcdmultiple  13716  gcdmultiplez  13717  rpmulgcd  13721  rplpwr  13722  sqgcd  13724  prmind2  13756  qredeq  13774  qredeu  13775  isprm6  13777  divnumden  13808  divdenle  13809  nn0gcdsq  13812  pythagtriplem1  13865  pythagtriplem2  13866  pythagtriplem6  13870  pythagtriplem7  13871  pythagtriplem12  13875  pythagtriplem14  13877  pythagtriplem15  13878  pythagtriplem16  13879  pythagtriplem17  13880  pythagtriplem19  13882  pcqcl  13905  pcexp  13908  pcneg  13922  fldivp1  13941  prmpwdvds  13947  infpnlem2  13954  prmreclem1  13959  prmreclem6  13964  4sqlem19  14006  vdwapun  14017  vdwapid1  14018  mulgnegnn  15616  mulgnnass  15634  odmod  16028  cnfldmulg  17691  prmirredlem  17758  prmirredlemOLD  17761  znidomb  17835  znrrg  17839  ovolunlem1  20821  uniioombllem3  20906  vitali  20934  mbfi1fseqlem3  21036  dvexp  21268  dvexp3  21291  plyeq0lem  21562  dgrcolem1  21624  aaliou3lem2  21693  aaliou3lem7  21699  pserdv2  21779  abelthlem6  21785  logtayl  21989  logtaylsum  21990  logtayl2  21991  cxpexp  21997  cxproot  22019  root1id  22076  root1eq1  22077  cxpeq  22079  atantayl  22216  atantayl2  22217  birthdaylem2  22230  dfef2  22248  emcllem2  22274  emcllem3  22275  basellem2  22303  basellem3  22304  basellem5  22306  basellem8  22309  mumul  22403  dvdsdivcl  22405  dvdsflip  22406  fsumdvdscom  22409  muinv  22417  chtublem  22434  perfect  22454  pcbcctr  22499  bclbnd  22503  bposlem1  22507  bposlem6  22512  lgssq  22558  lgssq2  22559  2sqlem6  22592  2sqlem10  22597  rplogsumlem1  22617  dchrmusumlema  22626  dchrmusum2  22627  dchrvmasumiflem1  22634  dchrvmaeq0  22637  dchrisum0re  22646  logdivbnd  22689  cusgrasize2inds  23207  gxnn0neg  23572  ipasslem4  24056  ipasslem5  24057  isarchi3  26027  oddpwdc  26584  eulerpartlemb  26598  fibp1  26631  zetacvg  26848  lgam1  26897  gamfac  26900  subfacp1lem6  26920  subfaclim  26923  snmlff  27065  circum  27165  divcnvlin  27245  iprodgam  27352  faclim  27398  faclim2  27400  nndivsub  28150  mblfinlem2  28270  ovoliunnfl  28274  voliunnfl  28276  nn0prpwlem  28358  irrapxlem1  29005  pellexlem1  29012  pellqrex  29062  2nn0ind  29128  jm2.17c  29147  acongrep  29165  jm2.18  29179  jm2.20nn  29188  jm2.16nn0  29195  hashgcdlem  29407  proot1ex  29411  clim1fr1  29617  wallispilem4  29706  wallispilem5  29707  wallispi  29708  wallispi2lem1  29709  wallispi2lem2  29710  wallispi2  29711  stirlinglem1  29712  stirlinglem3  29714  stirlinglem4  29715  stirlinglem5  29716  stirlinglem6  29717  stirlinglem7  29718  stirlinglem8  29719  stirlinglem10  29721  stirlinglem11  29722  stirlinglem12  29723  stirlinglem13  29724  stirlinglem14  29725  stirlinglem15  29726  subsubelfzo0  30053  clwwlkel  30298  clwwlkf  30299  clwwlkf1  30301  wwlksubclwwlk  30309  rusgra0edg  30416  clwwlkextfrlem1  30512  numclwwlk2lem1  30538  numclwlk2lem2f  30539  numclwlk2lem2f1o  30541