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

Theorem mulcld 7028
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 6989 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 391 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  (class class class)co 5499  cc 6868   · cmul 6875
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcl 6963
This theorem is referenced by:  kcnktkm1cn  7359  rereim  7553  cru  7569  apreim  7570  mulreim  7571  apadd1  7575  apneg  7578  mulext1  7579  mulext  7581  mulap0  7611  receuap  7626  divrecap  7643  divcanap3  7651  divdivdivap  7665  divsubdivap  7680  apmul1  7740  qapne  8546  cnref1o  8553  lincmb01cmp  8838  iccf1o  8839  mulexpzap  9173  expmulzap  9179  binom2  9240  binom3  9244  bernneq  9247  remullem  9349  cjreim2  9382  cnrecnv  9388  absval  9477  resqrexlemover  9486  resqrexlemcalc1  9490  resqrexlemnm  9494  absimle  9558  abstri  9578  mulcn2  9710  iisermulc2  9737  climcvg1nlem  9745
  Copyright terms: Public domain W3C validator