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

Theorem mulcld 7793
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 7754 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3syl2anc 408 1  |-  ( ph  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480  (class class class)co 5774   CCcc 7625    x. cmul 7632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulcl 7725
This theorem is referenced by:  kcnktkm1cn  8152  rereim  8355  cru  8371  apreim  8372  mulreim  8373  apadd1  8377  apneg  8380  mulext1  8381  mulext  8383  aprcl  8415  mulap0  8422  receuap  8437  mul0eqap  8438  divrecap  8455  divcanap3  8465  muldivdirap  8474  divdivdivap  8480  divsubdivap  8495  apmul1  8555  apdivmuld  8580  qapne  9438  cnref1o  9447  mul2lt0rlt0  9553  lincmb01cmp  9793  iccf1o  9794  qbtwnrelemcalc  10040  flqpmodeq  10107  modq0  10109  modqdiffl  10115  modqvalp1  10123  modqcyc  10139  modqcyc2  10140  modqadd1  10141  mulqaddmodid  10144  modqmuladdnn0  10148  qnegmod  10149  modqmul1  10157  mulexpzap  10340  expmulzap  10346  binom2  10410  binom3  10416  bernneq  10419  nn0opthd  10475  bcval5  10516  remullem  10650  cjreim2  10683  cnrecnv  10689  absval  10780  resqrexlemover  10789  resqrexlemcalc1  10793  resqrexlemnm  10797  absimle  10863  abstri  10883  bdtrilem  11017  mulcn2  11088  reccn2ap  11089  climcvg1nlem  11125  isummulc2  11202  fsummulc2  11224  fsumparts  11246  binomlem  11259  binom1dif  11263  trireciplem  11276  mertenslemi1  11311  mertensabs  11313  ntrivcvgap  11324  efaddlem  11387  sinval  11415  cosval  11416  sinadd  11449  cosadd  11450  tanaddaplem  11451  tanaddap  11452  addsin  11455  sincossq  11461  sin2t  11462  cos12dec  11480  eirraplem  11489  dvdscmulr  11528  dvdsmulcr  11529  dvds2ln  11532  oddm1even  11578  divalglemnn  11621  divalglemnqt  11623  flodddiv4  11637  gcdaddm  11678  bezoutlemnewy  11690  bezoutlema  11693  bezoutlemb  11694  lcmgcdlem  11764  oddpwdc  11858  phiprmpw  11904  oddennn  11911  mulc1cncf  12754  mulcncf  12769  dvmulxxbr  12844  dvimulf  12848  dvexp  12853  dvmptmulx  12860  dvmptcmulcn  12861  sin0pilem1  12878  qdencn  13275  cvgcmp2nlemabs  13280
  Copyright terms: Public domain W3C validator