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

Theorem mulid1 8835
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 8834 . 2  |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
2 recn 8827 . . . . . 6  |-  ( x  e.  RR  ->  x  e.  CC )
3 ax-icn 8796 . . . . . . 7  |-  _i  e.  CC
4 recn 8827 . . . . . . 7  |-  ( y  e.  RR  ->  y  e.  CC )
5 mulcl 8821 . . . . . . 7  |-  ( ( _i  e.  CC  /\  y  e.  CC )  ->  ( _i  x.  y
)  e.  CC )
63, 4, 5sylancr 644 . . . . . 6  |-  ( y  e.  RR  ->  (
_i  x.  y )  e.  CC )
7 ax-1cn 8795 . . . . . . 7  |-  1  e.  CC
8 adddir 8830 . . . . . . 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 1266 . . . . . 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 463 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( ( x  x.  1 )  +  ( ( _i  x.  y )  x.  1 ) ) )
11 ax-1rid 8807 . . . . . 6  |-  ( x  e.  RR  ->  (
x  x.  1 )  =  x )
12 mulass 8825 . . . . . . . . 9  |-  ( ( _i  e.  CC  /\  y  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
133, 7, 12mp3an13 1268 . . . . . . . 8  |-  ( y  e.  CC  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
144, 13syl 15 . . . . . . 7  |-  ( y  e.  RR  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
15 ax-1rid 8807 . . . . . . . 8  |-  ( y  e.  RR  ->  (
y  x.  1 )  =  y )
1615oveq2d 5874 . . . . . . 7  |-  ( y  e.  RR  ->  (
_i  x.  ( y  x.  1 ) )  =  ( _i  x.  y
) )
1714, 16eqtrd 2315 . . . . . 6  |-  ( y  e.  RR  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  y ) )
1811, 17oveqan12d 5877 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  x.  1 )  +  ( ( _i  x.  y
)  x.  1 ) )  =  ( x  +  ( _i  x.  y ) ) )
1910, 18eqtrd 2315 . . . 4  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( x  +  ( _i  x.  y ) ) )
20 oveq1 5865 . . . . 5  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  ( A  x.  1 )  =  ( ( x  +  ( _i  x.  y ) )  x.  1 ) )
21 id 19 . . . . 5  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  A  =  ( x  +  ( _i  x.  y
) ) )
2220, 21eqeq12d 2297 . . . 4  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
( A  x.  1 )  =  A  <->  ( (
x  +  ( _i  x.  y ) )  x.  1 )  =  ( x  +  ( _i  x.  y ) ) ) )
2319, 22syl5ibrcom 213 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( A  =  ( x  +  ( _i  x.  y ) )  ->  ( A  x.  1 )  =  A ) )
2423rexlimivv 2672 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) )  ->  ( A  x.  1 )  =  A )
251, 24syl 15 1  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   E.wrex 2544  (class class class)co 5858   CCcc 8735   RRcr 8736   1c1 8738   _ici 8739    + caddc 8740    x. cmul 8742
This theorem is referenced by:  mulid2  8836  mulid1i  8839  mulid1d  8852  muleqadd  9412  divdiv1  9471  conjmul  9477  nnmulcl  9769  expmul  11147  binom21  11219  sq01  11223  bernneq  11227  hashiun  12280  efexp  12381  cncrng  16395  cnfld1  16399  0dgr  19627  ecxp  20020  dvcxp1  20082  efrlim  20264  lgsdilem2  20570  gxnn0mul  20944  cnrngo  21070  ipasslem2  21410  addltmulALT  23026  axcontlem7  24598  fsumcube  24795  fmul01  27710  fmul01lt1lem1  27714  stoweidlem11  27760  stoweidlem13  27762  stoweidlem16  27765  stoweidlem26  27775  stoweidlem38  27787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulcom 8801  ax-mulass 8803  ax-distr 8804  ax-1rid 8807  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator