Theorem nncnd 12221

Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nncnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem nncnd

Step	Hyp	Ref	Expression
1		nnsscn 12210	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3934	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 11066  ℕcn 12205

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 7712  ax-1cn 11126  ax-addcl 11128

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 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-om 7841  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-nn 12206

This theorem is referenced by:  nnadddir  12264  nnmul1com  12265  nnmulcom  12266  nneo  12652  facdiv  14295  facndiv  14296  faclbnd  14298  faclbnd5  14306  faclbnd6  14307  facubnd  14308  facavg  14309  bccmpl  14317  bcn0  14318  bcn1  14321  bcm1k  14323  bcp1n  14324  bcp1nk  14325  bcval5  14326  bcpasc  14329  permnn  14334  hashf1  14465  hashfac  14466  relexpaddnn  15059  binom11  15843  binom1dif  15844  climcndslem2  15861  arisum2  15872  trireciplem  15873  trirecip  15874  geo2sum  15884  geo2lim  15886  fprodfac  15984  risefacfac  16046  fallfacfwd  16047  fallfacval4  16054  bcfallfac  16055  fallfacfac  16056  bpolycl  16063  bpolysum  16064  bpolydiflem  16065  fsumkthpow  16067  eftcl  16084  eftabs  16086  efcllem  16088  ege2le3  16101  efcj  16103  efaddlem  16104  eftlub  16122  eirrlem  16217  sqrt2irrlem  16261  oexpneg  16360  pwp1fsum  16406  bitsp1  16446  bitsfzolem  16449  bitsfzo  16450  bitsmod  16451  bitscmp  16453  bitsinv1lem  16456  bitsinv1  16457  2ebits  16462  bitsinvp1  16464  sadcaddlem  16472  sadadd3  16476  bitsres  16488  bitsuz  16489  bitsshft  16490  dvdsgcdidd  16552  mulgcd  16563  rplpwr  16573  sqgcd  16577  expgcd  16578  nn0expgcd  16579  lcmgcdlem  16621  3lcm2e6woprm  16630  coprmprod  16676  coprmproddvdslem  16677  cncongr1  16682  cncongr2  16683  prmind2  16700  isprm5  16723  divgcdodd  16726  prmdvdsexpr  16733  qmuldeneqnum  16763  divnumden  16764  qnumgt0  16766  numdensq  16770  numdenexp  16776  hashdvds  16791  phiprmpw  16792  prmdiv  16801  prmdivdiv  16803  phisum  16807  modprm0  16822  pythagtriplem4  16836  pythagtriplem6  16838  pythagtriplem7  16839  pythagtriplem14  16845  pythagtriplem15  16846  pythagtriplem19  16850  pythagtrip  16851  pcprendvds2  16858  pcpre1  16859  pcpremul  16860  pceulem  16862  pcdiv  16869  pcqmul  16870  pcelnn  16887  pcid  16890  pc2dvds  16896  dvdsprmpweqnn  16902  dvdsprmpweqle  16903  pcaddlem  16905  pcadd  16906  pcfaclem  16915  qexpz  16918  expnprm  16919  oddprmdvds  16920  prmpwdvds  16921  pockthlem  16922  pockthg  16923  infpnlem1  16927  prmreclem1  16933  prmreclem2  16934  prmreclem3  16935  prmreclem4  16936  prmreclem6  16938  4sqlem6  16960  4sqlem7  16961  4sqlem10  16964  mul4sqlem  16970  4sqlem11  16972  4sqlem12  16973  4sqlem14  16975  4sqlem17  16978  4sqlem18  16979  vdwlem1  16998  vdwlem2  16999  vdwlem3  17000  vdwlem5  17002  vdwlem6  17003  vdwlem8  17005  vdwlem9  17006  vdwlem10  17007  vdwlem12  17009  ramub1lem2  17044  ramcl  17046  prmop1  17055  prmdvdsprmo  17059  prmgaplem7  17074  prmgaplem8  17075  chnub  18635  gsumsgrpccat  18855  mulgnndir  19126  mulgnnass  19132  psgnunilem5  19515  odf1o2  19594  pgp0  19617  sylow1lem1  19619  odcau  19625  sylow2blem3  19643  sylow3lem3  19650  sylow3lem4  19651  gexexlem  19873  ablfacrp2  20090  ablfac1lem  20091  ablfac1eu  20096  pgpfac1lem3a  20099  pgpfac1lem3  20100  fincygsubgodexd  20136  zringlpirlem3  21494  znrrg  21595  psdpw  22213  cpmadugsumlemF  22914  lebnumlem3  25003  ovollb2lem  25528  ovolunlem1a  25536  ovolunlem1  25537  uniioombllem3  25625  uniioombllem4  25626  dyaddisjlem  25635  mbfi1fseqlem3  25757  mbfi1fseqlem4  25758  itgpowd  26090  dgrcolem1  26311  vieta1lem1  26349  vieta1lem2  26350  elqaalem2  26359  elqaalem3  26360  aalioulem1  26371  aaliou3lem2  26382  aaliou3lem8  26384  aaliou3lem6  26387  aaliou3lem9  26389  taylfvallem1  26395  tayl0  26400  taylply2  26406  taylply  26407  dvtaylp  26408  taylthlem1  26411  taylthlem2  26412  pserdvlem2  26466  advlogexp  26695  cxpmul2  26729  cxpeq  26797  rtprmirr  26800  atantayl3  26979  leibpi  26982  log2cnv  26984  log2tlbnd  26985  birthdaylem2  26992  birthdaylem3  26993  amgmlem  27029  amgm  27030  emcllem5  27039  fsumharmonic  27051  zetacvg  27054  dmgmdivn0  27067  lgamgulmlem3  27070  lgamgulmlem4  27071  lgamgulmlem5  27072  lgamgulmlem6  27073  lgamgulm2  27075  lgamcvg2  27094  gamcvg  27095  gamcvg2lem  27098  facgam  27105  wilthlem1  27107  wilthlem2  27108  wilthlem3  27109  wilthimp  27111  basellem1  27120  basellem2  27121  basellem3  27122  basellem4  27123  basellem5  27124  basellem8  27127  vmaprm  27156  sgmval2  27182  0sgm  27183  sgmf  27184  vma1  27205  fsumdvdsdiaglem  27222  dvdsflf1o  27226  muinv  27232  mpodvdsmulf1o  27233  dvdsmulf1o  27235  sgmppw  27236  1sgmprm  27238  1sgm2ppw  27239  sgmmul  27240  chtublem  27250  fsumvma2  27253  chpchtsum  27258  logfaclbnd  27261  logexprlim  27264  mersenne  27266  perfect1  27267  perfectlem1  27268  perfectlem2  27269  perfect  27270  dchrsum2  27307  dchrhash  27310  bcmono  27316  bcp1ctr  27318  bclbnd  27319  bposlem1  27323  bposlem2  27324  bposlem3  27325  bposlem5  27327  bposlem6  27328  lgsval2lem  27346  lgsqrlem2  27386  gausslemma2dlem6  27411  gausslemma2dlem7  27412  gausslemma2d  27413  lgseisenlem1  27414  lgseisenlem4  27417  lgsquadlem1  27419  lgsquadlem2  27420  lgsquadlem3  27421  lgsquad2  27425  m1lgs  27427  2sqlem3  27459  2sqlem4  27460  chebbnd1lem1  27508  chebbnd1  27511  rplogsumlem1  27523  rplogsumlem2  27524  rpvmasumlem  27526  dchrisumlem1  27528  dchrmusum2  27533  dchrvmasumlem1  27534  dchrvmasum2lem  27535  dchrvmasum2if  27536  dchrvmasumlem2  27537  dchrvmasumlem3  27538  dchrvmasumiflem1  27540  dchrisum0flblem1  27547  dchrisum0flblem2  27548  dchrisum0fno1  27550  rpvmasum2  27551  rplogsum  27566  mulogsumlem  27570  mulogsum  27571  mulog2sumlem2  27574  vmalogdivsum2  27577  vmalogdivsum  27578  2vmadivsumlem  27579  logsqvma  27581  selberglem2  27585  selberglem3  27586  selberg  27587  selberg2lem  27589  logdivbnd  27595  selberg3lem1  27596  selberg4lem1  27599  pntrsumo1  27604  pntrsumbnd2  27606  selberg3r  27608  selberg4r  27609  selberg34r  27610  pntsval2  27615  pntrlog2bndlem2  27617  pntrlog2bndlem4  27619  pntrlog2bndlem6  27622  pntpbnd1  27625  pntpbnd2  27626  pntlemg  27637  pntlemn  27639  pntlemf  27644  pnt  27653  padicabvf  27670  ostth2lem2  27673  ostth3  27677  fusgrhashclwwlkn  30225  eucrct2eupth  30391  nrt2irr  30619  elq2  32962  numdenneg  32965  ltesubnnd  32973  2exple2exp  32995  oexpled  32997  gsummptp1  33196  1arithidomlem2  33691  1arithidom  33692  zringfrac  33709  cos9thpiminplylem1  34038  cos9thpiminplylem2  34039  1smat1  34060  madjusmdetlem2  34084  madjusmdetlem4  34086  qqhnm  34246  oddpwdc  34610  eulerpartlemsv2  34614  eulerpartlems  34616  eulerpartlemsv3  34617  eulerpartlemgc  34618  eulerpartlemv  34620  eulerpartlemgs2  34636  fibp1  34657  ballotlemfc0  34749  ballotlemfcc  34750  signsvtn0  34826  reprpmtf1o  34882  vtscl  34894  hgt750lemb  34912  tgoldbachgt  34919  subfacp1lem1  35482  subfacp1lem5  35487  subfacval2  35490  subfaclim  35491  cvmliftlem2  35589  cvmliftlem7  35594  cvmliftlem10  35597  cvmliftlem11  35598  cvmliftlem13  35599  bcm1nt  36040  bcprod  36041  iprodgam  36045  faclimlem1  36046  faclimlem2  36047  faclim2  36051  nn0prpwlem  36635  nn0prpw  36636  knoppcnlem10  36893  knoppndvlem16  36918  poimirlem1  38073  poimirlem2  38074  poimirlem6  38078  poimirlem7  38079  poimirlem8  38080  poimirlem9  38081  poimirlem10  38082  poimirlem11  38083  poimirlem12  38084  poimirlem13  38085  poimirlem15  38087  poimirlem16  38088  poimirlem17  38089  poimirlem18  38090  poimirlem19  38091  poimirlem20  38092  poimirlem21  38093  poimirlem22  38094  poimirlem23  38095  poimirlem24  38096  poimirlem25  38097  poimirlem26  38098  poimirlem27  38099  poimirlem31  38103  nnproddivdvdsd  42570  lcmfunnnd  42582  lcmineqlem3  42601  lcmineqlem4  42602  lcmineqlem6  42604  lcmineqlem8  42606  lcmineqlem10  42608  lcmineqlem11  42609  lcmineqlem12  42610  lcmineqlem16  42614  lcmineqlem18  42616  lcmineqlem23  42621  dvrelogpow2b  42638  aks4d1p1p2  42640  aks4d1p1  42646  aks4d1p8  42657  primrootsunit1  42667  primrootscoprmpow  42669  posbezout  42670  primrootscoprbij  42672  primrootspoweq0  42676  aks6d1c1p3  42680  aks6d1c1p8  42685  aks6d1c2p2  42689  hashscontpow1  42691  2np3bcnp1  42714  2ap1caineq  42715  sticksstones10  42725  sticksstones12a  42727  sticksstones16  42732  sticksstones22  42738  bcled  42748  bcle2d  42749  aks6d1c7lem1  42750  aks6d1c7  42754  unitscyglem2  42766  unitscyglem4  42768  unitscyglem5  42769  aks5lem8  42771  oddnumth  42873  nicomachus  42874  zaddcom  43039  fltabcoprmex  43174  fltaccoprm  43175  fltbccoprm  43176  fltne  43179  flt4lem3  43183  flt4lem5elem  43186  flt4lem5a  43187  flt4lem5b  43188  flt4lem5c  43189  flt4lem5d  43190  flt4lem5e  43191  flt4lem5f  43192  flt4lem6  43193  flt4lem7  43194  nna4b4nsq  43195  fltltc  43196  fltnltalem  43197  fltnlta  43198  irrapxlem4  43355  irrapxlem5  43356  pellexlem2  43360  pellexlem6  43364  pell1234qrne0  43383  pell1234qrreccl  43384  pell1234qrmulcl  43385  pell1234qrdich  43391  pell14qrdich  43399  pell1qrge1  43400  pell1qr1  43401  pell14qrgapw  43406  rmxyneg  43450  rmxm1  43464  rmxluc  43466  rmxdbl  43469  jm2.19lem1  43519  jm2.27c  43537  relexpmulnn  44238  relexpmulg  44239  inductionexd  44684  hashnzfzclim  44851  bcccl  44868  bcc0  44869  bccp1k  44870  bccm1k  44871  binomcxplemwb  44877  fsumnncl  46101  mccllem  46126  clim1fr1  46130  sumnnodd  46159  dvsinexp  46438  dvxpaek  46467  dvnxpaek  46469  dvnprodlem2  46474  itgsinexplem1  46481  itgsinexp  46482  stoweidlem1  46528  stoweidlem11  46538  stoweidlem25  46552  stoweidlem26  46553  stoweidlem34  46561  stoweidlem37  46564  stoweidlem38  46565  stoweidlem42  46569  wallispi2lem1  46598  wallispi2  46600  stirlinglem4  46604  stirlinglem5  46605  stirlinglem10  46610  stirlinglem15  46615  dirkertrigeqlem3  46627  dirkertrigeq  46628  dirkercncflem2  46631  dirkercncflem4  46633  fourierdlem11  46645  fourierdlem15  46649  fourierdlem79  46712  fourierdlem83  46716  sqwvfourb  46756  etransclem14  46775  etransclem15  46776  etransclem20  46781  etransclem21  46782  etransclem22  46783  etransclem23  46784  etransclem24  46785  etransclem25  46786  etransclem28  46789  etransclem31  46792  etransclem32  46793  etransclem33  46794  etransclem34  46795  etransclem35  46796  etransclem38  46799  etransclem41  46802  etransclem44  46805  etransclem45  46806  etransclem47  46808  etransclem48  46809  nnfoctbdjlem  46982  deccarry  47858  iccpartgtprec  47979  fmtnoodd  48095  fmtnorec2lem  48104  fmtnorec2  48105  fmtnodvds  48106  goldbachthlem2  48108  fmtnorec3  48110  fmtnorec4  48111  fmtnoprmfac1lem  48126  fmtnoprmfac1  48127  fmtnoprmfac2lem1  48128  fmtnoprmfac2  48129  2pwp1prm  48151  sfprmdvdsmersenne  48165  lighneallem4b  48171  lighneal  48173  proththdlem  48175  proththd  48176  ppivalnnprm  48187  oexpnegALTV  48252  perfectALTVlem1  48296  perfectALTVlem2  48297  perfectALTV  48298  nnpw2pmod  49158  nnolog2flm1  49165  blennn0em1  49166  blengt1fldiv2p1  49168  nn0sumshdiglemB  49195  amgmlemALT  50377