# Metamath Proof Explorer

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 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\to {A}{\cdot }_{𝑒}\left({B}{+}_{𝑒}{C}\right)=\left({A}{\cdot }_{𝑒}{B}\right){+}_{𝑒}\left({A}{\cdot }_{𝑒}{C}\right)$

### Proof

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