ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulrid Unicode version

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

Proof of Theorem mulrid
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 7982 . 2  |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
2 recn 7973 . . . . . 6  |-  ( x  e.  RR  ->  x  e.  CC )
3 ax-icn 7935 . . . . . . 7  |-  _i  e.  CC
4 recn 7973 . . . . . . 7  |-  ( y  e.  RR  ->  y  e.  CC )
5 mulcl 7967 . . . . . . 7  |-  ( ( _i  e.  CC  /\  y  e.  CC )  ->  ( _i  x.  y
)  e.  CC )
63, 4, 5sylancr 414 . . . . . 6  |-  ( y  e.  RR  ->  (
_i  x.  y )  e.  CC )
7 ax-1cn 7933 . . . . . . 7  |-  1  e.  CC
8 adddir 7977 . . . . . . 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 1337 . . . . . 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 289 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( ( x  x.  1 )  +  ( ( _i  x.  y )  x.  1 ) ) )
11 ax-1rid 7947 . . . . . 6  |-  ( x  e.  RR  ->  (
x  x.  1 )  =  x )
12 mulass 7971 . . . . . . . . 9  |-  ( ( _i  e.  CC  /\  y  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
133, 7, 12mp3an13 1339 . . . . . . . 8  |-  ( y  e.  CC  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
144, 13syl 14 . . . . . . 7  |-  ( y  e.  RR  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  ( y  x.  1 ) ) )
15 ax-1rid 7947 . . . . . . . 8  |-  ( y  e.  RR  ->  (
y  x.  1 )  =  y )
1615oveq2d 5911 . . . . . . 7  |-  ( y  e.  RR  ->  (
_i  x.  ( y  x.  1 ) )  =  ( _i  x.  y
) )
1714, 16eqtrd 2222 . . . . . 6  |-  ( y  e.  RR  ->  (
( _i  x.  y
)  x.  1 )  =  ( _i  x.  y ) )
1811, 17oveqan12d 5914 . . . . 5  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  x.  1 )  +  ( ( _i  x.  y
)  x.  1 ) )  =  ( x  +  ( _i  x.  y ) ) )
1910, 18eqtrd 2222 . . . 4  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( ( x  +  ( _i  x.  y
) )  x.  1 )  =  ( x  +  ( _i  x.  y ) ) )
20 oveq1 5902 . . . . 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 2204 . . . 4  |-  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
( A  x.  1 )  =  A  <->  ( (
x  +  ( _i  x.  y ) )  x.  1 )  =  ( x  +  ( _i  x.  y ) ) ) )
2319, 22syl5ibrcom 157 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( A  =  ( x  +  ( _i  x.  y ) )  ->  ( A  x.  1 )  =  A ) )
2423rexlimivv 2613 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) )  ->  ( A  x.  1 )  =  A )
251, 24syl 14 1  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1364    e. wcel 2160   E.wrex 2469  (class class class)co 5895   CCcc 7838   RRcr 7839   1c1 7841   _ici 7842    + caddc 7843    x. cmul 7845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7932  ax-1cn 7933  ax-icn 7935  ax-addcl 7936  ax-mulcl 7938  ax-mulcom 7941  ax-mulass 7943  ax-distr 7944  ax-1rid 7947  ax-cnre 7951
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5898
This theorem is referenced by:  mullid  7984  mulid1i  7988  mulridd  8003  muleqadd  8654  divdivap1  8709  conjmulap  8715  nnmulcl  8969  expmul  10595  binom21  10663  binom2sub1  10665  bernneq  10671  hashiun  11517  fproddccvg  11611  prodmodclem2a  11615  efexp  11721  cncrng  13869  cnfld1  13872  ecxp  14774  lgsdilem2  14890
  Copyright terms: Public domain W3C validator