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 \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$

Proof

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

Metamath Proof Explorer

Theorem xadddi

Proof