Theorem nncn 11500

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

Syntax hints:   → wi 4   ∈ wcel 2083  ℂcc 10388  ℕcn 11492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-1cn 10448  ax-addcl 10450

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-nn 11493

This theorem is referenced by:  nncni  11502  nn1m1nn  11512  nn1suc  11513  nnaddcl  11514  nnmulcl  11515  nnmtmip  11517  nnneneg  11526  nnsub  11535  nndiv  11537  nndivtr  11538  nnnn0addcl  11781  nn0nnaddcl  11782  elnnnn0  11794  nn0sub  11801  nnnegz  11838  elz2  11853  zaddcl  11876  nnaddm1cl  11893  zdiv  11906  zdivadd  11907  zdivmul  11908  nneo  11920  peano5uzi  11925  elq  12203  qmulz  12204  qaddcl  12218  qnegcl  12219  qmulcl  12220  qreccl  12222  rpnnen1lem5  12234  nnledivrp  12355  nn0ledivnn  12356  fseq1m1p1  12836  ubmelm1fzo  12987  subfzo0  13013  quoremz  13077  quoremnn0ALT  13079  intfracq  13081  fldiv  13082  fldiv2  13083  modmulnn  13111  addmodid  13141  addmodidr  13142  modaddmodup  13156  modfzo0difsn  13165  modsumfzodifsn  13166  addmodlteq  13168  nn0ennn  13201  ser1const  13280  expneg  13291  expm1t  13311  nnsqcl  13347  nnlesq  13422  digit2  13451  digit1  13452  expnngt1  13456  facdiv  13501  facndiv  13502  faclbnd  13504  faclbnd4lem1  13507  faclbnd4lem4  13510  bcn1  13527  bcm1k  13529  bcp1n  13530  bcval5  13532  bcn2m1  13538  cshwidxmod  14005  cshwidxm  14010  cshwidxn  14011  repswcshw  14014  isercoll2  14863  divcnv  15045  harmonic  15051  arisum  15052  arisum2  15053  expcnv  15056  pwdif  15060  geomulcvg  15069  mertenslem2  15078  ef0lem  15269  efexp  15291  ruclem12  15431  sqrt2irr  15439  nndivides  15454  modmulconst  15478  dvdsflip  15504  nn0enne  15565  nno  15570  pwp1fsum  15579  divalgmod  15594  ndvdsadd  15598  modgcd  15717  gcddiv  15732  gcdmultiple  15733  gcdmultiplez  15734  rpmulgcd  15739  rplpwr  15740  sqgcd  15742  lcmgcdlem  15783  qredeq  15834  qredeu  15835  cncongrcoprm  15847  prmind2  15862  isprm6  15891  divnumden  15921  divdenle  15922  nn0gcdsq  15925  hashgcdlem  15958  pythagtriplem1  15986  pythagtriplem2  15987  pythagtriplem6  15991  pythagtriplem7  15992  pythagtriplem12  15996  pythagtriplem14  15998  pythagtriplem15  15999  pythagtriplem16  16000  pythagtriplem17  16001  pythagtriplem19  16003  pcqcl  16026  pcexp  16029  pcneg  16043  fldivp1  16066  oddprmdvds  16072  prmpwdvds  16073  infpnlem2  16080  prmreclem1  16085  prmreclem6  16090  4sqlem19  16132  vdwapun  16143  vdwapid1  16144  prmonn2  16208  prmgaplem7  16226  mulgnegnn  17997  mulgnnass  18020  mulgmodid  18024  odmod  18409  cply1mul  20149  cnfldmulg  20263  prmirredlem  20326  znidomb  20394  znrrg  20398  chfacfscmul0  21154  chfacfscmulfsupp  21155  chfacfscmulgsum  21156  chfacfpmmul0  21158  chfacfpmmulfsupp  21159  chfacfpmmulgsum  21160  cayhamlem1  21162  cpmadugsumlemF  21172  ovolunlem1  23785  uniioombllem3  23873  vitali  23901  mbfi1fseqlem3  24005  dvexp  24237  dvexp3  24262  plyeq0lem  24487  dgrcolem1  24550  aaliou3lem2  24619  aaliou3lem7  24625  pserdv2  24705  abelthlem6  24711  logtayl  24928  logtaylsum  24929  logtayl2  24930  cxpexp  24936  cxproot  24958  root1id  25020  root1eq1  25021  cxpeq  25023  logbgcd1irr  25057  atantayl  25200  atantayl2  25201  birthdaylem2  25216  dfef2  25234  emcllem2  25260  emcllem3  25261  zetacvg  25278  lgam1  25327  gamfac  25330  basellem2  25345  basellem3  25346  basellem5  25348  basellem8  25351  mumul  25444  fsumdvdscom  25448  muinv  25456  chtublem  25473  perfect  25493  pcbcctr  25538  bclbnd  25542  bposlem1  25546  bposlem6  25551  lgssq2  25600  gausslemma2dlem1a  25627  gausslemma2dlem3  25630  2lgslem1a1  25651  2sqlem6  25685  2sqlem10  25690  2sqnn  25701  2sqreunnltlem  25712  rplogsumlem1  25746  dchrmusumlema  25755  dchrmusum2  25756  dchrvmasumiflem1  25763  dchrvmaeq0  25766  dchrisum0re  25775  logdivbnd  25818  cusgrsize2inds  26922  wlkdlem2  27151  crctcshwlkn0lem1  27274  crctcshwlkn0lem6  27279  0enwwlksnge1  27328  wspthsnonn0vne  27382  clwwlknwwlksn  27502  clwwlkinwwlk  27504  clwwlkel  27511  clwwlkf  27512  clwwlkf1  27514  wwlksubclwwlk  27523  eucrctshift  27708  eucrct2eupth  27710  numclwwlk2lem1  27843  numclwlk2lem2f  27844  numclwlk2lem2f1o  27846  ipasslem4  28298  ipasslem5  28299  isarchi3  30450  oddpwdc  31225  eulerpartlemb  31239  fibp1  31272  subfacp1lem6  32042  subfaclim  32045  snmlff  32186  circum  32527  divcnvlin  32574  bcprod  32580  iprodgam  32584  faclim  32588  faclim2  32590  nn0prpwlem  33281  nndivsub  33416  knoppndvlem13  33474  poimirlem13  34457  poimirlem14  34458  poimirlem29  34473  poimirlem30  34474  poimirlem31  34475  poimirlem32  34476  mblfinlem2  34482  ovoliunnfl  34486  voliunnfl  34488  nnadd1com  38706  nnaddcom  38707  expgcd  38726  nn0expgcd  38727  dffltz  38789  irrapxlem1  38925  pellexlem1  38932  pellqrex  38982  2nn0ind  39048  jm2.17c  39065  acongrep  39083  jm2.18  39091  jm2.20nn  39100  jm2.16nn0  39107  proot1ex  39307  hashnzfzclim  40213  binomcxplemnotnn0  40247  nnsplit  41188  clim1fr1  41445  sumnnodd  41474  wallispilem4  41917  wallispilem5  41918  wallispi  41919  wallispi2lem1  41920  wallispi2lem2  41921  wallispi2  41922  stirlinglem1  41923  stirlinglem3  41925  stirlinglem4  41926  stirlinglem5  41927  stirlinglem6  41928  stirlinglem7  41929  stirlinglem8  41930  stirlinglem10  41932  stirlinglem11  41933  stirlinglem12  41934  stirlinglem13  41935  stirlinglem14  41936  stirlinglem15  41937  dirkerper  41945  dirkertrigeqlem1  41947  fouriersw  42080  nnfoctbdjlem  42301  deccarry  43049  subsubelfzo0  43064  sqrtpwpw2p  43204  fmtnodvds  43210  fmtnoprmfac1  43231  fmtnoprmfac2lem1  43232  fmtnoprmfac2  43233  lighneallem2  43275  lighneallem3  43276  lighneallem4  43279  nnennexALTV  43370  perfectALTV  43392  fppr2odd  43400  fpprwppr  43408  fpprwpprb  43409  tgoldbachlt  43485  nnsgrp  43588  nnsgrpnmnd  43589  bcpascm1  43899  altgsumbcALT  43901  eluz2cnn0n1  44069  pw2m1lepw2m1  44078  mod0mul  44082  m1modmmod  44084  nnennex  44088  logbpw2m1  44130  blenpw2m1  44142  nnpw2blen  44143  nnpw2pmod  44146  blennnt2  44152  blennn0em1  44154  nn0digval  44163  dignn0fr  44164  dignn0ldlem  44165  dig0  44169  nn0sumshdiglemA  44182  nn0sumshdiglemB  44183  nn0sumshdiglem1  44184