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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ·e ( 𝐵 +𝑒 𝐶 ) ) = ( ( 𝐴 ·e 𝐵 ) +𝑒 ( 𝐴 ·e 𝐶 ) ) )

Proof

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