Theorem nncn 12215

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 11068  ℕcn 12207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714  ax-1cn 11128  ax-addcl 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-nn 12208

This theorem is referenced by:  nncni  12217  nn1m1nn  12228  nn1suc  12229  nnaddcl  12230  nnmulcl  12231  nnadd1com  12233  nnaddcom  12234  nnmtmip  12236  nnneneg  12245  nnsub  12254  nndiv  12256  nndivtr  12257  nnnn0addcl  12508  nn0nnaddcl  12509  elnnnn0  12521  nn0sub  12528  nnnegz  12568  elz2  12583  zaddcl  12608  nnaddm1cl  12627  zdiv  12640  zdivadd  12641  zdivmul  12642  nneo  12654  peano5uzi  12659  elq  12948  qmulz  12949  qaddcl  12963  qnegcl  12964  qmulcl  12965  qreccl  12967  rpnnen1lem5  12979  nnledivrp  13104  nn0ledivnn  13105  fseq1m1p1  13601  ubmelm1fzo  13766  subfzo0  13795  quoremz  13862  quoremnn0ALT  13864  intfracq  13866  fldiv  13867  fldiv2  13868  modmulnn  13896  addmodid  13929  addmodidr  13930  modaddmodup  13944  modfzo0difsn  13953  modsumfzodifsn  13954  addmodlteq  13956  nn0ennn  13989  ser1const  14068  expneg  14079  expm1t  14100  nnsqcl  14138  nnlesq  14215  digit2  14246  digit1  14247  expnngt1  14251  facdiv  14297  facndiv  14298  faclbnd  14300  faclbnd4lem1  14303  faclbnd4lem4  14306  bcn1  14323  bcm1k  14325  bcp1n  14326  bcval5  14328  bcn2m1  14334  cshwidxmod  14813  cshwidxm  14818  cshwidxn  14819  repswcshw  14822  isercoll2  15679  divcnv  15866  harmonic  15872  arisum  15873  arisum2  15874  expcnv  15877  pwdif  15881  geomulcvg  15889  mertenslem2  15898  ef0lem  16091  efexp  16116  ruclem12  16256  sqrt2irr  16264  nndivides  16279  modmulconst  16305  dvdsflip  16334  nn0enne  16394  nno  16399  pwp1fsum  16408  divalgmod  16423  ndvdsadd  16427  modgcd  16549  gcdmultiplez  16552  gcddiv  16568  rpmulgcd  16574  rplpwr  16575  sqgcd  16579  expgcd  16580  nn0expgcd  16581  lcmgcdlem  16623  qredeq  16674  qredeu  16675  cncongrcoprm  16687  prmind2  16702  isprm6  16732  divnumden  16766  divdenle  16767  nn0gcdsq  16770  hashgcdlem  16806  pythagtriplem1  16835  pythagtriplem2  16836  pythagtriplem6  16840  pythagtriplem7  16841  pythagtriplem12  16845  pythagtriplem14  16847  pythagtriplem15  16848  pythagtriplem16  16849  pythagtriplem17  16850  pythagtriplem19  16852  pcqcl  16875  pcexp  16878  pcneg  16893  fldivp1  16916  oddprmdvds  16922  prmpwdvds  16923  infpnlem2  16930  prmreclem1  16935  prmreclem6  16940  4sqlem19  16982  vdwapun  16993  vdwapid1  16994  prmonn2  17058  prmgaplem7  17076  mulgnegnn  19109  mulgnnass  19134  mulgmodid  19138  odmod  19569  cnfldmulg  21436  prmirredlem  21504  znidomb  21593  znrrg  21597  cply1mul  22339  chfacfscmul0  22898  chfacfscmulfsupp  22899  chfacfscmulgsum  22900  chfacfpmmul0  22902  chfacfpmmulfsupp  22903  chfacfpmmulgsum  22904  cayhamlem1  22906  cpmadugsumlemF  22916  ovolunlem1  25539  uniioombllem3  25627  vitali  25655  mbfi1fseqlem3  25759  dvexp  25995  dvexp3  26020  plyeq0lem  26250  dgrcolem1  26313  aaliou3lem2  26384  aaliou3lem7  26390  pserdv2  26470  abelthlem6  26476  logtayl  26702  logtaylsum  26703  logtayl2  26704  cxpexp  26710  cxproot  26732  root1id  26796  root1eq1  26797  cxpeq  26799  logbgcd1irr  26836  atantayl  26979  atantayl2  26980  birthdaylem2  26994  dfef2  27012  emcllem2  27038  emcllem3  27039  zetacvg  27056  lgam1  27105  gamfac  27108  basellem2  27123  basellem3  27124  basellem5  27126  basellem8  27129  mumul  27222  fsumdvdscom  27226  muinv  27234  chtublem  27252  perfect  27272  pcbcctr  27317  bclbnd  27321  bposlem1  27325  bposlem6  27330  lgssq2  27379  gausslemma2dlem1a  27406  gausslemma2dlem3  27409  2lgslem1a1  27430  2sqlem6  27464  2sqlem10  27469  2sqnn  27480  2sqreunnltlem  27491  rplogsumlem1  27525  dchrmusumlema  27534  dchrmusum2  27535  dchrvmasumiflem1  27542  dchrvmaeq0  27545  dchrisum0re  27554  logdivbnd  27597  cusgrsize2inds  29600  wlkdlem2  29828  crctcshwlkn0lem1  29956  crctcshwlkn0lem6  29961  0enwwlksnge1  30010  wspthsnonn0vne  30063  clwwlknwwlksn  30186  clwwlkinwwlk  30188  clwwlkel  30194  clwwlkf  30195  clwwlkf1  30197  wwlksubclwwlk  30206  eucrctshift  30391  eucrct2eupth  30393  numclwwlk2lem1  30524  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  ipasslem4  30983  ipasslem5  30984  isarchi3  33328  oddpwdc  34612  eulerpartlemb  34626  fibp1  34659  subfacp1lem6  35499  subfaclim  35502  snmlff  35643  circum  35988  divcnvlin  36047  bcprod  36052  iprodgam  36056  faclim  36060  faclim2  36062  nn0prpwlem  36646  nndivsub  36781  knoppndvlem13  36926  poimirlem13  38096  poimirlem14  38097  poimirlem29  38112  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  mblfinlem2  38121  ovoliunnfl  38125  voliunnfl  38127  facp2  42724  dvdsexpnn0  42907  renegmulnnass  43051  fimgmcyc  43116  dffltz  43180  irrapxlem1  43363  pellexlem1  43370  pellqrex  43420  2nn0ind  43486  jm2.17c  43503  acongrep  43521  jm2.18  43529  jm2.20nn  43538  jm2.16nn0  43545  proot1ex  43737  hashnzfzclim  44862  binomcxplemnotnn0  44896  nnsplit  45898  clim1fr1  46141  sumnnodd  46170  wallispilem4  46606  wallispilem5  46607  wallispi  46608  wallispi2lem1  46609  wallispi2lem2  46610  wallispi2  46611  stirlinglem1  46612  stirlinglem3  46614  stirlinglem4  46615  stirlinglem5  46616  stirlinglem6  46617  stirlinglem7  46618  stirlinglem8  46619  stirlinglem10  46621  stirlinglem11  46622  stirlinglem12  46623  stirlinglem13  46624  stirlinglem14  46625  stirlinglem15  46626  dirkerper  46634  dirkertrigeqlem1  46636  fouriersw  46769  nnfoctbdjlem  46993  deccarry  47869  subsubelfzo0  47885  submodlt  47914  mod0mul  47920  m1modmmod  47922  modlt0b  47927  sqrtpwpw2p  48111  fmtnodvds  48117  fmtnoprmfac1  48138  fmtnoprmfac2lem1  48139  fmtnoprmfac2  48140  lighneallem2  48179  lighneallem3  48180  lighneallem4  48183  nnennexALTV  48287  perfectALTV  48309  fppr2odd  48317  fpprwppr  48325  fpprwpprb  48326  tgoldbachlt  48402  gpgedgvtx0  48647  gpg3kgrtriexlem2  48670  gpg3kgrtriexlem5  48673  gpg3kgrtriex  48675  nnsgrp  48763  nnsgrpnmnd  48764  bcpascm1  48937  altgsumbcALT  48939  eluz2cnn0n1  49097  pw2m1lepw2m1  49106  nnennex  49111  logbpw2m1  49153  blenpw2m1  49165  nnpw2blen  49166  nnpw2pmod  49169  blennnt2  49175  blennn0em1  49177  nn0digval  49186  dignn0fr  49187  dignn0ldlem  49188  dig0  49192  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206  nn0sumshdiglem1  49207