Theorem mulid2 10038

Description: Identity law for multiplication. Note: see mulid1 10037 for commuted version. (Contributed by NM, 8-Oct-1999.)

Assertion

Ref	Expression
mulid2	|- ( A e. CC -> ( 1 x. A ) = A )

Proof of Theorem mulid2

Step	Hyp	Ref	Expression
1		ax-1cn 9994	. . 3 |- 1 e. CC
2		mulcom 10022	. . 3 |- ( ( 1 e. CC /\ A e. CC ) -> ( 1 x. A ) = ( A x. 1 ) )
3	1, 2	mpan 706	. 2 |- ( A e. CC -> ( 1 x. A ) = ( A x. 1 ) )
4		mulid1 10037	. 2 |- ( A e. CC -> ( A x. 1 ) = A )
5	3, 4	eqtrd 2656	1 |- ( A e. CC -> ( 1 x. A ) = A )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   1c1 9937   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  mulid2i  10043  mulid2d  10058  muladd11  10206  1p1times  10207  mul02lem1  10212  cnegex2  10218  mulm1  10471  div1  10716  recdiv  10731  divdiv2  10737  conjmul  10742  ser1const  12857  expp1  12867  recan  14076  arisum  14592  geo2sum  14604  prodrblem  14659  prodmolem2a  14664  risefac1  14764  fallfac1  14765  bpoly3  14789  bpoly4  14790  sinhval  14884  coshval  14885  demoivreALT  14931  gcdadd  15247  gcdid  15248  cncrng  19767  cnfld1  19771  cnfldmulg  19778  blcvx  22601  icccvx  22749  cnlmod  22940  coeidp  24019  dgrid  24020  quartlem1  24584  asinsinlem  24618  asinsin  24619  atantan  24650  musumsum  24918  brbtwn2  25785  axsegconlem1  25797  ax5seglem1  25808  ax5seglem2  25809  ax5seglem4  25812  ax5seglem5  25813  axeuclid  25843  axcontlem2  25845  axcontlem4  25847  cncvcOLD  27438  subdivcomb2  31612  dvcosax  40141