Theorem nncn 10551

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

Syntax hints:   -> wi 4   e. wcel 1804   CCcc 9493   NNcn 10543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-om 6686  df-recs 7044  df-rdg 7078  df-nn 10544

This theorem is referenced by:  nn1m1nn  10563  nn1suc  10564  nnaddcl  10565  nnmulcl  10566  nnsub  10581  nndiv  10583  nndivtr  10584  nnnn0addcl  10833  nn0nnaddcl  10834  elnnnn0  10846  nn0sub  10853  nnnegz  10874  elz2  10888  zaddcl  10911  nnaddm1cl  10927  zdiv  10940  zdivadd  10941  zdivmul  10942  nneo  10953  peano5uzi  10958  uzindOLD  10964  elq  11194  qmulz  11195  qaddcl  11208  qnegcl  11209  qmulcl  11210  qreccl  11212  rpnnen1lem5  11222  fseq1m1p1  11763  ubmelm1fzo  11889  quoremz  11963  quoremnn0ALT  11965  intfracq  11967  fldiv  11968  fldiv2  11969  modmulnn  11994  modidmul0  12003  modaddmodup  12031  nn0ennn  12070  ser1const  12144  expneg  12155  expm1t  12175  nnsqcl  12218  nnlesq  12252  digit2  12280  digit1  12281  facdiv  12346  facndiv  12347  faclbnd  12349  faclbnd4lem1  12352  faclbnd4lem4  12355  bcn1  12372  bcm1k  12374  bcp1n  12375  bcval5  12377  bcn2m1  12383  swrdccatwrd  12674  cshwidxmod  12755  cshwidxm  12759  cshwidxn  12760  repswcshw  12761  isercoll2  13472  divcnv  13646  harmonic  13651  arisum  13652  arisum2  13653  expcnv  13656  geomulcvg  13666  mertenslem2  13675  ef0lem  13795  efexp  13817  ruclem12  13955  sqrt2irr  13963  divalgmod  14045  ndvdsadd  14047  modgcd  14155  gcddiv  14168  gcdmultiple  14169  gcdmultiplez  14170  rpmulgcd  14174  rplpwr  14175  sqgcd  14177  prmind2  14209  qredeq  14228  qredeu  14229  isprm6  14231  divnumden  14262  divdenle  14263  nn0gcdsq  14266  pythagtriplem1  14321  pythagtriplem2  14322  pythagtriplem6  14326  pythagtriplem7  14327  pythagtriplem12  14331  pythagtriplem14  14333  pythagtriplem15  14334  pythagtriplem16  14335  pythagtriplem17  14336  pythagtriplem19  14338  pcqcl  14361  pcexp  14364  pcneg  14378  fldivp1  14397  prmpwdvds  14403  infpnlem2  14410  prmreclem1  14415  prmreclem6  14420  4sqlem19  14462  vdwapun  14473  vdwapid1  14474  mulgnegnn  16130  mulgnnass  16148  odmod  16548  cply1mul  18313  cnfldmulg  18428  prmirredlem  18500  prmirredlemOLD  18503  znidomb  18577  znrrg  18581  chfacfscmul0  19336  chfacfscmulfsupp  19337  chfacfscmulgsum  19338  chfacfpmmul0  19340  chfacfpmmulfsupp  19341  chfacfpmmulgsum  19342  cayhamlem1  19344  cpmadugsumlemF  19354  ovolunlem1  21885  uniioombllem3  21971  vitali  21999  mbfi1fseqlem3  22101  dvexp  22333  dvexp3  22356  plyeq0lem  22584  dgrcolem1  22646  aaliou3lem2  22715  aaliou3lem7  22721  pserdv2  22801  abelthlem6  22807  logtayl  23017  logtaylsum  23018  logtayl2  23019  cxpexp  23025  cxproot  23047  root1id  23104  root1eq1  23105  cxpeq  23107  atantayl  23244  atantayl2  23245  birthdaylem2  23258  dfef2  23276  emcllem2  23302  emcllem3  23303  basellem2  23331  basellem3  23332  basellem5  23334  basellem8  23337  mumul  23431  dvdsdivcl  23433  dvdsflip  23434  fsumdvdscom  23437  muinv  23445  chtublem  23462  perfect  23482  pcbcctr  23527  bclbnd  23531  bposlem1  23535  bposlem6  23540  lgssq  23586  lgssq2  23587  2sqlem6  23620  2sqlem10  23625  rplogsumlem1  23645  dchrmusumlema  23654  dchrmusum2  23655  dchrvmasumiflem1  23662  dchrvmaeq0  23665  dchrisum0re  23674  logdivbnd  23717  cusgrasize2inds  24453  clwwlkel  24769  clwwlkf  24770  clwwlkf1  24772  wwlksubclwwlk  24780  rusgra0edg  24931  clwwlkextfrlem1  25052  numclwwlk2lem1  25078  numclwlk2lem2f  25079  numclwlk2lem2f1o  25081  gxnn0neg  25241  ipasslem4  25725  ipasslem5  25726  isarchi3  27708  oddpwdc  28270  eulerpartlemb  28284  fibp1  28317  zetacvg  28534  lgam1  28583  gamfac  28586  subfacp1lem6  28606  subfaclim  28609  snmlff  28751  circum  29017  divcnvlin  29095  iprodgam  29100  faclim  29146  faclim2  29148  nndivsub  29897  mblfinlem2  30027  ovoliunnfl  30031  voliunnfl  30033  nn0prpwlem  30115  irrapxlem1  30733  pellexlem1  30740  pellqrex  30790  2nn0ind  30856  jm2.17c  30875  acongrep  30893  jm2.18  30905  jm2.20nn  30914  jm2.16nn0  30921  hashgcdlem  31133  proot1ex  31137  lcmgcdlem  31188  hashnzfzclim  31203  clim1fr1  31515  sumnnodd  31544  wallispilem4  31739  wallispilem5  31740  wallispi  31741  wallispi2lem1  31742  wallispi2lem2  31743  wallispi2  31744  stirlinglem1  31745  stirlinglem3  31747  stirlinglem4  31748  stirlinglem5  31749  stirlinglem6  31750  stirlinglem7  31751  stirlinglem8  31752  stirlinglem10  31754  stirlinglem11  31755  stirlinglem12  31756  stirlinglem13  31757  stirlinglem14  31758  stirlinglem15  31759  dirkerper  31767  dirkertrigeqlem1  31769  fouriersw  31903  subsubelfzo0  32176  nnsgrp  32342  nnsgrpnmnd  32343  bcpascm1  32673  altgsumbcALT  32675