Theorem mulcli 11297

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 11268	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mul02lem2  11467  addrid  11470  cnegex2  11472  ixi  11919  2mulicn  12516  numma  12802  nummac  12803  9t11e99  12888  decbin2  12899  irec  14250  binom2i  14261  crreczi  14277  3dec  14315  nn0opthi  14319  faclbnd4lem1  14342  rei  15205  imi  15206  iseraltlem2  15731  bpoly3  16106  bpoly4  16107  3dvdsdec  16380  3dvds2dec  16381  odd2np1  16389  gcdaddmlem  16570  3lcm2e6woprm  16662  6lcm4e12  16663  modxai  17115  mod2xnegi  17118  decexp2  17122  karatsuba  17131  sinhalfpilem  26523  ef2pi  26537  ef2kpi  26538  efper  26539  sinperlem  26540  sin2kpi  26543  cos2kpi  26544  sin2pim  26545  cos2pim  26546  sincos4thpi  26573  sincos6thpi  26576  pige3ALT  26580  abssinper  26581  efeq1  26588  logi  26647  logneg  26648  logm1  26649  eflogeq  26662  logimul  26674  logneg2  26675  cxpsqrt  26763  root1eq1  26816  cxpeq  26818  ang180lem1  26870  ang180lem3  26872  ang180lem4  26873  1cubrlem  26902  1cubr  26903  quart1lem  26916  asin1  26955  atanlogsublem  26976  log2ublem2  27008  log2ublem3  27009  log2ub  27010  bclbnd  27342  bposlem8  27353  bposlem9  27354  lgsdir2lem5  27391  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  ax5seglem7  28968  ip0i  30857  ip1ilem  30858  ipasslem10  30871  siilem1  30883  normlem0  31141  normlem1  31142  normlem2  31143  normlem3  31144  normlem5  31146  normlem7  31148  bcseqi  31152  norm-ii-i  31169  normpar2i  31188  polid2i  31189  h1de2i  31585  lnopunilem1  32042  lnophmlem2  32049  dfdec100  32834  dpmul100  32861  dp3mul10  32862  dpmul1000  32863  dpexpp1  32872  dpmul  32877  dpmul4  32878  ballotth  34502  efmul2picn  34573  itgexpif  34583  vtscl  34615  circlemeth  34617  hgt750lem  34628  problem2  35634  problem4  35636  quad3  35638  heiborlem6  37776  gcdaddmzz2nncomi  41952  sn-1ne2  42254  sqsumi  42270  sqmid3api  42272  sqdeccom12  42278  cxp112d  42329  cxp111d  42330  cxpi11d  42331  re1m1e0m0  42373  reixi  42398  sn-1ticom  42410  sn-0tie0  42415  sn-inelr  42443  proot1ex  43157  areaquad  43177  resqrtvalex  43607  imsqrtvalex  43608  coskpi2  45787  cosnegpi  45788  cosknegpi  45790  wallispilem4  45989  dirkerper  46017  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem57  46084  fourierdlem62  46089  fourierswlem  46151  fmtnorec3  47422  fmtnorec4  47423  lighneallem3  47481  3exp4mod41  47490  41prothprmlem1  47491  zlmodzxzequap  48228  nn0sumshdiglemB  48354  i2linesi  48872