Theorem mulcli 10229

Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
mulcli	⊢ (𝐴 · 𝐵) ∈ ℂ

Proof of Theorem mulcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcl 10204	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 710	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2131  (class class class)co 6805  ℂcc 10118   · cmul 10125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 10182

This theorem depends on definitions:  df-bi 197  df-an 385

This theorem is referenced by:  mul02lem2  10397  addid1  10400  cnegex2  10402  ixi  10840  2mulicn  11439  numma  11741  nummac  11742  9t11e99  11855  9t11e99OLD  11856  decbin2  11867  irec  13150  binom2i  13160  crreczi  13175  3dec  13236  sq10OLD  13237  3decOLD  13239  nn0opthi  13243  faclbnd4lem1  13266  rei  14087  imi  14088  iseraltlem2  14604  bpoly3  14980  bpoly4  14981  3dvdsdec  15248  3dvdsdecOLD  15249  3dvds2dec  15250  3dvds2decOLD  15251  odd2np1  15259  gcdaddmlem  15439  3lcm2e6woprm  15522  6lcm4e12  15523  modxai  15966  mod2xnegi  15969  decexp2  15973  decsplitOLD  15985  karatsuba  15986  karatsubaOLD  15987  sinhalfpilem  24406  ef2pi  24420  ef2kpi  24421  efper  24422  sinperlem  24423  sin2kpi  24426  cos2kpi  24427  sin2pim  24428  cos2pim  24429  sincos4thpi  24456  sincos6thpi  24458  pige3  24460  abssinper  24461  efeq1  24466  logneg  24525  logm1  24526  eflogeq  24539  logimul  24551  logneg2  24552  cxpsqrt  24640  root1eq1  24687  cxpeq  24689  ang180lem1  24730  ang180lem3  24732  ang180lem4  24733  1cubrlem  24759  1cubr  24760  quart1lem  24773  asin1  24812  atanlogsublem  24833  log2ublem2  24865  log2ublem3  24866  log2ub  24867  bclbnd  25196  bposlem8  25207  bposlem9  25208  lgsdir2lem5  25245  2lgsoddprmlem3c  25328  2lgsoddprmlem3d  25329  ax5seglem7  26006  ip0i  27981  ip1ilem  27982  ipasslem10  27995  siilem1  28007  normlem0  28267  normlem1  28268  normlem2  28269  normlem3  28270  normlem5  28272  normlem7  28274  bcseqi  28278  norm-ii-i  28295  normpar2i  28314  polid2i  28315  h1de2i  28713  lnopunilem1  29170  lnophmlem2  29177  dfdec100  29877  dpmul100  29906  dp3mul10  29907  dpmul1000  29908  dpexpp1  29917  dpmul  29922  dpmul4  29923  ballotth  30900  efmul2picn  30975  itgexpif  30985  vtscl  31017  circlemeth  31019  hgt750lem  31030  problem2  31858  problem2OLD  31859  problem4  31861  quad3  31863  logi  31919  heiborlem6  33920  proot1ex  38273  areaquad  38296  coskpi2  40572  cosnegpi  40573  cosknegpi  40575  wallispilem4  40780  dirkerper  40808  dirkertrigeq  40813  dirkercncflem2  40816  fourierdlem57  40875  fourierdlem62  40880  fourierswlem  40942  fmtnorec3  41962  fmtnorec4  41963  lighneallem3  42026  3exp4mod41  42035  41prothprmlem1  42036  zlmodzxzequap  42790  nn0sumshdiglemB  42916  i2linesi  43029