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

Theorem mulcli 8090
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
Assertion
Ref Expression
mulcli  |-  ( A  x.  B )  e.  CC

Proof of Theorem mulcli
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 mulcl 8065 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 426 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 2177  (class class class)co 5954   CCcc 7936    x. cmul 7943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8036
This theorem is referenced by:  ixi  8669  2mulicn  9272  numma  9560  nummac  9561  9t11e99  9646  decbin2  9657  irec  10797  binom2i  10806  3dec  10872  rei  11260  imi  11261  3dvdsdec  12226  3dvds2dec  12227  odd2np1  12234  3lcm2e6woprm  12458  6lcm4e12  12459  modxai  12789  karatsuba  12803  sinhalfpilem  15313  ef2pi  15327  ef2kpi  15328  efper  15329  sinperlem  15330  sin2kpi  15333  cos2kpi  15334  sin2pim  15335  cos2pim  15336  sincos4thpi  15362  sincos6thpi  15364  abssinper  15368  cosq34lt1  15372  lgsdir2lem5  15559  2lgsoddprmlem3c  15636  2lgsoddprmlem3d  15637
  Copyright terms: Public domain W3C validator