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

Theorem mulcl 7448
Description: Alias for ax-mulcl 7422, for naming consistency with mulcli 7472. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 7422 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  (class class class)co 5634  cc 7327   · cmul 7334
This theorem was proved from axioms:  ax-mulcl 7422
This theorem is referenced by:  0cn  7459  mulid1  7464  mulcli  7472  mulcld  7487  mul31  7592  mul4  7593  muladd11r  7617  cnegexlem2  7637  cnegex  7639  muladd  7841  subdi  7842  mul02  7844  submul2  7856  mulsub  7858  recextlem1  8094  recexap  8096  muleqadd  8111  divassap  8131  divmulassap  8136  divmuldivap  8153  divmuleqap  8158  divadddivap  8168  conjmulap  8170  cju  8393  zneo  8817  exp3vallem  9921  exp3val  9922  exp1  9926  expp1  9927  expcl  9938  expclzaplem  9944  mulexp  9959  sqcl  9981  subsq  10026  subsq2  10027  binom2sub  10032  mulbinom2  10035  binom3  10036  zesq  10037  bernneq  10039  bernneq2  10040  facnn  10100  fac0  10101  fac1  10102  facp1  10103  ibcval5  10136  bcn2  10137  reim  10251  imcl  10253  crre  10256  crim  10257  remim  10259  mulreap  10263  cjreb  10265  recj  10266  reneg  10267  readd  10268  remullem  10270  remul2  10272  imcj  10274  imneg  10275  imadd  10276  immul2  10279  cjadd  10283  ipcnval  10285  cjmulrcl  10286  cjneg  10289  imval2  10293  cjreim  10302  rennim  10400  sqabsadd  10453  sqabssub  10454  absreimsq  10465  absreim  10466  absmul  10467  mulcn2  10665  climmul  10679  iisermulc2  10692  fsummulc2  10805  odd2np1lem  10965  odd2np1  10966  opoe  10988  omoe  10989  opeo  10990  omeo  10991  modgcd  11075  qredeq  11171
  Copyright terms: Public domain W3C validator