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

Theorem mulcld 7452
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 7413 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  (class class class)co 5613  cc 7292   · cmul 7299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcl 7387
This theorem is referenced by:  kcnktkm1cn  7805  rereim  8004  cru  8020  apreim  8021  mulreim  8022  apadd1  8026  apneg  8029  mulext1  8030  mulext  8032  mulap0  8062  receuap  8077  divrecap  8094  divcanap3  8104  muldivdirap  8113  divdivdivap  8119  divsubdivap  8134  apmul1  8194  qapne  9056  cnref1o  9065  lincmb01cmp  9352  iccf1o  9353  qbtwnrelemcalc  9595  flqpmodeq  9662  modq0  9664  modqdiffl  9670  modqvalp1  9678  modqcyc  9694  modqcyc2  9695  modqadd1  9696  mulqaddmodid  9699  modqmuladdnn0  9703  qnegmod  9704  modqmul1  9712  mulexpzap  9893  expmulzap  9899  binom2  9962  binom3  9967  bernneq  9970  nn0opthd  10026  ibcval5  10067  remullem  10200  cjreim2  10233  cnrecnv  10239  absval  10329  resqrexlemover  10338  resqrexlemcalc1  10342  resqrexlemnm  10346  absimle  10412  abstri  10432  mulcn2  10593  iisermulc2  10620  climcvg1nlem  10628  dvdscmulr  10700  dvdsmulcr  10701  dvds2ln  10704  oddm1even  10750  divalglemnn  10793  divalglemnqt  10795  flodddiv4  10809  gcdaddm  10850  bezoutlemnewy  10860  bezoutlema  10863  bezoutlemb  10864  lcmgcdlem  10934  oddpwdc  11027  phiprmpw  11073  oddennn  11080  qdencn  11353
  Copyright terms: Public domain W3C validator