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 B * C * A 𝑒 B + 𝑒 C = A 𝑒 B + 𝑒 A 𝑒 C

Proof

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