Metamath Proof Explorer

Theorem xadddi

Description: Distributive property for extended real addition and multiplication. Like xaddass , this has an unusual domain of correctness due to counterexamples like ( +oo x. ( 2 - 1 ) ) = -oo =/= ( ( +oo x. 2 ) - ( +oo x. 1 ) ) = ( +oo - +oo ) = 0 . In this theorem we show that if the multiplier is real then everything works as expected. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xadddi 
|- ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )

Proof

Step Hyp Ref Expression
1 xadddilem 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < A ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
2 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> B e. RR* )
3 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> C e. RR* )
4 xaddcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B +e C ) e. RR* )
5 2 3 4 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( B +e C ) e. RR* )
6 xmul02 
 |-  ( ( B +e C ) e. RR* -> ( 0 *e ( B +e C ) ) = 0 )
7 5 6 syl 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e ( B +e C ) ) = 0 )
8 0xr 
 |-  0 e. RR*
9 xaddid1 
 |-  ( 0 e. RR* -> ( 0 +e 0 ) = 0 )
10 8 9 ax-mp 
 |-  ( 0 +e 0 ) = 0
11 7 10 eqtr4di 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e ( B +e C ) ) = ( 0 +e 0 ) )
12 simpr 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> 0 = A )
13 12 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e ( B +e C ) ) = ( A *e ( B +e C ) ) )
14 xmul02 
 |-  ( B e. RR* -> ( 0 *e B ) = 0 )
15 2 14 syl 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e B ) = 0 )
16 12 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e B ) = ( A *e B ) )
17 15 16 eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> 0 = ( A *e B ) )
18 xmul02 
 |-  ( C e. RR* -> ( 0 *e C ) = 0 )
19 3 18 syl 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e C ) = 0 )
20 12 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 *e C ) = ( A *e C ) )
21 19 20 eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> 0 = ( A *e C ) )
22 17 21 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( 0 +e 0 ) = ( ( A *e B ) +e ( A *e C ) ) )
23 11 13 22 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 = A ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
24 simp1 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> A e. RR )
25 24 adantr 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> A e. RR )
26 rexneg 
 |-  ( A e. RR -> -e A = -u A )
27 renegcl 
 |-  ( A e. RR -> -u A e. RR )
28 26 27 eqeltrd 
 |-  ( A e. RR -> -e A e. RR )
29 25 28 syl 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> -e A e. RR )
30 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> B e. RR* )
31 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> C e. RR* )
32 24 rexrd 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> A e. RR* )
33 xlt0neg1 
 |-  ( A e. RR* -> ( A < 0 <-> 0 < -e A ) )
34 32 33 syl 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> ( A < 0 <-> 0 < -e A ) )
35 34 biimpa 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> 0 < -e A )
36 xadddilem 
 |-  ( ( ( -e A e. RR /\ B e. RR* /\ C e. RR* ) /\ 0 < -e A ) -> ( -e A *e ( B +e C ) ) = ( ( -e A *e B ) +e ( -e A *e C ) ) )
37 29 30 31 35 36 syl31anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( -e A *e ( B +e C ) ) = ( ( -e A *e B ) +e ( -e A *e C ) ) )
38 32 adantr 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> A e. RR* )
39 30 31 4 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( B +e C ) e. RR* )
40 xmulneg1 
 |-  ( ( A e. RR* /\ ( B +e C ) e. RR* ) -> ( -e A *e ( B +e C ) ) = -e ( A *e ( B +e C ) ) )
41 38 39 40 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( -e A *e ( B +e C ) ) = -e ( A *e ( B +e C ) ) )
42 xmulneg1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A *e B ) = -e ( A *e B ) )
43 38 30 42 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( -e A *e B ) = -e ( A *e B ) )
44 xmulneg1 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( -e A *e C ) = -e ( A *e C ) )
45 38 31 44 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( -e A *e C ) = -e ( A *e C ) )
46 43 45 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( ( -e A *e B ) +e ( -e A *e C ) ) = ( -e ( A *e B ) +e -e ( A *e C ) ) )
47 xmulcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) e. RR* )
48 38 30 47 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( A *e B ) e. RR* )
49 xmulcl 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A *e C ) e. RR* )
50 38 31 49 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( A *e C ) e. RR* )
51 xnegdi 
 |-  ( ( ( A *e B ) e. RR* /\ ( A *e C ) e. RR* ) -> -e ( ( A *e B ) +e ( A *e C ) ) = ( -e ( A *e B ) +e -e ( A *e C ) ) )
52 48 50 51 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> -e ( ( A *e B ) +e ( A *e C ) ) = ( -e ( A *e B ) +e -e ( A *e C ) ) )
53 46 52 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( ( -e A *e B ) +e ( -e A *e C ) ) = -e ( ( A *e B ) +e ( A *e C ) ) )
54 37 41 53 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> -e ( A *e ( B +e C ) ) = -e ( ( A *e B ) +e ( A *e C ) ) )
55 xmulcl 
 |-  ( ( A e. RR* /\ ( B +e C ) e. RR* ) -> ( A *e ( B +e C ) ) e. RR* )
56 38 39 55 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( A *e ( B +e C ) ) e. RR* )
57 xaddcl 
 |-  ( ( ( A *e B ) e. RR* /\ ( A *e C ) e. RR* ) -> ( ( A *e B ) +e ( A *e C ) ) e. RR* )
58 48 50 57 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( ( A *e B ) +e ( A *e C ) ) e. RR* )
59 xneg11 
 |-  ( ( ( A *e ( B +e C ) ) e. RR* /\ ( ( A *e B ) +e ( A *e C ) ) e. RR* ) -> ( -e ( A *e ( B +e C ) ) = -e ( ( A *e B ) +e ( A *e C ) ) <-> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) ) )
60 56 58 59 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( -e ( A *e ( B +e C ) ) = -e ( ( A *e B ) +e ( A *e C ) ) <-> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) ) )
61 54 60 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR* /\ C e. RR* ) /\ A < 0 ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
62 0re 
 |-  0 e. RR
63 lttri4 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A \/ 0 = A \/ A < 0 ) )
64 62 24 63 sylancr 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> ( 0 < A \/ 0 = A \/ A < 0 ) )
65 1 23 61 64 mpjao3dan 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )