Theorem mulcli 11316

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11262

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul02lem2  11487  addrid  11490  cnegex2  11492  ixi  11945  2mulicn  12570  numma  12863  nummac  12864  9t11e99OLD  12950  decbin2  12962  irec  14345  binom2i  14356  crreczi  14372  3dec  14410  nn0opthi  14414  faclbnd4lem1  14437  rei  15323  imi  15324  iseraltlem2  15850  bpoly3  16224  bpoly4  16225  3dvdsdec  16502  3dvds2dec  16503  odd2np1  16511  gcdaddmlem  16696  3lcm2e6woprm  16790  6lcm4e12  16791  modxai  17246  mod2xnegi  17249  karatsuba  17261  2picn  26786  sinhalfpilem  26792  ef2pi  26806  ef2kpi  26807  efper  26808  sinperlem  26809  sin2kpi  26812  cos2kpi  26813  sin2pim  26814  cos2pim  26815  sincos4thpi  26842  sincos6thpi  26844  pige3ALT  26848  abssinper  26849  efeq1  26856  logi  26915  logneg  26916  logm1  26917  eflogeq  26930  logimul  26942  logneg2  26943  cxpsqrt  27031  root1eq1  27083  cxpeq  27085  ang180lem1  27137  ang180lem3  27139  ang180lem4  27140  1cubrlem  27169  1cubr  27170  quart1lem  27183  asin1  27222  atanlogsublem  27243  log2ublem2  27275  log2ublem3  27276  log2ub  27277  bclbnd  27607  bposlem8  27618  bposlem9  27619  lgsdir2lem5  27656  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  ax5seglem7  29513  ip0i  31427  ip1ilem  31428  ipasslem10  31441  siilem1  31453  normlem0  31711  normlem1  31712  normlem2  31713  normlem3  31714  normlem5  31716  normlem7  31718  bcseqi  31722  norm-ii-i  31739  normpar2i  31758  polid2i  31759  h1de2i  32155  lnopunilem1  32612  lnophmlem2  32619  dfdec100  33421  dpmul100  33463  dp3mul10  33464  dpmul1000  33465  dpexpp1  33474  dpmul  33479  dpmul4  33480  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  ballotth  35170  efmul2picn  35225  itgexpif  35235  vtscl  35267  circlemeth  35269  hgt750lem  35280  problem2  36431  problem4  36433  quad3  36435  heiborlem6  38750  gcdaddmzz2nncomi  43045  25or6to4  43256  sn-1ne2  43330  sqsumi  43338  sqmid3api  43340  sqdeccom12  43346  cxp112d  43392  cxp111d  43393  cxpi11d  43394  re1m1e0m0  43448  reixi  43474  sn-1ticom  43486  sn-0tie0  43515  proot1ex  44197  areaquad  44217  resqrtvalex  44644  imsqrtvalex  44645  coskpi2  46875  cosnegpi  46876  cosknegpi  46878  wallispilem4  47077  dirkertrigeq  47110  fourierdlem57  47172  fourierdlem62  47177  fourierswlem  47239  cos5t  47924  goldpolyfactor  47926  goldrasin  47928  goldratmolem3  47933  goldratmolem4  47934  fmtnorec3  48632  fmtnorec4  48633  lighneallem3  48691  3exp4mod41  48700  41prothprmlem1  48701  zlmodzxzequap  49610  nn0sumshdiglemB  49731  i2linesi  50873