Theorem mullid 11131

Description: Identity law for multiplication. See mulrid 11130 for commuted version. (Contributed by NM, 8-Oct-1999.)

Assertion

Ref	Expression
mullid	⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Proof of Theorem mullid

Step	Hyp	Ref	Expression
1		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
2		mulcom 11112	. . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = (𝐴 · 1))
3	1, 2	mpan 690	. 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = (𝐴 · 1))
4		mulrid 11130	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
5	3, 4	eqtrd 2771	1 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092  ax-distr 11093  ax-1rid 11096  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  mullidi  11137  mullidd  11150  muladd11  11303  1p1times  11304  mul02lem1  11309  cnegex2  11315  mulm1  11578  div1  11831  subdivcomb2  11837  recdiv  11847  divdiv2  11853  conjmul  11858  ser1const  13981  expp1  13991  recan  15260  arisum  15783  geo2sum  15796  prodrblem  15852  prodmolem2a  15857  risefac1  15956  fallfac1  15957  bpoly3  15981  bpoly4  15982  sinhval  16079  coshval  16080  demoivreALT  16126  gcdadd  16453  gcdid  16454  cncrng  21343  cncrngOLD  21344  cnfld1  21348  cnfld1OLD  21349  blcvx  24742  icccvx  24904  cnlmod  25096  coeidp  26225  dgrid  26226  quartlem1  26823  asinsinlem  26857  asinsin  26858  atantan  26889  musumsum  27158  brbtwn2  28978  axsegconlem1  28990  ax5seglem1  29001  ax5seglem2  29002  ax5seglem4  29005  ax5seglem5  29006  axeuclid  29036  axcontlem2  29038  axcontlem4  29040  cncvcOLD  30658  dvcosax  46166