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

Theorem mulcld 7253
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
mulcld  |-  ( ph  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 mulcl 7214 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434  (class class class)co 5563   CCcc 7093    x. cmul 7100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulcl 7188
This theorem is referenced by:  kcnktkm1cn  7606  rereim  7805  cru  7821  apreim  7822  mulreim  7823  apadd1  7827  apneg  7830  mulext1  7831  mulext  7833  mulap0  7863  receuap  7878  divrecap  7895  divcanap3  7905  muldivdirap  7914  divdivdivap  7920  divsubdivap  7935  apmul1  7995  qapne  8857  cnref1o  8866  lincmb01cmp  9153  iccf1o  9154  qbtwnrelemcalc  9394  flqpmodeq  9461  modq0  9463  modqdiffl  9469  modqvalp1  9477  modqcyc  9493  modqcyc2  9494  modqadd1  9495  mulqaddmodid  9498  modqmuladdnn0  9502  qnegmod  9503  modqmul1  9511  mulexpzap  9665  expmulzap  9671  binom2  9734  binom3  9739  bernneq  9742  nn0opthd  9798  ibcval5  9839  remullem  9959  cjreim2  9992  cnrecnv  9998  absval  10088  resqrexlemover  10097  resqrexlemcalc1  10101  resqrexlemnm  10105  absimle  10171  abstri  10191  mulcn2  10352  iisermulc2  10379  climcvg1nlem  10387  dvdscmulr  10432  dvdsmulcr  10433  dvds2ln  10436  oddm1even  10482  divalglemnn  10525  divalglemnqt  10527  flodddiv4  10541  gcdaddm  10582  bezoutlemnewy  10592  bezoutlema  10595  bezoutlemb  10596  lcmgcdlem  10666  oddpwdc  10759  phiprmpw  10805  oddennn  10812  qdencn  11052
  Copyright terms: Public domain W3C validator