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

Theorem mulcld 7710
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 7671 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3syl2anc 406 1 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1463  (class class class)co 5728  cc 7545   · cmul 7552
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107  ax-mulcl 7643
This theorem is referenced by:  kcnktkm1cn  8064  rereim  8266  cru  8282  apreim  8283  mulreim  8284  apadd1  8288  apneg  8291  mulext1  8292  mulext  8294  mulap0  8328  receuap  8343  mul0eqap  8344  divrecap  8361  divcanap3  8371  muldivdirap  8380  divdivdivap  8386  divsubdivap  8401  apmul1  8461  apdivmuld  8486  qapne  9333  cnref1o  9342  lincmb01cmp  9679  iccf1o  9680  qbtwnrelemcalc  9926  flqpmodeq  9993  modq0  9995  modqdiffl  10001  modqvalp1  10009  modqcyc  10025  modqcyc2  10026  modqadd1  10027  mulqaddmodid  10030  modqmuladdnn0  10034  qnegmod  10035  modqmul1  10043  mulexpzap  10226  expmulzap  10232  binom2  10296  binom3  10302  bernneq  10305  nn0opthd  10361  bcval5  10402  remullem  10536  cjreim2  10569  cnrecnv  10575  absval  10665  resqrexlemover  10674  resqrexlemcalc1  10678  resqrexlemnm  10682  absimle  10748  abstri  10768  bdtrilem  10902  mulcn2  10973  reccn2ap  10974  climcvg1nlem  11010  isummulc2  11087  fsummulc2  11109  fsumparts  11131  binomlem  11144  binom1dif  11148  trireciplem  11161  mertenslemi1  11196  mertensabs  11198  efaddlem  11231  sinval  11260  cosval  11261  sinadd  11294  cosadd  11295  tanaddaplem  11296  tanaddap  11297  addsin  11300  sincossq  11306  sin2t  11307  eirraplem  11331  dvdscmulr  11370  dvdsmulcr  11371  dvds2ln  11374  oddm1even  11420  divalglemnn  11463  divalglemnqt  11465  flodddiv4  11479  gcdaddm  11520  bezoutlemnewy  11530  bezoutlema  11533  bezoutlemb  11534  lcmgcdlem  11604  oddpwdc  11697  phiprmpw  11743  oddennn  11750  mulc1cncf  12562  mulcncf  12577  dvmulxxbr  12621  dvimulf  12625  qdencn  12914  cvgcmp2nlemabs  12919
  Copyright terms: Public domain W3C validator