Theorem nncnd 12329

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 12318	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3929	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11176  ℕcn 12313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740  ax-1cn 11236  ax-addcl 11238

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-nn 12314

This theorem is used by:  nnadddir  12372  nnmul1com  12373  nnmulcom  12374  nneo  12761  facdiv  14408  facndiv  14409  faclbnd  14411  faclbnd5  14419  faclbnd6  14420  facubnd  14421  facavg  14422  bccmpl  14430  bcn0  14431  bcn1  14434  bcm1k  14436  bcp1n  14437  bcp1nk  14438  bcval5  14439  bcpasc  14442  permnn  14447  hashf1  14579  hashfac  14580  relexpaddnn  15181  binom11  15978  binom1dif  15979  climcndslem2  15996  arisum2  16007  trireciplem  16008  trirecip  16009  geo2sum  16019  geo2lim  16021  fprodfac  16117  risefacfac  16178  fallfacfwd  16179  fallfacval4  16186  bcfallfac  16187  fallfacfac  16188  bpolycl  16195  bpolysum  16196  bpolydiflem  16197  fsumkthpow  16199  eftcl  16216  eftabs  16218  efcllem  16220  ege2le3  16233  efcj  16235  efaddlem  16236  eftlub  16254  eirrlem  16349  sqrt2irrlem  16393  oexpneg  16492  pwp1fsum  16538  bitsp1  16578  bitsfzolem  16581  bitsfzo  16582  bitsmod  16583  bitscmp  16585  bitsinv1lem  16588  bitsinv1  16589  2ebits  16594  bitsinvp1  16596  sadcaddlem  16604  sadadd3  16608  bitsres  16620  bitsuz  16621  bitsshft  16622  dvdsgcdidd  16687  mulgcd  16698  rplpwr  16709  sqgcd  16713  expgcd  16714  nn0expgcd  16715  lcmgcdlem  16758  3lcm2e6woprm  16767  coprmprod  16813  coprmproddvdslem  16814  cncongr1  16819  cncongr2  16820  prmind2  16837  isprm5  16860  divgcdodd  16863  prmdvdsexpr  16870  qmuldeneqnum  16900  divnumden  16901  qnumgt0  16903  numdensq  16907  numdenexp  16914  hashdvds  16929  phiprmpw  16930  prmdiv  16939  prmdivdiv  16941  phisum  16945  modprm0  16960  pythagtriplem4  16974  pythagtriplem6  16976  pythagtriplem7  16977  pythagtriplem14  16983  pythagtriplem15  16984  pythagtriplem19  16988  pythagtrip  16989  pcprendvds2  16996  pcpre1  16997  pcpremul  16998  pceulem  17000  pcdiv  17007  pcqmul  17008  pcelnn  17025  pcid  17028  pc2dvds  17034  dvdsprmpweqnn  17040  dvdsprmpweqle  17041  pcaddlem  17043  pcadd  17044  pcfaclem  17053  qexpz  17056  expnprm  17057  oddprmdvds  17058  prmpwdvds  17059  pockthlem  17060  pockthg  17061  infpnlem1  17065  prmreclem1  17071  prmreclem2  17072  prmreclem3  17073  prmreclem4  17074  prmreclem6  17076  4sqlem6  17098  4sqlem7  17099  4sqlem10  17102  mul4sqlem  17108  4sqlem11  17110  4sqlem12  17111  4sqlem14  17113  4sqlem17  17116  4sqlem18  17117  vdwlem1  17136  vdwlem2  17137  vdwlem3  17138  vdwlem5  17140  vdwlem6  17141  vdwlem8  17143  vdwlem9  17144  vdwlem10  17145  vdwlem12  17147  ramub1lem2  17182  ramcl  17184  prmop1  17193  prmdvdsprmo  17197  prmgaplem7  17212  prmgaplem8  17213  chnub  18773  gsumsgrpccat  19013  mulgnndir  19290  mulgnnass  19296  psgnunilem5  19685  odf1o2  19764  pgp0  19787  sylow1lem1  19789  odcau  19795  sylow2blem3  19813  sylow3lem3  19820  sylow3lem4  19821  gexexlem  20043  ablfacrp2  20260  ablfac1lem  20261  ablfac1eu  20266  pgpfac1lem3a  20269  pgpfac1lem3  20270  fincygsubgodexd  20306  zringlpirlem3  21747  znrrg  21848  psdpw  22468  cpmadugsumlemF  23171  lebnumlem3  25261  ovollb2lem  25786  ovolunlem1a  25794  ovolunlem1  25795  uniioombllem3  25883  uniioombllem4  25884  dyaddisjlem  25893  mbfi1fseqlem3  26015  mbfi1fseqlem4  26016  itgpowd  26347  dgrcolem1  26569  vieta1lem1  26612  vieta1lem2  26613  elqaalem2  26622  elqaalem3  26623  aalioulem1  26638  aaliou3lem2  26649  aaliou3lem8  26651  aaliou3lem6  26654  aaliou3lem9  26656  taylfvallem1  26663  tayl0  26668  taylply2  26674  taylply  26675  dvtaylp  26676  taylthlem1  26679  taylthlem2  26680  pserdvlem2  26734  advlogexp  26962  cxpmul2  26996  cxpeq  27064  rtprmirr  27067  atantayl3  27246  leibpi  27249  log2cnv  27251  log2tlbnd  27252  birthdaylem2  27259  birthdaylem3  27260  amgmlem  27296  amgm  27297  emcllem5  27306  fsumharmonic  27318  zetacvg  27321  dmgmdivn0  27334  lgamgulmlem3  27337  lgamgulmlem4  27338  lgamgulmlem5  27339  lgamgulmlem6  27340  lgamgulm2  27342  lgamcvg2  27361  gamcvg  27362  gamcvg2lem  27365  facgam  27372  wilthlem1  27374  wilthlem2  27375  wilthlem3  27376  wilthimp  27378  basellem1  27387  basellem2  27388  basellem3  27389  basellem4  27390  basellem5  27391  basellem8  27394  vmaprm  27423  sgmval2  27449  0sgm  27450  sgmf  27451  vma1  27472  fsumdvdsdiaglem  27489  dvdsflf1o  27493  muinv  27499  mpodvdsmulf1o  27500  dvdsmulf1o  27502  sgmppw  27503  1sgmprm  27505  1sgm2ppw  27506  sgmmul  27507  chtublem  27517  fsumvma2  27520  chpchtsum  27525  logfaclbnd  27528  logexprlim  27531  mersenne  27533  perfect1  27534  perfectlem1  27535  perfectlem2  27536  perfect  27537  dchrsum2  27574  dchrhash  27577  bcmono  27583  bcp1ctr  27585  bclbnd  27586  bposlem1  27590  bposlem2  27591  bposlem3  27592  bposlem5  27594  bposlem6  27595  lgsval2lem  27613  lgsqrlem2  27653  gausslemma2dlem6  27678  gausslemma2dlem7  27679  gausslemma2d  27680  lgseisenlem1  27681  lgseisenlem4  27684  lgsquadlem1  27686  lgsquadlem2  27687  lgsquadlem3  27688  lgsquad2  27692  m1lgs  27694  2sqlem3  27726  2sqlem4  27727  chebbnd1lem1  27775  chebbnd1  27778  rplogsumlem1  27790  rplogsumlem2  27791  rpvmasumlem  27793  dchrisumlem1  27795  dchrmusum2  27800  dchrvmasumlem1  27801  dchrvmasum2lem  27802  dchrvmasum2if  27803  dchrvmasumlem2  27804  dchrvmasumlem3  27805  dchrvmasumiflem1  27807  dchrisum0flblem1  27814  dchrisum0flblem2  27815  dchrisum0fno1  27817  rpvmasum2  27818  rplogsum  27833  mulogsumlem  27837  mulogsum  27838  mulog2sumlem2  27841  vmalogdivsum2  27844  vmalogdivsum  27845  2vmadivsumlem  27846  logsqvma  27848  selberglem2  27852  selberglem3  27853  selberg  27854  selberg2lem  27856  logdivbnd  27862  selberg3lem1  27863  selberg4lem1  27866  pntrsumo1  27871  pntrsumbnd2  27873  selberg3r  27875  selberg4r  27876  selberg34r  27877  pntsval2  27882  pntrlog2bndlem2  27884  pntrlog2bndlem4  27886  pntrlog2bndlem6  27889  pntpbnd1  27892  pntpbnd2  27893  pntlemg  27904  pntlemn  27906  pntlemf  27911  pnt  27920  padicabvf  27937  ostth2lem2  27940  ostth3  27944  fltabcoprmex  27950  fltaccoprm  27951  fltbccoprm  27952  fltne  27954  flt4lem3  27957  flt4lem5elem  27960  flt4lem5a  27961  flt4lem5b  27962  flt4lem5c  27963  flt4lem5d  27964  flt4lem5e  27965  flt4lem5f  27966  flt4lem6  27967  flt4lem7  27968  nna4b4nsq  27969  flt4  27970  flt4ALT  27971  fltoprm  27974  fusgrhashclwwlkn  30649  eucrct2eupth  30825  nrt2irr  31053  elq2  33382  numdenneg  33385  ltesubnnd  33393  2exple2exp  33404  oexpled  33406  gsummptp1  33597  1arithidomlem2  34047  1arithidom  34048  zringfrac  34065  cos9thpiminplylem1  34393  cos9thpiminplylem2  34394  1smat1  34415  madjusmdetlem2  34439  madjusmdetlem4  34441  qqhnm  34601  oddpwdc  34966  eulerpartlemsv2  34970  eulerpartlems  34972  eulerpartlemsv3  34973  eulerpartlemgc  34974  eulerpartlemv  34976  eulerpartlemgs2  34992  fibp1  35013  ballotlemfc0  35105  ballotlemfcc  35106  signsvtn0  35179  reprpmtf1o  35235  vtscl  35247  hgt750lemb  35265  tgoldbachgt  35272  subfacp1lem1  35910  subfacp1lem5  35915  subfacval2  35918  subfaclim  35919  cvmliftlem2  36017  cvmliftlem7  36022  cvmliftlem10  36025  cvmliftlem11  36026  cvmliftlem13  36027  bcm1nt  36468  bcprod  36469  iprodgam  36473  faclimlem1  36474  faclimlem2  36475  faclim2  36479  nn0prpwlem  37077  nn0prpw  37078  knoppcnlem10  37335  knoppndvlem16  37360  poimirlem1  38504  poimirlem2  38505  poimirlem6  38509  poimirlem7  38510  poimirlem8  38511  poimirlem9  38512  poimirlem10  38513  poimirlem11  38514  poimirlem12  38515  poimirlem13  38516  poimirlem15  38518  poimirlem16  38519  poimirlem17  38520  poimirlem18  38521  poimirlem19  38522  poimirlem20  38523  poimirlem21  38524  poimirlem22  38525  poimirlem23  38526  poimirlem24  38527  poimirlem25  38528  poimirlem26  38529  poimirlem27  38530  poimirlem31  38534  nnproddivdvdsd  43015  lcmfunnnd  43027  lcmineqlem3  43046  lcmineqlem4  43047  lcmineqlem6  43049  lcmineqlem8  43051  lcmineqlem10  43053  lcmineqlem11  43054  lcmineqlem12  43055  lcmineqlem16  43059  lcmineqlem18  43061  lcmineqlem23  43066  dvrelogpow2b  43083  aks4d1p1p2  43085  aks4d1p1  43091  aks4d1p8  43102  primrootsunit1  43112  primrootscoprmpow  43114  posbezout  43115  primrootscoprbij  43117  primrootspoweq0  43121  aks6d1c1p3  43125  aks6d1c1p8  43130  aks6d1c2p2  43134  hashscontpow1  43136  2np3bcnp1  43159  2ap1caineq  43160  sticksstones10  43170  sticksstones12a  43172  sticksstones16  43177  sticksstones22  43183  bcled  43193  bcle2d  43194  aks6d1c7lem1  43195  aks6d1c7  43199  unitscyglem2  43211  unitscyglem4  43213  unitscyglem5  43214  aks5lem8  43216  oddnumth  43333  nicomachus  43334  zaddcom  43493  fltltc  43623  fltnltalem  43624  fltnlta  43625  irrapxlem4  43782  irrapxlem5  43783  pellexlem2  43787  pellexlem6  43791  pell1234qrne0  43810  pell1234qrreccl  43811  pell1234qrmulcl  43812  pell1234qrdich  43818  pell14qrdich  43826  pell1qrge1  43827  pell1qr1  43828  pell14qrgapw  43833  rmxyneg  43877  rmxm1  43891  rmxluc  43893  rmxdbl  43896  jm2.19lem1  43946  jm2.27c  43964  relexpmulnn  44665  relexpmulg  44666  inductionexd  45111  hashnzfzclim  45262  bcccl  45279  bcc0  45280  bccp1k  45281  bccm1k  45282  binomcxplemwb  45288  fsumnncl  46525  mccllem  46550  clim1fr1  46554  sumnnodd  46583  dvsinexp  46862  dvxpaek  46891  dvnxpaek  46893  dvnprodlem2  46898  itgsinexplem1  46905  itgsinexp  46906  stoweidlem1  46952  stoweidlem11  46962  stoweidlem25  46976  stoweidlem26  46977  stoweidlem34  46985  stoweidlem37  46988  stoweidlem38  46989  stoweidlem42  46993  wallispi2lem1  47022  wallispi2  47024  stirlinglem4  47028  stirlinglem5  47029  stirlinglem10  47034  stirlinglem15  47039  dirkertrigeqlem3  47051  dirkertrigeq  47052  dirkercncflem2  47055  dirkercncflem4  47057  fourierdlem11  47069  fourierdlem15  47073  fourierdlem79  47136  fourierdlem83  47140  sqwvfourb  47180  etransclem14  47199  etransclem15  47200  etransclem20  47205  etransclem21  47206  etransclem22  47207  etransclem23  47208  etransclem24  47209  etransclem25  47210  etransclem28  47213  etransclem31  47216  etransclem32  47217  etransclem33  47218  etransclem34  47219  etransclem35  47220  etransclem38  47223  etransclem41  47226  etransclem44  47229  etransclem45  47230  etransclem47  47232  etransclem48  47233  nnfoctbdjlem  47406  deccarry  48322  iccpartgtprec  48443  fmtnoodd  48559  fmtnorec2lem  48568  fmtnorec2  48569  fmtnodvds  48570  goldbachthlem2  48572  fmtnorec3  48574  fmtnorec4  48575  fmtnoprmfac1lem  48590  fmtnoprmfac1  48591  fmtnoprmfac2lem1  48592  fmtnoprmfac2  48593  2pwp1prm  48615  sfprmdvdsmersenne  48629  lighneallem4b  48635  lighneal  48637  proththdlem  48639  proththd  48640  ppivalnnprm  48651  oexpnegALTV  48716  perfectALTVlem1  48760  perfectALTVlem2  48761  perfectALTV  48762  nnpw2pmod  49636  nnolog2flm1  49643  blennn0em1  49644  blengt1fldiv2p1  49646  nn0sumshdiglemB  49673  amgmlemALT  50929