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

Theorem mulcld 7754
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 7715 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 408 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1465  (class class class)co 5742  cc 7586   · cmul 7593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7686
This theorem is referenced by:  kcnktkm1cn  8113  rereim  8316  cru  8332  apreim  8333  mulreim  8334  apadd1  8338  apneg  8341  mulext1  8342  mulext  8344  aprcl  8376  mulap0  8383  receuap  8398  mul0eqap  8399  divrecap  8416  divcanap3  8426  muldivdirap  8435  divdivdivap  8441  divsubdivap  8456  apmul1  8516  apdivmuld  8541  qapne  9399  cnref1o  9408  mul2lt0rlt0  9514  lincmb01cmp  9754  iccf1o  9755  qbtwnrelemcalc  10001  flqpmodeq  10068  modq0  10070  modqdiffl  10076  modqvalp1  10084  modqcyc  10100  modqcyc2  10101  modqadd1  10102  mulqaddmodid  10105  modqmuladdnn0  10109  qnegmod  10110  modqmul1  10118  mulexpzap  10301  expmulzap  10307  binom2  10371  binom3  10377  bernneq  10380  nn0opthd  10436  bcval5  10477  remullem  10611  cjreim2  10644  cnrecnv  10650  absval  10741  resqrexlemover  10750  resqrexlemcalc1  10754  resqrexlemnm  10758  absimle  10824  abstri  10844  bdtrilem  10978  mulcn2  11049  reccn2ap  11050  climcvg1nlem  11086  isummulc2  11163  fsummulc2  11185  fsumparts  11207  binomlem  11220  binom1dif  11224  trireciplem  11237  mertenslemi1  11272  mertensabs  11274  efaddlem  11307  sinval  11336  cosval  11337  sinadd  11370  cosadd  11371  tanaddaplem  11372  tanaddap  11373  addsin  11376  sincossq  11382  sin2t  11383  cos12dec  11401  eirraplem  11410  dvdscmulr  11449  dvdsmulcr  11450  dvds2ln  11453  oddm1even  11499  divalglemnn  11542  divalglemnqt  11544  flodddiv4  11558  gcdaddm  11599  bezoutlemnewy  11611  bezoutlema  11614  bezoutlemb  11615  lcmgcdlem  11685  oddpwdc  11779  phiprmpw  11825  oddennn  11832  mulc1cncf  12672  mulcncf  12687  dvmulxxbr  12762  dvimulf  12766  dvexp  12771  dvmptmulx  12778  dvmptcmulcn  12779  sin0pilem1  12789  qdencn  13149  cvgcmp2nlemabs  13154
  Copyright terms: Public domain W3C validator