Theorem mulcli 11187

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072   · cmul 11079

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

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

This theorem is referenced by:  mul02lem2  11357  addrid  11360  cnegex2  11362  ixi  11813  2mulicn  12412  numma  12699  nummac  12700  9t11e99  12785  decbin2  12796  irec  14172  binom2i  14183  crreczi  14199  3dec  14237  nn0opthi  14241  faclbnd4lem1  14264  rei  15128  imi  15129  iseraltlem2  15655  bpoly3  16030  bpoly4  16031  3dvdsdec  16308  3dvds2dec  16309  odd2np1  16317  gcdaddmlem  16500  3lcm2e6woprm  16591  6lcm4e12  16592  modxai  17045  mod2xnegi  17048  karatsuba  17060  sinhalfpilem  26378  ef2pi  26392  ef2kpi  26393  efper  26394  sinperlem  26395  sin2kpi  26398  cos2kpi  26399  sin2pim  26400  cos2pim  26401  sincos4thpi  26428  sincos6thpi  26431  pige3ALT  26435  abssinper  26436  efeq1  26443  logi  26502  logneg  26503  logm1  26504  eflogeq  26517  logimul  26529  logneg2  26530  cxpsqrt  26618  root1eq1  26671  cxpeq  26673  ang180lem1  26725  ang180lem3  26727  ang180lem4  26728  1cubrlem  26757  1cubr  26758  quart1lem  26771  asin1  26810  atanlogsublem  26831  log2ublem2  26863  log2ublem3  26864  log2ub  26865  bclbnd  27197  bposlem8  27208  bposlem9  27209  lgsdir2lem5  27246  2lgsoddprmlem3c  27329  2lgsoddprmlem3d  27330  ax5seglem7  28868  ip0i  30760  ip1ilem  30761  ipasslem10  30774  siilem1  30786  normlem0  31044  normlem1  31045  normlem2  31046  normlem3  31047  normlem5  31049  normlem7  31051  bcseqi  31055  norm-ii-i  31072  normpar2i  31091  polid2i  31092  h1de2i  31488  lnopunilem1  31945  lnophmlem2  31952  dfdec100  32761  dpmul100  32823  dp3mul10  32824  dpmul1000  32825  dpexpp1  32834  dpmul  32839  dpmul4  32840  cos9thpiminplylem4  33781  cos9thpiminplylem5  33782  ballotth  34535  efmul2picn  34593  itgexpif  34603  vtscl  34635  circlemeth  34637  hgt750lem  34648  problem2  35653  problem4  35655  quad3  35657  heiborlem6  37805  gcdaddmzz2nncomi  41978  sn-1ne2  42248  sqsumi  42264  sqmid3api  42266  sqdeccom12  42272  cxp112d  42324  cxp111d  42325  cxpi11d  42326  re1m1e0m0  42380  reixi  42406  sn-1ticom  42418  sn-0tie0  42434  sn-inelr  42468  proot1ex  43178  areaquad  43198  resqrtvalex  43627  imsqrtvalex  43628  coskpi2  45857  cosnegpi  45858  cosknegpi  45860  wallispilem4  46059  dirkerper  46087  dirkertrigeq  46092  dirkercncflem2  46095  fourierdlem57  46154  fourierdlem62  46159  fourierswlem  46221  fmtnorec3  47539  fmtnorec4  47540  lighneallem3  47598  3exp4mod41  47607  41prothprmlem1  47608  zlmodzxzequap  48478  nn0sumshdiglemB  48599  i2linesi  49757