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

Theorem xmulass 11362
Description: Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 11324 which has to avoid the "undefined" combinations +oo +e -oo and -oo +e +oo. The equivalent "undefined" expression here would be  0 xe +oo, but since this is defined to equal  0 any zeroes in the expression make the whole thing evaluate to zero (on both sides), thus establishing the identity in this case. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xmulass  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( A xe B ) xe C )  =  ( A xe ( B xe C ) ) )

Proof of Theorem xmulass
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6208 . . . 4  |-  ( x  =  A  ->  (
x xe B )  =  ( A xe B ) )
21oveq1d 6216 . . 3  |-  ( x  =  A  ->  (
( x xe B ) xe C )  =  ( ( A xe B ) xe C ) )
3 oveq1 6208 . . 3  |-  ( x  =  A  ->  (
x xe ( B xe C ) )  =  ( A xe ( B xe C ) ) )
42, 3eqeq12d 2476 . 2  |-  ( x  =  A  ->  (
( ( x xe B ) xe C )  =  ( x xe ( B xe C ) )  <->  ( ( A xe B ) xe C )  =  ( A xe ( B xe C ) ) ) )
5 oveq1 6208 . . . 4  |-  ( x  =  -e A  ->  ( x xe B )  =  (  -e A xe B ) )
65oveq1d 6216 . . 3  |-  ( x  =  -e A  ->  ( ( x xe B ) xe C )  =  ( (  -e A xe B ) xe C ) )
7 oveq1 6208 . . 3  |-  ( x  =  -e A  ->  ( x xe ( B xe C ) )  =  (  -e
A xe ( B xe C ) ) )
86, 7eqeq12d 2476 . 2  |-  ( x  =  -e A  ->  ( ( ( x xe B ) xe C )  =  ( x xe ( B xe C ) )  <->  ( (  -e A xe B ) xe C )  =  ( 
-e A xe ( B xe C ) ) ) )
9 xmulcl 11348 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A xe B )  e.  RR* )
1093adant3 1008 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  ( A xe B )  e.  RR* )
11 simp3 990 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  C  e.  RR* )
12 xmulcl 11348 . . 3  |-  ( ( ( A xe B )  e.  RR*  /\  C  e.  RR* )  ->  ( ( A xe B ) xe C )  e. 
RR* )
1310, 11, 12syl2anc 661 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( A xe B ) xe C )  e.  RR* )
14 simp1 988 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  A  e.  RR* )
15 xmulcl 11348 . . . 4  |-  ( ( B  e.  RR*  /\  C  e.  RR* )  ->  ( B xe C )  e.  RR* )
16153adant1 1006 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  ( B xe C )  e.  RR* )
17 xmulcl 11348 . . 3  |-  ( ( A  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  ( A xe ( B xe C ) )  e.  RR* )
1814, 16, 17syl2anc 661 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  ( A xe ( B xe C ) )  e.  RR* )
19 oveq2 6209 . . . . 5  |-  ( y  =  B  ->  (
x xe y )  =  ( x xe B ) )
2019oveq1d 6216 . . . 4  |-  ( y  =  B  ->  (
( x xe y ) xe C )  =  ( ( x xe B ) xe C ) )
21 oveq1 6208 . . . . 5  |-  ( y  =  B  ->  (
y xe C )  =  ( B xe C ) )
2221oveq2d 6217 . . . 4  |-  ( y  =  B  ->  (
x xe ( y xe C ) )  =  ( x xe ( B xe C ) ) )
2320, 22eqeq12d 2476 . . 3  |-  ( y  =  B  ->  (
( ( x xe y ) xe C )  =  ( x xe ( y xe C ) )  <->  ( (
x xe B ) xe C )  =  ( x xe ( B xe C ) ) ) )
24 oveq2 6209 . . . . 5  |-  ( y  =  -e B  ->  ( x xe y )  =  ( x xe 
-e B ) )
2524oveq1d 6216 . . . 4  |-  ( y  =  -e B  ->  ( ( x xe y ) xe C )  =  ( ( x xe  -e
B ) xe C ) )
26 oveq1 6208 . . . . 5  |-  ( y  =  -e B  ->  ( y xe C )  =  (  -e B xe C ) )
2726oveq2d 6217 . . . 4  |-  ( y  =  -e B  ->  ( x xe ( y xe C ) )  =  ( x xe (  -e
B xe C ) ) )
2825, 27eqeq12d 2476 . . 3  |-  ( y  =  -e B  ->  ( ( ( x xe y ) xe C )  =  ( x xe ( y xe C ) )  <->  ( ( x xe  -e
B ) xe C )  =  ( x xe ( 
-e B xe C ) ) ) )
29 simprl 755 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  ->  x  e.  RR* )
30 simpl2 992 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  ->  B  e.  RR* )
31 xmulcl 11348 . . . . 5  |-  ( ( x  e.  RR*  /\  B  e.  RR* )  ->  (
x xe B )  e.  RR* )
3229, 30, 31syl2anc 661 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe B )  e.  RR* )
3311adantr 465 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  ->  C  e.  RR* )
34 xmulcl 11348 . . . 4  |-  ( ( ( x xe B )  e.  RR*  /\  C  e.  RR* )  ->  ( ( x xe B ) xe C )  e. 
RR* )
3532, 33, 34syl2anc 661 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe B ) xe C )  e. 
RR* )
3616adantr 465 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( B xe C )  e.  RR* )
37 xmulcl 11348 . . . 4  |-  ( ( x  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  (
x xe ( B xe C ) )  e.  RR* )
3829, 36, 37syl2anc 661 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe ( B xe C ) )  e. 
RR* )
39 oveq2 6209 . . . . 5  |-  ( z  =  C  ->  (
( x xe y ) xe z )  =  ( ( x xe y ) xe C ) )
40 oveq2 6209 . . . . . 6  |-  ( z  =  C  ->  (
y xe z )  =  ( y xe C ) )
4140oveq2d 6217 . . . . 5  |-  ( z  =  C  ->  (
x xe ( y xe z ) )  =  ( x xe ( y xe C ) ) )
4239, 41eqeq12d 2476 . . . 4  |-  ( z  =  C  ->  (
( ( x xe y ) xe z )  =  ( x xe ( y xe z ) )  <->  ( (
x xe y ) xe C )  =  ( x xe ( y xe C ) ) ) )
43 oveq2 6209 . . . . 5  |-  ( z  =  -e C  ->  ( ( x xe y ) xe z )  =  ( ( x xe y ) xe  -e
C ) )
44 oveq2 6209 . . . . . 6  |-  ( z  =  -e C  ->  ( y xe z )  =  ( y xe 
-e C ) )
4544oveq2d 6217 . . . . 5  |-  ( z  =  -e C  ->  ( x xe ( y xe z ) )  =  ( x xe ( y xe  -e C ) ) )
4643, 45eqeq12d 2476 . . . 4  |-  ( z  =  -e C  ->  ( ( ( x xe y ) xe z )  =  ( x xe ( y xe z ) )  <->  ( ( x xe y ) xe  -e
C )  =  ( x xe ( y xe  -e C ) ) ) )
4729adantr 465 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  ->  x  e.  RR* )
48 simprl 755 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
y  e.  RR* )
49 xmulcl 11348 . . . . . 6  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x xe y )  e.  RR* )
5047, 48, 49syl2anc 661 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe y )  e.  RR* )
5133adantr 465 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  ->  C  e.  RR* )
52 xmulcl 11348 . . . . 5  |-  ( ( ( x xe y )  e.  RR*  /\  C  e.  RR* )  ->  ( ( x xe y ) xe C )  e. 
RR* )
5350, 51, 52syl2anc 661 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( ( x xe y ) xe C )  e. 
RR* )
54 xmulcl 11348 . . . . . 6  |-  ( ( y  e.  RR*  /\  C  e.  RR* )  ->  (
y xe C )  e.  RR* )
5548, 51, 54syl2anc 661 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( y xe C )  e.  RR* )
56 xmulcl 11348 . . . . 5  |-  ( ( x  e.  RR*  /\  (
y xe C )  e.  RR* )  ->  ( x xe ( y xe C ) )  e. 
RR* )
5747, 55, 56syl2anc 661 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe ( y xe C ) )  e. 
RR* )
58 xmulasslem3 11361 . . . . . 6  |-  ( ( ( x  e.  RR*  /\  0  <  x )  /\  ( y  e. 
RR*  /\  0  <  y )  /\  ( z  e.  RR*  /\  0  <  z ) )  -> 
( ( x xe y ) xe z )  =  ( x xe ( y xe z ) ) )
59583expa 1188 . . . . 5  |-  ( ( ( ( x  e. 
RR*  /\  0  <  x )  /\  ( y  e.  RR*  /\  0  <  y ) )  /\  ( z  e.  RR*  /\  0  <  z ) )  ->  ( (
x xe y ) xe z )  =  ( x xe ( y xe z ) ) )
6059adantlll 717 . . . 4  |-  ( ( ( ( ( A  e.  RR*  /\  B  e. 
RR*  /\  C  e.  RR* )  /\  ( x  e.  RR*  /\  0  <  x ) )  /\  ( y  e.  RR*  /\  0  <  y ) )  /\  ( z  e.  RR*  /\  0  <  z ) )  -> 
( ( x xe y ) xe z )  =  ( x xe ( y xe z ) ) )
61 xmul01 11342 . . . . . . . 8  |-  ( ( x xe y )  e.  RR*  ->  ( ( x xe y ) xe 0 )  =  0 )
6250, 61syl 16 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( ( x xe y ) xe 0 )  =  0 )
63 xmul01 11342 . . . . . . . 8  |-  ( x  e.  RR*  ->  ( x xe 0 )  =  0 )
6447, 63syl 16 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe 0 )  =  0 )
6562, 64eqtr4d 2498 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( ( x xe y ) xe 0 )  =  ( x xe 0 ) )
66 xmul01 11342 . . . . . . . 8  |-  ( y  e.  RR*  ->  ( y xe 0 )  =  0 )
6766ad2antrl 727 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( y xe 0 )  =  0 )
6867oveq2d 6217 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe ( y xe 0 ) )  =  ( x xe 0 ) )
6965, 68eqtr4d 2498 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( ( x xe y ) xe 0 )  =  ( x xe ( y xe 0 ) ) )
70 oveq2 6209 . . . . . 6  |-  ( z  =  0  ->  (
( x xe y ) xe z )  =  ( ( x xe y ) xe 0 ) )
71 oveq2 6209 . . . . . . 7  |-  ( z  =  0  ->  (
y xe z )  =  ( y xe 0 ) )
7271oveq2d 6217 . . . . . 6  |-  ( z  =  0  ->  (
x xe ( y xe z ) )  =  ( x xe ( y xe 0 ) ) )
7370, 72eqeq12d 2476 . . . . 5  |-  ( z  =  0  ->  (
( ( x xe y ) xe z )  =  ( x xe ( y xe z ) )  <->  ( (
x xe y ) xe 0 )  =  ( x xe ( y xe 0 ) ) ) )
7469, 73syl5ibrcom 222 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( z  =  0  ->  ( ( x xe y ) xe z )  =  ( x xe ( y xe z ) ) ) )
75 xmulneg2 11345 . . . . 5  |-  ( ( ( x xe y )  e.  RR*  /\  C  e.  RR* )  ->  ( ( x xe y ) xe  -e C )  =  -e
( ( x xe y ) xe C ) )
7650, 51, 75syl2anc 661 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( ( x xe y ) xe  -e C )  =  -e
( ( x xe y ) xe C ) )
77 xmulneg2 11345 . . . . . . 7  |-  ( ( y  e.  RR*  /\  C  e.  RR* )  ->  (
y xe  -e C )  = 
-e ( y xe C ) )
7848, 51, 77syl2anc 661 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( y xe 
-e C )  =  -e ( y xe C ) )
7978oveq2d 6217 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe ( y xe 
-e C ) )  =  ( x xe  -e
( y xe C ) ) )
80 xmulneg2 11345 . . . . . 6  |-  ( ( x  e.  RR*  /\  (
y xe C )  e.  RR* )  ->  ( x xe 
-e ( y xe C ) )  =  -e
( x xe ( y xe C ) ) )
8147, 55, 80syl2anc 661 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe 
-e ( y xe C ) )  =  -e
( x xe ( y xe C ) ) )
8279, 81eqtrd 2495 . . . 4  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( x xe ( y xe 
-e C ) )  =  -e
( x xe ( y xe C ) ) )
8342, 46, 53, 57, 51, 60, 74, 76, 82xmulasslem 11360 . . 3  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( ( x xe y ) xe C )  =  ( x xe ( y xe C ) ) )
84 xmul02 11343 . . . . . . . 8  |-  ( C  e.  RR*  ->  ( 0 xe C )  =  0 )
85843ad2ant3 1011 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
0 xe C )  =  0 )
8685adantr 465 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( 0 xe C )  =  0 )
8763ad2antrl 727 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe 0 )  =  0 )
8886, 87eqtr4d 2498 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( 0 xe C )  =  ( x xe 0 ) )
8987oveq1d 6216 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe 0 ) xe C )  =  ( 0 xe C ) )
9086oveq2d 6217 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe ( 0 xe C ) )  =  ( x xe 0 ) )
9188, 89, 903eqtr4d 2505 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe 0 ) xe C )  =  ( x xe ( 0 xe C ) ) )
92 oveq2 6209 . . . . . 6  |-  ( y  =  0  ->  (
x xe y )  =  ( x xe 0 ) )
9392oveq1d 6216 . . . . 5  |-  ( y  =  0  ->  (
( x xe y ) xe C )  =  ( ( x xe 0 ) xe C ) )
94 oveq1 6208 . . . . . 6  |-  ( y  =  0  ->  (
y xe C )  =  ( 0 xe C ) )
9594oveq2d 6217 . . . . 5  |-  ( y  =  0  ->  (
x xe ( y xe C ) )  =  ( x xe ( 0 xe C ) ) )
9693, 95eqeq12d 2476 . . . 4  |-  ( y  =  0  ->  (
( ( x xe y ) xe C )  =  ( x xe ( y xe C ) )  <->  ( (
x xe 0 ) xe C )  =  ( x xe ( 0 xe C ) ) ) )
9791, 96syl5ibrcom 222 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( y  =  0  ->  ( ( x xe y ) xe C )  =  ( x xe ( y xe C ) ) ) )
98 xmulneg2 11345 . . . . . 6  |-  ( ( x  e.  RR*  /\  B  e.  RR* )  ->  (
x xe  -e B )  = 
-e ( x xe B ) )
9929, 30, 98syl2anc 661 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe 
-e B )  =  -e ( x xe B ) )
10099oveq1d 6216 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe  -e B ) xe C )  =  (  -e ( x xe B ) xe C ) )
101 xmulneg1 11344 . . . . 5  |-  ( ( ( x xe B )  e.  RR*  /\  C  e.  RR* )  ->  (  -e ( x xe B ) xe C )  =  -e
( ( x xe B ) xe C ) )
10232, 33, 101syl2anc 661 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
(  -e ( x xe B ) xe C )  =  -e ( ( x xe B ) xe C ) )
103100, 102eqtrd 2495 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe  -e B ) xe C )  =  -e
( ( x xe B ) xe C ) )
104 xmulneg1 11344 . . . . . 6  |-  ( ( B  e.  RR*  /\  C  e.  RR* )  ->  (  -e B xe C )  =  -e ( B xe C ) )
10530, 33, 104syl2anc 661 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
(  -e B xe C )  = 
-e ( B xe C ) )
106105oveq2d 6217 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe (  -e B xe C ) )  =  ( x xe  -e
( B xe C ) ) )
107 xmulneg2 11345 . . . . 5  |-  ( ( x  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  (
x xe  -e ( B xe C ) )  =  -e ( x xe ( B xe C ) ) )
10829, 36, 107syl2anc 661 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe 
-e ( B xe C ) )  =  -e
( x xe ( B xe C ) ) )
109106, 108eqtrd 2495 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe (  -e B xe C ) )  =  -e
( x xe ( B xe C ) ) )
11023, 28, 35, 38, 30, 83, 97, 103, 109xmulasslem 11360 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe B ) xe C )  =  ( x xe ( B xe C ) ) )
111 xmul02 11343 . . . . . 6  |-  ( B  e.  RR*  ->  ( 0 xe B )  =  0 )
1121113ad2ant2 1010 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
0 xe B )  =  0 )
113112oveq1d 6216 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( 0 xe B ) xe C )  =  ( 0 xe C ) )
114 xmul02 11343 . . . . 5  |-  ( ( B xe C )  e.  RR*  ->  ( 0 xe ( B xe C ) )  =  0 )
11516, 114syl 16 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
0 xe ( B xe C ) )  =  0 )
11685, 113, 1153eqtr4d 2505 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( 0 xe B ) xe C )  =  ( 0 xe ( B xe C ) ) )
117 oveq1 6208 . . . . 5  |-  ( x  =  0  ->  (
x xe B )  =  ( 0 xe B ) )
118117oveq1d 6216 . . . 4  |-  ( x  =  0  ->  (
( x xe B ) xe C )  =  ( ( 0 xe B ) xe C ) )
119 oveq1 6208 . . . 4  |-  ( x  =  0  ->  (
x xe ( B xe C ) )  =  ( 0 xe ( B xe C ) ) )
120118, 119eqeq12d 2476 . . 3  |-  ( x  =  0  ->  (
( ( x xe B ) xe C )  =  ( x xe ( B xe C ) )  <->  ( (
0 xe B ) xe C )  =  ( 0 xe ( B xe C ) ) ) )
121116, 120syl5ibrcom 222 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
x  =  0  -> 
( ( x xe B ) xe C )  =  ( x xe ( B xe C ) ) ) )
122 xmulneg1 11344 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (  -e A xe B )  =  -e ( A xe B ) )
1231223adant3 1008 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (  -e A xe B )  =  -e ( A xe B ) )
124123oveq1d 6216 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
(  -e A xe B ) xe C )  =  (  -e ( A xe B ) xe C ) )
125 xmulneg1 11344 . . . 4  |-  ( ( ( A xe B )  e.  RR*  /\  C  e.  RR* )  ->  (  -e ( A xe B ) xe C )  =  -e
( ( A xe B ) xe C ) )
12610, 11, 125syl2anc 661 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (  -e ( A xe B ) xe C )  = 
-e ( ( A xe B ) xe C ) )
127124, 126eqtrd 2495 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
(  -e A xe B ) xe C )  = 
-e ( ( A xe B ) xe C ) )
128 xmulneg1 11344 . . 3  |-  ( ( A  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  (  -e A xe ( B xe C ) )  = 
-e ( A xe ( B xe C ) ) )
12914, 16, 128syl2anc 661 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (  -e A xe ( B xe C ) )  = 
-e ( A xe ( B xe C ) ) )
1304, 8, 13, 18, 14, 110, 121, 127, 129xmulasslem 11360 1  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( A xe B ) xe C )  =  ( A xe ( B xe C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758   class class class wbr 4401  (class class class)co 6201   0cc0 9394   RR*cxr 9529    < clt 9530    -ecxne 11198   xecxmu 11200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-cnex 9450  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-po 4750  df-so 4751  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-1st 6688  df-2nd 6689  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-xneg 11201  df-xmul 11203
This theorem is referenced by:  xlemul1  11365  xrsmcmn  17965  nmoi2  20442  xmulcand  26242  xreceu  26243  xdivrec  26248  xrge0slmod  26458
  Copyright terms: Public domain W3C validator