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

Theorem mulcl 7715
Description: Alias for ax-mulcl 7686, for naming consistency with mulcli 7739. (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 7686 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 1465  (class class class)co 5742   CCcc 7586    x. cmul 7593
This theorem was proved from axioms:  ax-mulcl 7686
This theorem is referenced by:  0cn  7726  mulid1  7731  mulcli  7739  mulcld  7754  mul31  7861  mul4  7862  muladd11r  7886  cnegexlem2  7906  cnegex  7908  muladd  8114  subdi  8115  mul02  8117  submul2  8129  mulsub  8131  recextlem1  8380  recexap  8382  muleqadd  8397  divassap  8418  divmulassap  8423  divmuldivap  8440  divmuleqap  8445  divadddivap  8455  conjmulap  8457  cju  8687  zneo  9120  exp3vallem  10262  exp3val  10263  exp1  10267  expp1  10268  expcl  10279  expclzaplem  10285  mulexp  10300  sqcl  10322  subsq  10367  subsq2  10368  binom2sub  10373  mulbinom2  10376  binom3  10377  zesq  10378  bernneq  10380  bernneq2  10381  facnn  10441  fac0  10442  fac1  10443  facp1  10444  bcval5  10477  bcn2  10478  reim  10592  imcl  10594  crre  10597  crim  10598  remim  10600  mulreap  10604  cjreb  10606  recj  10607  reneg  10608  readd  10609  remullem  10611  remul2  10613  imcj  10615  imneg  10616  imadd  10617  immul2  10620  cjadd  10624  ipcnval  10626  cjmulrcl  10627  cjneg  10630  imval2  10634  cjreim  10643  rennim  10742  sqabsadd  10795  sqabssub  10796  absreimsq  10807  absreim  10808  absmul  10809  mul0inf  10980  mulcn2  11049  climmul  11064  isermulc2  11077  fsummulc2  11185  efexp  11315  sinf  11338  cosf  11339  tanval2ap  11347  tanval3ap  11348  resinval  11349  recosval  11350  efi4p  11351  resin4p  11352  recos4p  11353  resincl  11354  recoscl  11355  sinneg  11360  cosneg  11361  efival  11366  efmival  11367  efeul  11368  sinadd  11370  cosadd  11371  sinsub  11374  cossub  11375  subsin  11377  sinmul  11378  cosmul  11379  addcos  11380  subcos  11381  cos2tsin  11385  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  absef  11403  absefib  11404  efieq1re  11405  demoivre  11406  demoivreALT  11407  odd2np1lem  11496  odd2np1  11497  opoe  11519  omoe  11520  opeo  11521  omeo  11522  modgcd  11606  qredeq  11704  mulc1cncf  12672  mulcncflem  12686  dvmulxxbr  12762  dvmulxx  12764  dvimulf  12766  efper  12815  sinperlem  12816  sin2kpi  12819  cos2kpi  12820  efimpi  12827  sincosq1eq  12847  abssinper  12854  sinkpi  12855  coskpi  12856
  Copyright terms: Public domain W3C validator