ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulcld GIF version

Theorem mulcld 7955
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
Assertion
Ref Expression
mulcld (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 mulcl 7916 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 411 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  (class class class)co 5868  cc 7787   · cmul 7794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 7887
This theorem is referenced by:  kcnktkm1cn  8317  rereim  8520  cru  8536  apreim  8537  mulreim  8538  apadd1  8542  apneg  8545  mulext1  8546  mulext  8548  aprcl  8580  mulap0  8587  receuap  8602  mul0eqap  8603  divrecap  8621  divcanap3  8631  muldivdirap  8640  divdivdivap  8646  divsubdivap  8661  apmul1  8721  apdivmuld  8746  qapne  9615  cnref1o  9626  mul2lt0rlt0  9733  lincmb01cmp  9977  iccf1o  9978  qbtwnrelemcalc  10229  flqpmodeq  10300  modq0  10302  modqdiffl  10308  modqvalp1  10316  modqcyc  10332  modqcyc2  10333  modqadd1  10334  mulqaddmodid  10337  modqmuladdnn0  10341  qnegmod  10342  modqmul1  10350  mulexpzap  10533  expmulzap  10539  binom2  10604  binom3  10610  bernneq  10613  nn0opthd  10673  bcval5  10714  remullem  10851  cjreim2  10884  cnrecnv  10890  absval  10981  resqrexlemover  10990  resqrexlemcalc1  10994  resqrexlemnm  10998  absimle  11064  abstri  11084  bdtrilem  11218  mulcn2  11291  reccn2ap  11292  climcvg1nlem  11328  isummulc2  11405  fsummulc2  11427  fsumparts  11449  binomlem  11462  binom1dif  11466  trireciplem  11479  mertenslemi1  11514  mertensabs  11516  ntrivcvgap  11527  fprodmul  11570  efaddlem  11653  sinval  11681  cosval  11682  sinadd  11715  cosadd  11716  tanaddaplem  11717  tanaddap  11718  addsin  11721  sincossq  11727  sin2t  11728  cos12dec  11746  eirraplem  11755  dvdscmulr  11798  dvdsmulcr  11799  dvds2ln  11802  oddm1even  11850  divalglemnn  11893  divalglemnqt  11895  flodddiv4  11909  gcdaddm  11955  bezoutlemnewy  11967  bezoutlema  11970  bezoutlemb  11971  lcmgcdlem  12047  oddpwdc  12144  phiprmpw  12192  eulerthlema  12200  pythagtriplem12  12245  pythagtriplem14  12247  pythagtriplem16  12249  pcpremul  12263  pcaddlem  12308  fldivp1  12316  mul4sqlem  12361  oddennn  12363  mulc1cncf  13709  mulcncf  13724  dvmulxxbr  13799  dvimulf  13803  dvexp  13808  dvmptmulx  13815  dvmptcmulcn  13816  sin0pilem1  13835  rpcxpef  13948  rpcncxpcl  13956  cxpap0  13958  rpcxpadd  13959  rpmulcxp  13963  cxpmul  13966  abscxp  13968  rpabscxpbnd  13992  binom4  14030  2sqlem3  14086  qdencn  14398  cvgcmp2nlemabs  14403
  Copyright terms: Public domain W3C validator