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

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

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 6980 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  (class class class)co 5512  cc 6885   · cmul 6892
This theorem was proved from axioms:  ax-mulcl 6980
This theorem is referenced by:  0cn  7017  mulid1  7022  mulcli  7030  mulcld  7045  mul31  7142  mul4  7143  cnegexlem2  7185  cnegex  7187  muladd  7379  subdi  7380  mul02  7382  submul2  7394  mulsub  7396  recextlem1  7630  recexap  7632  muleqadd  7647  divassap  7667  divmuldivap  7686  divmuleqap  7691  divadddivap  7701  conjmulap  7703  cju  7911  zneo  8337  expivallem  9230  expival  9231  exp1  9235  expp1  9236  expcl  9247  expclzaplem  9253  mulexp  9268  sqcl  9289  subsq  9332  subsq2  9333  binom2sub  9338  binom3  9340  zesq  9341  bernneq  9343  bernneq2  9344  reim  9426  imcl  9428  crre  9431  crim  9432  remim  9434  mulreap  9438  cjreb  9440  recj  9441  reneg  9442  readd  9443  remullem  9445  remul2  9447  imcj  9449  imneg  9450  imadd  9451  immul2  9454  cjadd  9458  ipcnval  9460  cjmulrcl  9461  cjneg  9464  imval2  9468  cjreim  9477  rennim  9574  sqabsadd  9627  sqabssub  9628  absreimsq  9639  absreim  9640  absmul  9641  mulcn2  9806  climmul  9820  iisermulc2  9833
  Copyright terms: Public domain W3C validator