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

Theorem mulcld 7047
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 7008 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 391 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  (class class class)co 5512  cc 6887   · cmul 6894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulcl 6982
This theorem is referenced by:  kcnktkm1cn  7380  rereim  7577  cru  7593  apreim  7594  mulreim  7595  apadd1  7599  apneg  7602  mulext1  7603  mulext  7605  mulap0  7635  receuap  7650  divrecap  7667  divcanap3  7675  divdivdivap  7689  divsubdivap  7704  apmul1  7764  qapne  8574  cnref1o  8582  lincmb01cmp  8871  iccf1o  8872  qbtwnrelemcalc  9110  flqpmodeq  9169  modq0  9171  modqdiffl  9177  mulexpzap  9295  expmulzap  9301  binom2  9362  binom3  9366  bernneq  9369  remullem  9471  cjreim2  9504  cnrecnv  9510  absval  9599  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemnm  9616  absimle  9680  abstri  9700  mulcn2  9833  iisermulc2  9860  climcvg1nlem  9868  qdencn  10124
  Copyright terms: Public domain W3C validator