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

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

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 6982 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  (class class class)co 5512  cc 6887   · cmul 6894
This theorem was proved from axioms:  ax-mulcl 6982
This theorem is referenced by:  0cn  7019  mulid1  7024  mulcli  7032  mulcld  7047  mul31  7144  mul4  7145  cnegexlem2  7187  cnegex  7189  muladd  7381  subdi  7382  mul02  7384  submul2  7396  mulsub  7398  recextlem1  7632  recexap  7634  muleqadd  7649  divassap  7669  divmuldivap  7688  divmuleqap  7693  divadddivap  7703  conjmulap  7705  cju  7913  zneo  8339  expivallem  9256  expival  9257  exp1  9261  expp1  9262  expcl  9273  expclzaplem  9279  mulexp  9294  sqcl  9315  subsq  9358  subsq2  9359  binom2sub  9364  binom3  9366  zesq  9367  bernneq  9369  bernneq2  9370  reim  9452  imcl  9454  crre  9457  crim  9458  remim  9460  mulreap  9464  cjreb  9466  recj  9467  reneg  9468  readd  9469  remullem  9471  remul2  9473  imcj  9475  imneg  9476  imadd  9477  immul2  9480  cjadd  9484  ipcnval  9486  cjmulrcl  9487  cjneg  9490  imval2  9494  cjreim  9503  rennim  9600  sqabsadd  9653  sqabssub  9654  absreimsq  9665  absreim  9666  absmul  9667  mulcn2  9833  climmul  9847  iisermulc2  9860
  Copyright terms: Public domain W3C validator