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

Theorem mulcl 7754
Description: Alias for ax-mulcl 7725, for naming consistency with mulcli 7778. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 7725 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1480  (class class class)co 5774   CCcc 7625    x. cmul 7632
This theorem was proved from axioms:  ax-mulcl 7725
This theorem is referenced by:  0cn  7765  mulid1  7770  mulcli  7778  mulcld  7793  mul31  7900  mul4  7901  muladd11r  7925  cnegexlem2  7945  cnegex  7947  muladd  8153  subdi  8154  mul02  8156  submul2  8168  mulsub  8170  recextlem1  8419  recexap  8421  muleqadd  8436  divassap  8457  divmulassap  8462  divmuldivap  8479  divmuleqap  8484  divadddivap  8494  conjmulap  8496  cju  8726  zneo  9159  exp3vallem  10301  exp3val  10302  exp1  10306  expp1  10307  expcl  10318  expclzaplem  10324  mulexp  10339  sqcl  10361  subsq  10406  subsq2  10407  binom2sub  10412  mulbinom2  10415  binom3  10416  zesq  10417  bernneq  10419  bernneq2  10420  facnn  10480  fac0  10481  fac1  10482  facp1  10483  bcval5  10516  bcn2  10517  reim  10631  imcl  10633  crre  10636  crim  10637  remim  10639  mulreap  10643  cjreb  10645  recj  10646  reneg  10647  readd  10648  remullem  10650  remul2  10652  imcj  10654  imneg  10655  imadd  10656  immul2  10659  cjadd  10663  ipcnval  10665  cjmulrcl  10666  cjneg  10669  imval2  10673  cjreim  10682  rennim  10781  sqabsadd  10834  sqabssub  10835  absreimsq  10846  absreim  10847  absmul  10848  mul0inf  11019  mulcn2  11088  climmul  11103  isermulc2  11116  fsummulc2  11224  prodf  11314  clim2prod  11315  clim2divap  11316  prod3fmul  11317  prodf1  11318  prodfap0  11321  prodfrecap  11322  prodrbdclem  11347  fproddccvg  11348  prodmodclem3  11351  prodmodclem2a  11352  efexp  11395  sinf  11417  cosf  11418  tanval2ap  11426  tanval3ap  11427  resinval  11428  recosval  11429  efi4p  11430  resin4p  11431  recos4p  11432  resincl  11433  recoscl  11434  sinneg  11439  cosneg  11440  efival  11445  efmival  11446  efeul  11447  sinadd  11449  cosadd  11450  sinsub  11453  cossub  11454  subsin  11456  sinmul  11457  cosmul  11458  addcos  11459  subcos  11460  cos2tsin  11464  ef01bndlem  11469  sin01bnd  11470  cos01bnd  11471  absef  11482  absefib  11483  efieq1re  11484  demoivre  11485  demoivreALT  11486  odd2np1lem  11575  odd2np1  11576  opoe  11598  omoe  11599  opeo  11600  omeo  11601  modgcd  11685  qredeq  11783  mulc1cncf  12754  mulcncflem  12768  dvmulxxbr  12844  dvmulxx  12846  dvimulf  12848  efper  12904  sinperlem  12905  sin2kpi  12908  cos2kpi  12909  efimpi  12916  sincosq1eq  12936  abssinper  12943  sinkpi  12944  coskpi  12945
  Copyright terms: Public domain W3C validator