MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulid1 Unicode version

Theorem mulid1 8711
Description:  1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
mulid1  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )

Proof of Theorem mulid1
StepHypRef Expression
1 ax-cnre 8687 . 2  |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
2 recn 8704 . . . . . 6  |-  ( x  e.  RR  ->  x  e.  CC )
3 ax-icn 8673 . . . . . . 7  |-  _i  e.  CC
4 recn 8704 . . . . . . 7  |-  ( y  e.  RR  ->  y  e.  CC )
5 mulcl 8698 . . . . . . 7  |-  ( ( _i  e.  CC  /\  y  e.  CC )  ->  ( _i  x.  y
)  e.  CC )
63, 4, 5sylancr 647 . . . . . 6  |-  ( y  e.  RR  ->  (
_i  x.  y )  e.  CC )
7 ax-1cn 8672 . . . . . . 7  |-  1  e.  CC
8 adddir 8707 . . . . . . 7  |-  ( ( x  e.  CC  /\  ( _i  x.  y
)  e.  CC  /\  1  e.  CC )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( ( x  x.  1 )  +  ( ( _i  x.  y )  x.  1 ) ) )
97, 8mp3an3 1271 . . . . . 6  |-  ( ( x  e.  CC  /\  ( _i  x.  y
)  e.  CC )  ->  ( ( x  +  ( _i  x.  y ) )  x.  1 )  =  ( ( x  x.  1 )  +  ( ( _i  x.  y )  x.  1 ) ) )
102, 6, 9syl2an 465 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( ( x  x.  1 )  +  ( ( _i  x.  y )  x.  1 ) ) )
11 ax-1rid 8684 . . . . . 6  |-  ( x  e.  RR  ->  (
x  x.  1 )  =  x )
12 mulass 8702 . . . . . . . . 9  |-  ( ( _i  e.  CC  /\  y  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
133, 7, 12mp3an13 1273 . . . . . . . 8  |-  ( y  e.  CC  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
144, 13syl 17 . . . . . . 7  |-  ( y  e.  RR  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
15 ax-1rid 8684 . . . . . . . 8  |-  ( y  e.  RR  ->  (
y  x.  1 )  =  y )
1615oveq2d 5723 . . . . . . 7  |-  ( y  e.  RR  ->  (
_i  x.  ( y  x.  1 ) )  =  ( _i  x.  y
) )
1714, 16eqtrd 2285 . . . . . 6  |-  ( y  e.  RR  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  y ) )
1811, 17oveqan12d 5726 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  x.  1 )  +  ( ( _i  x.  y
)  x.  1 ) )  =  ( x  +  ( _i  x.  y ) ) )
1910, 18eqtrd 2285 . . . 4  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( x  +  ( _i  x.  y ) ) )
20 oveq1 5714 . . . . 5  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  ( A  x.  1 )  =  ( ( x  +  ( _i  x.  y ) )  x.  1 ) )
21 id 21 . . . . 5  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  A  =  ( x  +  ( _i  x.  y
) ) )
2220, 21eqeq12d 2267 . . . 4  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
( A  x.  1 )  =  A  <->  ( (
x  +  ( _i  x.  y ) )  x.  1 )  =  ( x  +  ( _i  x.  y ) ) ) )
2319, 22syl5ibrcom 215 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( A  =  ( x  +  ( _i  x.  y ) )  ->  ( A  x.  1 )  =  A ) )
2423rexlimivv 2632 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) )  ->  ( A  x.  1 )  =  A )
251, 24syl 17 1  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   E.wrex 2508  (class class class)co 5707   CCcc 8612   RRcr 8613   1c1 8615   _ici 8616    + caddc 8617    x. cmul 8619
This theorem is referenced by:  mulid2  8712  mulid1i  8716  mulid1d  8729  muleqadd  9270  divdiv1  9327  conjmul  9333  nnmulcl  9617  expmul  10990  binom21  11061  sq01  11065  bernneq  11069  hashiun  12119  efexp  12217  cncrng  16189  cnfld1  16193  0dgr  19421  ecxp  19822  dvcxp1  19884  efrlim  20030  lgsdilem2  20336  gxnn0mul  20703  cnrngo  20829  ipasslem2  21169  addltmulALT  22785  axcontlem7  23701  fsumcube  23898
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-resscn 8671  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-mulcl 8676  ax-mulcom 8678  ax-mulass 8680  ax-distr 8681  ax-1rid 8684  ax-cnre 8687
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-xp 4591  df-cnv 4593  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fv 4605  df-ov 5710
  Copyright terms: Public domain W3C validator