Theorem mulcli 10045

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

Syntax hints:   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934   · cmul 9941

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

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

This theorem is referenced by:  mul02lem2  10213  addid1  10216  cnegex2  10218  ixi  10656  2mulicn  11255  numma  11557  nummac  11558  9t11e99  11671  9t11e99OLD  11672  decbin2  11683  irec  12964  binom2i  12974  crreczi  12989  3dec  13050  sq10OLD  13051  3decOLD  13053  nn0opthi  13057  faclbnd4lem1  13080  rei  13896  imi  13897  iseraltlem2  14413  bpoly3  14789  bpoly4  14790  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  odd2np1  15065  gcdaddmlem  15245  3lcm2e6woprm  15328  6lcm4e12  15329  modxai  15772  mod2xnegi  15775  decexp2  15779  decsplitOLD  15791  karatsuba  15792  karatsubaOLD  15793  sinhalfpilem  24215  ef2pi  24229  ef2kpi  24230  efper  24231  sinperlem  24232  sin2kpi  24235  cos2kpi  24236  sin2pim  24237  cos2pim  24238  sincos4thpi  24265  sincos6thpi  24267  pige3  24269  abssinper  24270  efeq1  24275  logneg  24334  logm1  24335  eflogeq  24348  logimul  24360  logneg2  24361  cxpsqrt  24449  root1eq1  24496  cxpeq  24498  ang180lem1  24539  ang180lem3  24541  ang180lem4  24542  1cubrlem  24568  1cubr  24569  quart1lem  24582  asin1  24621  atanlogsublem  24642  log2ublem2  24674  log2ublem3  24675  log2ub  24676  bclbnd  25005  bposlem8  25016  bposlem9  25017  lgsdir2lem5  25054  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  ax5seglem7  25815  ip0i  27680  ip1ilem  27681  ipasslem10  27694  siilem1  27706  normlem0  27966  normlem1  27967  normlem2  27968  normlem3  27969  normlem5  27971  normlem7  27973  bcseqi  27977  norm-ii-i  27994  normpar2i  28013  polid2i  28014  h1de2i  28412  lnopunilem1  28869  lnophmlem2  28876  dfdec100  29576  dpmul100  29605  dp3mul10  29606  dpmul1000  29607  dpexpp1  29616  dpmul  29621  dpmul4  29622  ballotth  30599  efmul2picn  30674  itgexpif  30684  vtscl  30716  circlemeth  30718  hgt750lem  30729  problem2  31559  problem2OLD  31560  problem4  31562  quad3  31564  logi  31620  heiborlem6  33615  proot1ex  37779  areaquad  37802  coskpi2  40077  cosnegpi  40078  cosknegpi  40080  wallispilem4  40285  dirkerper  40313  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem57  40380  fourierdlem62  40385  fourierswlem  40447  fmtnorec3  41460  fmtnorec4  41461  lighneallem3  41524  3exp4mod41  41533  41prothprmlem1  41534  zlmodzxzequap  42288  nn0sumshdiglemB  42414  i2linesi  42524