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

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

Proof of Theorem mulcl
StepHypRef Expression
1 ax-mulcl 7040 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wcel 1409  (class class class)co 5540  cc 6945   · cmul 6952
This theorem was proved from axioms:  ax-mulcl 7040
This theorem is referenced by:  0cn  7077  mulid1  7082  mulcli  7090  mulcld  7105  mul31  7205  mul4  7206  muladd11r  7230  cnegexlem2  7250  cnegex  7252  muladd  7453  subdi  7454  mul02  7456  submul2  7468  mulsub  7470  recextlem1  7706  recexap  7708  muleqadd  7723  divassap  7743  divmuldivap  7763  divmuleqap  7768  divadddivap  7778  conjmulap  7780  cju  7989  zneo  8398  expivallem  9421  expival  9422  exp1  9426  expp1  9427  expcl  9438  expclzaplem  9444  mulexp  9459  sqcl  9481  subsq  9525  subsq2  9526  binom2sub  9531  mulbinom2  9533  binom3  9534  zesq  9535  bernneq  9537  bernneq2  9538  facnn  9595  fac0  9596  fac1  9597  facp1  9598  ibcval5  9631  bcn2  9632  reim  9680  imcl  9682  crre  9685  crim  9686  remim  9688  mulreap  9692  cjreb  9694  recj  9695  reneg  9696  readd  9697  remullem  9699  remul2  9701  imcj  9703  imneg  9704  imadd  9705  immul2  9708  cjadd  9712  ipcnval  9714  cjmulrcl  9715  cjneg  9718  imval2  9722  cjreim  9731  rennim  9829  sqabsadd  9882  sqabssub  9883  absreimsq  9894  absreim  9895  absmul  9896  mulcn2  10064  climmul  10078  iisermulc2  10091  odd2np1lem  10183  odd2np1  10184  opoe  10207  omoe  10208  opeo  10209  omeo  10210
  Copyright terms: Public domain W3C validator