Theorem nncn 10905

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℕcn 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898

This theorem is referenced by:  nn1m1nn  10917  nn1suc  10918  nnaddcl  10919  nnmulcl  10920  nnsub  10936  nndiv  10938  nndivtr  10939  nnnn0addcl  11200  nn0nnaddcl  11201  elnnnn0  11213  nn0sub  11220  nnnegz  11257  elz2  11271  zaddcl  11294  nnaddm1cl  11311  zdiv  11323  zdivadd  11324  zdivmul  11325  nneo  11337  peano5uzi  11342  elq  11666  qmulz  11667  qaddcl  11680  qnegcl  11681  qmulcl  11682  qreccl  11684  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  nnledivrp  11816  nn0ledivnn  11817  fseq1m1p1  12284  ubmelm1fzo  12430  subfzo0  12452  quoremz  12516  quoremnn0ALT  12518  intfracq  12520  fldiv  12521  fldiv2  12522  modmulnn  12550  addmodid  12580  addmodidr  12581  modaddmodup  12595  modfzo0difsn  12604  modsumfzodifsn  12605  addmodlteq  12607  nn0ennn  12640  ser1const  12719  expneg  12730  expm1t  12750  nnsqcl  12795  nnlesq  12830  digit2  12859  digit1  12860  facdiv  12936  facndiv  12937  faclbnd  12939  faclbnd4lem1  12942  faclbnd4lem4  12945  bcn1  12962  bcm1k  12964  bcp1n  12965  bcval5  12967  bcn2m1  12973  swrdccatwrd  13320  cshwidxmod  13400  cshwidxm  13405  cshwidxn  13406  repswcshw  13409  isercoll2  14247  divcnv  14424  harmonic  14430  arisum  14431  arisum2  14432  expcnv  14435  geomulcvg  14446  mertenslem2  14456  ef0lem  14648  efexp  14670  ruclem12  14809  sqrt2irr  14817  nndivides  14828  modmulconst  14851  dvdsflip  14877  nn0enne  14932  nno  14936  pwp1fsum  14952  divalgmod  14967  divalgmodOLD  14968  ndvdsadd  14972  modgcd  15091  gcddiv  15106  gcdmultiple  15107  gcdmultiplez  15108  rpmulgcd  15113  rplpwr  15114  sqgcd  15116  lcmgcdlem  15157  qredeq  15209  qredeu  15210  cncongrcoprm  15222  prmind2  15236  isprm6  15264  divnumden  15294  divdenle  15295  nn0gcdsq  15298  hashgcdlem  15331  pythagtriplem1  15359  pythagtriplem2  15360  pythagtriplem6  15364  pythagtriplem7  15365  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem15  15372  pythagtriplem16  15373  pythagtriplem17  15374  pythagtriplem19  15376  pcqcl  15399  pcexp  15402  pcneg  15416  fldivp1  15439  oddprmdvds  15445  prmpwdvds  15446  infpnlem2  15453  prmreclem1  15458  prmreclem6  15463  4sqlem19  15505  vdwapun  15516  vdwapid1  15517  prmonn2  15581  prmgaplem7  15599  mulgnegnn  17374  mulgnnass  17399  mulgnnassOLD  17400  mulgmodid  17404  odmod  17788  cply1mul  19485  cnfldmulg  19597  prmirredlem  19660  znidomb  19729  znrrg  19733  chfacfscmul0  20482  chfacfscmulfsupp  20483  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulfsupp  20487  chfacfpmmulgsum  20488  cayhamlem1  20490  cpmadugsumlemF  20500  ovolunlem1  23072  uniioombllem3  23159  vitali  23188  mbfi1fseqlem3  23290  dvexp  23522  dvexp3  23545  plyeq0lem  23770  dgrcolem1  23833  aaliou3lem2  23902  aaliou3lem7  23908  pserdv2  23988  abelthlem6  23994  logtayl  24206  logtaylsum  24207  logtayl2  24208  cxpexp  24214  cxproot  24236  root1id  24295  root1eq1  24296  cxpeq  24298  atantayl  24464  atantayl2  24465  birthdaylem2  24479  dfef2  24497  emcllem2  24523  emcllem3  24524  zetacvg  24541  lgam1  24590  gamfac  24593  basellem2  24608  basellem3  24609  basellem5  24611  basellem8  24614  mumul  24707  fsumdvdscom  24711  muinv  24719  chtublem  24736  perfect  24756  pcbcctr  24801  bclbnd  24805  bposlem1  24809  bposlem6  24814  lgssq2  24863  gausslemma2dlem1a  24890  gausslemma2dlem3  24893  2lgslem1a1  24914  2sqlem6  24948  2sqlem10  24953  rplogsumlem1  24973  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumiflem1  24990  dchrvmaeq0  24993  dchrisum0re  25002  logdivbnd  25045  cusgrasize2inds  26005  clwwlkel  26321  clwwlkf  26322  clwwlkf1  26324  wwlksubclwwlk  26332  rusgra0edg  26482  clwwlkextfrlem1  26603  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  ipasslem4  27073  ipasslem5  27074  isarchi3  29072  oddpwdc  29743  eulerpartlemb  29757  fibp1  29790  subfacp1lem6  30421  subfaclim  30424  snmlff  30565  circum  30822  divcnvlin  30871  bcprod  30877  iprodgam  30881  faclim  30885  faclim2  30887  nn0prpwlem  31487  nndivsub  31626  knoppndvlem13  31685  poimirlem13  32592  poimirlem14  32593  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  irrapxlem1  36404  pellexlem1  36411  pellqrex  36461  2nn0ind  36528  jm2.17c  36547  acongrep  36565  jm2.18  36573  jm2.20nn  36582  jm2.16nn0  36589  proot1ex  36798  hashnzfzclim  37543  binomcxplemnotnn0  37577  nnsplit  38515  clim1fr1  38668  sumnnodd  38697  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem4  38970  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  dirkerper  38989  dirkertrigeqlem1  38991  fouriersw  39124  nnfoctbdjlem  39348  deccarry  39941  sqrtpwpw2p  39988  fmtnodvds  39994  fmtnoprmfac1  40015  fmtnoprmfac2lem1  40016  fmtnoprmfac2  40017  pwdif  40039  lighneallem2  40061  lighneallem3  40062  lighneallem4  40065  perfectALTV  40166  tgoldbachlt  40230  tgoldbachltOLD  40237  subsubelfzo0  40359  cusgrsize2inds  40669  1wlkdlem2  40892  crctcsh1wlkn0lem1  41013  crctcsh1wlkn0lem6  41018  0enwwlksnge1  41060  wspthsnonn0vne  41124  clwwlksel  41221  clwwlksf  41222  clwwlksf1  41224  wwlksubclwwlks  41232  eucrctshift  41411  eucrct2eupth  41413  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  nnsgrp  41607  nnsgrpnmnd  41608  bcpascm1  41922  altgsumbcALT  41924  eluz2cnn0n1  42095  pw2m1lepw2m1  42104  mod0mul  42108  m1modmmod  42110  logbpw2m1  42159  blenpw2m1  42171  nnpw2blen  42172  nnpw2pmod  42175  blennnt2  42181  blennn0em1  42183  nn0digval  42192  dignn0fr  42193  dignn0ldlem  42194  dig0  42198  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213