xadddi2

Description: The assumption that the multiplier be real in xadddi can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xadddi2	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A \in ℝ) \to A \in ℝ$
2		simp2l	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \to B \in ℝ^{}$
3	2	ad2antrr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \land A \in ℝ) \to B \in ℝ^{}$
4		simp3l	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \to C \in ℝ^{}$
5	4	ad2antrr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \land A \in ℝ) \to C \in ℝ^{}$
6		xadddi	$⊢ (A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
7	1 3 5 6	syl3anc	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
8		pnfxr	$⊢ +∞ \in ℝ^{*}$
9	4	adantr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to C \in ℝ^{}$
10		xmulcl	$⊢ (+∞ \in ℝ^{} \land C \in ℝ^{}) \to +∞ \cdot_{𝑒} C \in ℝ^{*}$
11	8 9 10	sylancr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to +∞ \cdot_{𝑒} C \in ℝ^{}$
12		simpl3r	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to 0 \leq C$
13		0lepnf	$⊢ 0 \leq +∞$
14		xmulge0	$⊢ ((+∞ \in ℝ^{} \land 0 \leq +∞) \land (C \in ℝ^{} \land 0 \leq C)) \to 0 \leq +∞ \cdot_{𝑒} C$
15	8 13 14	mpanl12	$⊢ (C \in ℝ^{*} \land 0 \leq C) \to 0 \leq +∞ \cdot_{𝑒} C$
16	4 12 15	syl2an2r	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to 0 \leq +∞ \cdot_{𝑒} C$
17		ge0nemnf	$⊢ (+∞ \cdot_{𝑒} C \in ℝ^{*} \land 0 \leq +∞ \cdot_{𝑒} C) \to +∞ \cdot_{𝑒} C \neq −∞$
18	11 16 17	syl2anc	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to +∞ \cdot_{𝑒} C \neq −∞$
19	18	adantr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = +∞) \to +∞ \cdot_{𝑒} C \neq −∞$
20		xaddpnf2	$⊢ (+∞ \cdot_{𝑒} C \in ℝ^{*} \land +∞ \cdot_{𝑒} C \neq −∞) \to +∞ +_{𝑒} (+∞ \cdot_{𝑒} C) = +∞$
21	11 19 20	syl2an2r	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = +∞) \to +∞ +_{𝑒} (+∞ \cdot_{𝑒} C) = +∞$
22		oveq1	$⊢ A = +∞ \to A \cdot_{𝑒} B = +∞ \cdot_{𝑒} B$
23		oveq1	$⊢ A = +∞ \to A \cdot_{𝑒} C = +∞ \cdot_{𝑒} C$
24	22 23	oveq12d	$⊢ A = +∞ \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (+∞ \cdot_{𝑒} B) +_{𝑒} (+∞ \cdot_{𝑒} C)$
25		xmulpnf2	$⊢ (B \in ℝ^{*} \land 0 < B) \to +∞ \cdot_{𝑒} B = +∞$
26	2 25	sylan	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to +∞ \cdot_{𝑒} B = +∞$
27	26	oveq1d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (+∞ \cdot_{𝑒} B) +_{𝑒} (+∞ \cdot_{𝑒} C) = +∞ +_{𝑒} (+∞ \cdot_{𝑒} C)$
28	24 27	sylan9eqr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = +∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = +∞ +_{𝑒} (+∞ \cdot_{𝑒} C)$
29		oveq1	$⊢ A = +∞ \to A \cdot_{𝑒} (B +_{𝑒} C) = +∞ \cdot_{𝑒} (B +_{𝑒} C)$
30		xaddcl	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to B +_{𝑒} C \in ℝ^{*}$
31	2 4 30	syl2anc	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \to B +_{𝑒} C \in ℝ^{}$
32		0xr	$⊢ 0 \in ℝ^{*}$
33	32	a1i	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to 0 \in ℝ^{}$
34	2	adantr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to B \in ℝ^{}$
35	31	adantr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to B +_{𝑒} C \in ℝ^{}$
36		simpr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to 0 < B$
37	34	xaddid1d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to B +_{𝑒} 0 = B$
38		xleadd2a	$⊢ ((0 \in ℝ^{} \land C \in ℝ^{} \land B \in ℝ^{*}) \land 0 \leq C) \to B +_{𝑒} 0 \leq B +_{𝑒} C$
39	33 9 34 12 38	syl31anc	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to B +_{𝑒} 0 \leq B +_{𝑒} C$
40	37 39	eqbrtrrd	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to B \leq B +_{𝑒} C$
41	33 34 35 36 40	xrltletrd	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to 0 < B +_{𝑒} C$
42		xmulpnf2	$⊢ (B +_{𝑒} C \in ℝ^{*} \land 0 < B +_{𝑒} C) \to +∞ \cdot_{𝑒} (B +_{𝑒} C) = +∞$
43	31 41 42	syl2an2r	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to +∞ \cdot_{𝑒} (B +_{𝑒} C) = +∞$
44	29 43	sylan9eqr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = +∞$
45	21 28 44	3eqtr4rd	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
46		mnfxr	$⊢ −∞ \in ℝ^{*}$
47		xmulcl	$⊢ (−∞ \in ℝ^{} \land C \in ℝ^{}) \to −∞ \cdot_{𝑒} C \in ℝ^{*}$
48	46 9 47	sylancr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to −∞ \cdot_{𝑒} C \in ℝ^{}$
49		xnegmnf	$⊢ - −∞ = +∞$
50	49	oveq1i	$⊢ (- −∞) \cdot_{𝑒} C = +∞ \cdot_{𝑒} C$
51		xmulneg1	$⊢ (−∞ \in ℝ^{} \land C \in ℝ^{}) \to (- −∞) \cdot_{𝑒} C = - (−∞ \cdot_{𝑒} C)$
52	46 9 51	sylancr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (- −∞) \cdot_{𝑒} C = - (−∞ \cdot_{𝑒} C)$
53	50 52	syl5reqr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to - (−∞ \cdot_{𝑒} C) = +∞ \cdot_{𝑒} C$
54		xnegpnf	$⊢ - +∞ = −∞$
55	54	a1i	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to - +∞ = −∞$
56	53 55	eqeq12d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (- (−∞ \cdot_{𝑒} C) = - +∞ \leftrightarrow +∞ \cdot_{𝑒} C = −∞)$
57		xneg11	$⊢ (−∞ \cdot_{𝑒} C \in ℝ^{} \land +∞ \in ℝ^{}) \to (- (−∞ \cdot_{𝑒} C) = - +∞ \leftrightarrow −∞ \cdot_{𝑒} C = +∞)$
58	48 8 57	sylancl	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (- (−∞ \cdot_{𝑒} C) = - +∞ \leftrightarrow −∞ \cdot_{𝑒} C = +∞)$
59	56 58	bitr3d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (+∞ \cdot_{𝑒} C = −∞ \leftrightarrow −∞ \cdot_{𝑒} C = +∞)$
60	59	necon3bid	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (+∞ \cdot_{𝑒} C \neq −∞ \leftrightarrow −∞ \cdot_{𝑒} C \neq +∞)$
61	18 60	mpbid	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to −∞ \cdot_{𝑒} C \neq +∞$
62		xaddmnf2	$⊢ (−∞ \cdot_{𝑒} C \in ℝ^{*} \land −∞ \cdot_{𝑒} C \neq +∞) \to −∞ +_{𝑒} (−∞ \cdot_{𝑒} C) = −∞$
63	48 61 62	syl2anc	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to −∞ +_{𝑒} (−∞ \cdot_{𝑒} C) = −∞$
64	63	adantr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = −∞) \to −∞ +_{𝑒} (−∞ \cdot_{𝑒} C) = −∞$
65		oveq1	$⊢ A = −∞ \to A \cdot_{𝑒} B = −∞ \cdot_{𝑒} B$
66		oveq1	$⊢ A = −∞ \to A \cdot_{𝑒} C = −∞ \cdot_{𝑒} C$
67	65 66	oveq12d	$⊢ A = −∞ \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (−∞ \cdot_{𝑒} B) +_{𝑒} (−∞ \cdot_{𝑒} C)$
68		xmulmnf2	$⊢ (B \in ℝ^{*} \land 0 < B) \to −∞ \cdot_{𝑒} B = −∞$
69	2 68	sylan	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to −∞ \cdot_{𝑒} B = −∞$
70	69	oveq1d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (−∞ \cdot_{𝑒} B) +_{𝑒} (−∞ \cdot_{𝑒} C) = −∞ +_{𝑒} (−∞ \cdot_{𝑒} C)$
71	67 70	sylan9eqr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = −∞ +_{𝑒} (−∞ \cdot_{𝑒} C)$
72		oveq1	$⊢ A = −∞ \to A \cdot_{𝑒} (B +_{𝑒} C) = −∞ \cdot_{𝑒} (B +_{𝑒} C)$
73		xmulmnf2	$⊢ (B +_{𝑒} C \in ℝ^{*} \land 0 < B +_{𝑒} C) \to −∞ \cdot_{𝑒} (B +_{𝑒} C) = −∞$
74	31 41 73	syl2an2r	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to −∞ \cdot_{𝑒} (B +_{𝑒} C) = −∞$
75	72 74	sylan9eqr	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = −∞$
76	64 71 75	3eqtr4rd	$⊢ (((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \land A = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
77		simpl1	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 < B) \to A \in ℝ^{}$
78		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
79	77 78	sylib	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
80	7 45 76 79	mpjao3dan	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 < B) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
81		simp1	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \to A \in ℝ^{}$
82		xmulcl	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to A \cdot_{𝑒} C \in ℝ^{*}$
83	81 4 82	syl2anc	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \to A \cdot_{𝑒} C \in ℝ^{}$
84	83	adantr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{} \land 0 \leq C)) \land 0 = B) \to A \cdot_{𝑒} C \in ℝ^{}$
85		xaddid2	$⊢ A \cdot_{𝑒} C \in ℝ^{*} \to 0 +_{𝑒} (A \cdot_{𝑒} C) = A \cdot_{𝑒} C$
86	84 85	syl	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 = B) \to 0 +_{𝑒} (A \cdot_{𝑒} C) = A \cdot_{𝑒} C$
87		oveq2	$⊢ 0 = B \to A \cdot_{𝑒} 0 = A \cdot_{𝑒} B$
88	87	eqcomd	$⊢ 0 = B \to A \cdot_{𝑒} B = A \cdot_{𝑒} 0$
89		xmul01	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = 0$
90	89	3ad2ant1	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to A \cdot_{𝑒} 0 = 0$
91	88 90	sylan9eqr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 = B) \to A \cdot_{𝑒} B = 0$
92	91	oveq1d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 = B) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = 0 +_{𝑒} (A \cdot_{𝑒} C)$
93		oveq1	$⊢ 0 = B \to 0 +_{𝑒} C = B +_{𝑒} C$
94	93	eqcomd	$⊢ 0 = B \to B +_{𝑒} C = 0 +_{𝑒} C$
95		xaddid2	$⊢ C \in ℝ^{*} \to 0 +_{𝑒} C = C$
96	4 95	syl	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to 0 +_{𝑒} C = C$
97	94 96	sylan9eqr	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 = B) \to B +_{𝑒} C = C$
98	97	oveq2d	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 = B) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} C$
99	86 92 98	3eqtr4rd	$⊢ ((A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \land 0 = B) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
100		simp2r	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to 0 \leq B$
101		xrleloe	$⊢ (0 \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
102	32 2 101	sylancr	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
103	100 102	mpbid	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to (0 < B \lor 0 = B)$
104	80 99 103	mpjaodan	$⊢ (A \in ℝ^{} \land (B \in ℝ^{} \land 0 \leq B) \land (C \in ℝ^{*} \land 0 \leq C)) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$

Metamath Proof Explorer

Theorem xadddi2

Proof