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

Theorem xmulass 11422
Description: Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 11384 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 6225 . . . 4  |-  ( x  =  A  ->  (
x xe B )  =  ( A xe B ) )
21oveq1d 6233 . . 3  |-  ( x  =  A  ->  (
( x xe B ) xe C )  =  ( ( A xe B ) xe C ) )
3 oveq1 6225 . . 3  |-  ( x  =  A  ->  (
x xe ( B xe C ) )  =  ( A xe ( B xe C ) ) )
42, 3eqeq12d 2418 . 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 6225 . . . 4  |-  ( x  =  -e A  ->  ( x xe B )  =  (  -e A xe B ) )
65oveq1d 6233 . . 3  |-  ( x  =  -e A  ->  ( ( x xe B ) xe C )  =  ( (  -e A xe B ) xe C ) )
7 oveq1 6225 . . 3  |-  ( x  =  -e A  ->  ( x xe ( B xe C ) )  =  (  -e
A xe ( B xe C ) ) )
86, 7eqeq12d 2418 . 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 11408 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A xe B )  e.  RR* )
10 xmulcl 11408 . . 3  |-  ( ( ( A xe B )  e.  RR*  /\  C  e.  RR* )  ->  ( ( A xe B ) xe C )  e. 
RR* )
119, 10stoic3 1624 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( A xe B ) xe C )  e.  RR* )
12 simp1 994 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  A  e.  RR* )
13 xmulcl 11408 . . . 4  |-  ( ( B  e.  RR*  /\  C  e.  RR* )  ->  ( B xe C )  e.  RR* )
14133adant1 1012 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  ( B xe C )  e.  RR* )
15 xmulcl 11408 . . 3  |-  ( ( A  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  ( A xe ( B xe C ) )  e.  RR* )
1612, 14, 15syl2anc 659 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  ( A xe ( B xe C ) )  e.  RR* )
17 oveq2 6226 . . . . 5  |-  ( y  =  B  ->  (
x xe y )  =  ( x xe B ) )
1817oveq1d 6233 . . . 4  |-  ( y  =  B  ->  (
( x xe y ) xe C )  =  ( ( x xe B ) xe C ) )
19 oveq1 6225 . . . . 5  |-  ( y  =  B  ->  (
y xe C )  =  ( B xe C ) )
2019oveq2d 6234 . . . 4  |-  ( y  =  B  ->  (
x xe ( y xe C ) )  =  ( x xe ( B xe C ) ) )
2118, 20eqeq12d 2418 . . 3  |-  ( y  =  B  ->  (
( ( x xe y ) xe C )  =  ( x xe ( y xe C ) )  <->  ( (
x xe B ) xe C )  =  ( x xe ( B xe C ) ) ) )
22 oveq2 6226 . . . . 5  |-  ( y  =  -e B  ->  ( x xe y )  =  ( x xe 
-e B ) )
2322oveq1d 6233 . . . 4  |-  ( y  =  -e B  ->  ( ( x xe y ) xe C )  =  ( ( x xe  -e
B ) xe C ) )
24 oveq1 6225 . . . . 5  |-  ( y  =  -e B  ->  ( y xe C )  =  (  -e B xe C ) )
2524oveq2d 6234 . . . 4  |-  ( y  =  -e B  ->  ( x xe ( y xe C ) )  =  ( x xe (  -e
B xe C ) ) )
2623, 25eqeq12d 2418 . . 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 ) ) ) )
27 simprl 754 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  ->  x  e.  RR* )
28 simpl2 998 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  ->  B  e.  RR* )
29 xmulcl 11408 . . . . 5  |-  ( ( x  e.  RR*  /\  B  e.  RR* )  ->  (
x xe B )  e.  RR* )
3027, 28, 29syl2anc 659 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe B )  e.  RR* )
31 simpl3 999 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  ->  C  e.  RR* )
32 xmulcl 11408 . . . 4  |-  ( ( ( x xe B )  e.  RR*  /\  C  e.  RR* )  ->  ( ( x xe B ) xe C )  e. 
RR* )
3330, 31, 32syl2anc 659 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe B ) xe C )  e. 
RR* )
3414adantr 463 . . . 4  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( B xe C )  e.  RR* )
35 xmulcl 11408 . . . 4  |-  ( ( x  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  (
x xe ( B xe C ) )  e.  RR* )
3627, 34, 35syl2anc 659 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe ( B xe C ) )  e. 
RR* )
37 oveq2 6226 . . . . 5  |-  ( z  =  C  ->  (
( x xe y ) xe z )  =  ( ( x xe y ) xe C ) )
38 oveq2 6226 . . . . . 6  |-  ( z  =  C  ->  (
y xe z )  =  ( y xe C ) )
3938oveq2d 6234 . . . . 5  |-  ( z  =  C  ->  (
x xe ( y xe z ) )  =  ( x xe ( y xe C ) ) )
4037, 39eqeq12d 2418 . . . 4  |-  ( z  =  C  ->  (
( ( x xe y ) xe z )  =  ( x xe ( y xe z ) )  <->  ( (
x xe y ) xe C )  =  ( x xe ( y xe C ) ) ) )
41 oveq2 6226 . . . . 5  |-  ( z  =  -e C  ->  ( ( x xe y ) xe z )  =  ( ( x xe y ) xe  -e
C ) )
42 oveq2 6226 . . . . . 6  |-  ( z  =  -e C  ->  ( y xe z )  =  ( y xe 
-e C ) )
4342oveq2d 6234 . . . . 5  |-  ( z  =  -e C  ->  ( x xe ( y xe z ) )  =  ( x xe ( y xe  -e C ) ) )
4441, 43eqeq12d 2418 . . . 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 ) ) ) )
4527adantr 463 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  ->  x  e.  RR* )
46 simprl 754 . . . . . 6  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
y  e.  RR* )
47 xmulcl 11408 . . . . . 6  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x xe y )  e.  RR* )
4845, 46, 47syl2anc 659 . . . . 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* )
4931adantr 463 . . . . 5  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  ->  C  e.  RR* )
50 xmulcl 11408 . . . . 5  |-  ( ( ( x xe y )  e.  RR*  /\  C  e.  RR* )  ->  ( ( x xe y ) xe C )  e. 
RR* )
5148, 49, 50syl2anc 659 . . . 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* )
52 xmulcl 11408 . . . . . 6  |-  ( ( y  e.  RR*  /\  C  e.  RR* )  ->  (
y xe C )  e.  RR* )
5346, 49, 52syl2anc 659 . . . . 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* )
54 xmulcl 11408 . . . . 5  |-  ( ( x  e.  RR*  /\  (
y xe C )  e.  RR* )  ->  ( x xe ( y xe C ) )  e. 
RR* )
5545, 53, 54syl2anc 659 . . . 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* )
56 xmulasslem3 11421 . . . . . 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 ) ) )
57563expa 1194 . . . . 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 ) ) )
5857adantlll 715 . . . 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 ) ) )
59 xmul01 11402 . . . . . . . 8  |-  ( ( x xe y )  e.  RR*  ->  ( ( x xe y ) xe 0 )  =  0 )
6048, 59syl 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 )
61 xmul01 11402 . . . . . . . 8  |-  ( x  e.  RR*  ->  ( x xe 0 )  =  0 )
6245, 61syl 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 )
6360, 62eqtr4d 2440 . . . . . 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 ) )
64 xmul01 11402 . . . . . . . 8  |-  ( y  e.  RR*  ->  ( y xe 0 )  =  0 )
6564ad2antrl 725 . . . . . . 7  |-  ( ( ( ( A  e. 
RR*  /\  B  e.  RR* 
/\  C  e.  RR* )  /\  ( x  e. 
RR*  /\  0  <  x ) )  /\  (
y  e.  RR*  /\  0  <  y ) )  -> 
( y xe 0 )  =  0 )
6665oveq2d 6234 . . . . . 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 ) )
6763, 66eqtr4d 2440 . . . . 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 ) ) )
68 oveq2 6226 . . . . . 6  |-  ( z  =  0  ->  (
( x xe y ) xe z )  =  ( ( x xe y ) xe 0 ) )
69 oveq2 6226 . . . . . . 7  |-  ( z  =  0  ->  (
y xe z )  =  ( y xe 0 ) )
7069oveq2d 6234 . . . . . 6  |-  ( z  =  0  ->  (
x xe ( y xe z ) )  =  ( x xe ( y xe 0 ) ) )
7168, 70eqeq12d 2418 . . . . 5  |-  ( z  =  0  ->  (
( ( x xe y ) xe z )  =  ( x xe ( y xe z ) )  <->  ( (
x xe y ) xe 0 )  =  ( x xe ( y xe 0 ) ) ) )
7267, 71syl5ibrcom 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 ) ) ) )
73 xmulneg2 11405 . . . . 5  |-  ( ( ( x xe y )  e.  RR*  /\  C  e.  RR* )  ->  ( ( x xe y ) xe  -e C )  =  -e
( ( x xe y ) xe C ) )
7448, 49, 73syl2anc 659 . . . 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 ) )
75 xmulneg2 11405 . . . . . . 7  |-  ( ( y  e.  RR*  /\  C  e.  RR* )  ->  (
y xe  -e C )  = 
-e ( y xe C ) )
7646, 49, 75syl2anc 659 . . . . . 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 ) )
7776oveq2d 6234 . . . . 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 ) ) )
78 xmulneg2 11405 . . . . . 6  |-  ( ( x  e.  RR*  /\  (
y xe C )  e.  RR* )  ->  ( x xe 
-e ( y xe C ) )  =  -e
( x xe ( y xe C ) ) )
7945, 53, 78syl2anc 659 . . . . 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 ) ) )
8077, 79eqtrd 2437 . . . 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 ) ) )
8140, 44, 51, 55, 49, 58, 72, 74, 80xmulasslem 11420 . . 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 ) ) )
82 xmul02 11403 . . . . . . . 8  |-  ( C  e.  RR*  ->  ( 0 xe C )  =  0 )
83823ad2ant3 1017 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
0 xe C )  =  0 )
8483adantr 463 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( 0 xe C )  =  0 )
8561ad2antrl 725 . . . . . 6  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe 0 )  =  0 )
8684, 85eqtr4d 2440 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( 0 xe C )  =  ( x xe 0 ) )
8785oveq1d 6233 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( ( x xe 0 ) xe C )  =  ( 0 xe C ) )
8884oveq2d 6234 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe ( 0 xe C ) )  =  ( x xe 0 ) )
8986, 87, 883eqtr4d 2447 . . . 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 ) ) )
90 oveq2 6226 . . . . . 6  |-  ( y  =  0  ->  (
x xe y )  =  ( x xe 0 ) )
9190oveq1d 6233 . . . . 5  |-  ( y  =  0  ->  (
( x xe y ) xe C )  =  ( ( x xe 0 ) xe C ) )
92 oveq1 6225 . . . . . 6  |-  ( y  =  0  ->  (
y xe C )  =  ( 0 xe C ) )
9392oveq2d 6234 . . . . 5  |-  ( y  =  0  ->  (
x xe ( y xe C ) )  =  ( x xe ( 0 xe C ) ) )
9491, 93eqeq12d 2418 . . . 4  |-  ( y  =  0  ->  (
( ( x xe y ) xe C )  =  ( x xe ( y xe C ) )  <->  ( (
x xe 0 ) xe C )  =  ( x xe ( 0 xe C ) ) ) )
9589, 94syl5ibrcom 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 ) ) ) )
96 xmulneg2 11405 . . . . . 6  |-  ( ( x  e.  RR*  /\  B  e.  RR* )  ->  (
x xe  -e B )  = 
-e ( x xe B ) )
9727, 28, 96syl2anc 659 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
( x xe 
-e B )  =  -e ( x xe B ) )
9897oveq1d 6233 . . . 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 ) )
99 xmulneg1 11404 . . . . 5  |-  ( ( ( x xe B )  e.  RR*  /\  C  e.  RR* )  ->  (  -e ( x xe B ) xe C )  =  -e
( ( x xe B ) xe C ) )
10030, 31, 99syl2anc 659 . . . 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 ) )
10198, 100eqtrd 2437 . . 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 ) )
102 xmulneg1 11404 . . . . . 6  |-  ( ( B  e.  RR*  /\  C  e.  RR* )  ->  (  -e B xe C )  =  -e ( B xe C ) )
10328, 31, 102syl2anc 659 . . . . 5  |-  ( ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  (
x  e.  RR*  /\  0  <  x ) )  -> 
(  -e B xe C )  = 
-e ( B xe C ) )
104103oveq2d 6234 . . . 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 ) ) )
105 xmulneg2 11405 . . . . 5  |-  ( ( x  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  (
x xe  -e ( B xe C ) )  =  -e ( x xe ( B xe C ) ) )
10627, 34, 105syl2anc 659 . . . 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 ) ) )
107104, 106eqtrd 2437 . . 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 ) ) )
10821, 26, 33, 36, 28, 81, 95, 101, 107xmulasslem 11420 . 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 ) ) )
109 xmul02 11403 . . . . . 6  |-  ( B  e.  RR*  ->  ( 0 xe B )  =  0 )
1101093ad2ant2 1016 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
0 xe B )  =  0 )
111110oveq1d 6233 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( 0 xe B ) xe C )  =  ( 0 xe C ) )
112 xmul02 11403 . . . . 5  |-  ( ( B xe C )  e.  RR*  ->  ( 0 xe ( B xe C ) )  =  0 )
11314, 112syl 16 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
0 xe ( B xe C ) )  =  0 )
11483, 111, 1133eqtr4d 2447 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
( 0 xe B ) xe C )  =  ( 0 xe ( B xe C ) ) )
115 oveq1 6225 . . . . 5  |-  ( x  =  0  ->  (
x xe B )  =  ( 0 xe B ) )
116115oveq1d 6233 . . . 4  |-  ( x  =  0  ->  (
( x xe B ) xe C )  =  ( ( 0 xe B ) xe C ) )
117 oveq1 6225 . . . 4  |-  ( x  =  0  ->  (
x xe ( B xe C ) )  =  ( 0 xe ( B xe C ) ) )
118116, 117eqeq12d 2418 . . 3  |-  ( x  =  0  ->  (
( ( x xe B ) xe C )  =  ( x xe ( B xe C ) )  <->  ( (
0 xe B ) xe C )  =  ( 0 xe ( B xe C ) ) ) )
119114, 118syl5ibrcom 222 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
x  =  0  -> 
( ( x xe B ) xe C )  =  ( x xe ( B xe C ) ) ) )
120 xmulneg1 11404 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (  -e A xe B )  =  -e ( A xe B ) )
1211203adant3 1014 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (  -e A xe B )  =  -e ( A xe B ) )
122121oveq1d 6233 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
(  -e A xe B ) xe C )  =  (  -e ( A xe B ) xe C ) )
123 xmulneg1 11404 . . . 4  |-  ( ( ( A xe B )  e.  RR*  /\  C  e.  RR* )  ->  (  -e ( A xe B ) xe C )  =  -e
( ( A xe B ) xe C ) )
1249, 123stoic3 1624 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (  -e ( A xe B ) xe C )  = 
-e ( ( A xe B ) xe C ) )
125122, 124eqtrd 2437 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (
(  -e A xe B ) xe C )  = 
-e ( ( A xe B ) xe C ) )
126 xmulneg1 11404 . . 3  |-  ( ( A  e.  RR*  /\  ( B xe C )  e.  RR* )  ->  (  -e A xe ( B xe C ) )  = 
-e ( A xe ( B xe C ) ) )
12712, 14, 126syl2anc 659 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e. 
RR* )  ->  (  -e A xe ( B xe C ) )  = 
-e ( A xe ( B xe C ) ) )
1284, 8, 11, 16, 12, 108, 119, 125, 127xmulasslem 11420 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 367    /\ w3a 971    = wceq 1399    e. wcel 1836   class class class wbr 4384  (class class class)co 6218   0cc0 9425   RR*cxr 9560    < clt 9561    -ecxne 11258   xecxmu 11260
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-id 4726  df-po 4731  df-so 4732  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-1st 6721  df-2nd 6722  df-er 7251  df-en 7458  df-dom 7459  df-sdom 7460  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-xneg 11261  df-xmul 11263
This theorem is referenced by:  xlemul1  11425  xrsmcmn  18577  nmoi2  21345  xmulcand  27804  xreceu  27805  xdivrec  27810  xrge0slmod  28023
  Copyright terms: Public domain W3C validator