xadddilem

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

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to A \in ℝ$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		recn	$⊢ B \in ℝ \to B \in ℂ$
4		recn	$⊢ C \in ℝ \to C \in ℂ$
5		adddi	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A (B + C) = A B + A C$
6	2 3 4 5	syl3an	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A (B + C) = A B + A C$
7	6	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A (B + C) = A B + A C$
8		readdcl	$⊢ (B \in ℝ \land C \in ℝ) \to B + C \in ℝ$
9		rexmul	$⊢ (A \in ℝ \land B + C \in ℝ) \to A \cdot_{𝑒} (B + C) = A (B + C)$
10	8 9	sylan2	$⊢ (A \in ℝ \land (B \in ℝ \land C \in ℝ)) \to A \cdot_{𝑒} (B + C) = A (B + C)$
11	10	anassrs	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} (B + C) = A (B + C)$
12		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
13	12	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A B \in ℝ$
14		remulcl	$⊢ (A \in ℝ \land C \in ℝ) \to A C \in ℝ$
15	14	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A C \in ℝ$
16	13 15	rexaddd	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A B +_{𝑒} A C = A B + A C$
17	7 11 16	3eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} (B + C) = A B +_{𝑒} A C$
18		rexadd	$⊢ (B \in ℝ \land C \in ℝ) \to B +_{𝑒} C = B + C$
19	18	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to B +_{𝑒} C = B + C$
20	19	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} (B + C)$
21		rexmul	$⊢ (A \in ℝ \land B \in ℝ) \to A \cdot_{𝑒} B = A B$
22	21	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} B = A B$
23		rexmul	$⊢ (A \in ℝ \land C \in ℝ) \to A \cdot_{𝑒} C = A C$
24	23	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} C = A C$
25	22 24	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = A B +_{𝑒} A C$
26	17 20 25	3eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
27	1 26	sylanl1	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
28		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
29	28	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \to A \in ℝ^{*}$
30		xmulpnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$
31	29 30	sylan	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$
32	31	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to A \cdot_{𝑒} +∞ = +∞$
33	21 12	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ) \to A \cdot_{𝑒} B \in ℝ$
34	1 33	sylan	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to A \cdot_{𝑒} B \in ℝ$
35		rexr	$⊢ A \cdot_{𝑒} B \in ℝ \to A \cdot_{𝑒} B \in ℝ^{*}$
36		renemnf	$⊢ A \cdot_{𝑒} B \in ℝ \to A \cdot_{𝑒} B \neq −∞$
37		xaddpnf1	$⊢ (A \cdot_{𝑒} B \in ℝ^{*} \land A \cdot_{𝑒} B \neq −∞) \to (A \cdot_{𝑒} B) +_{𝑒} +∞ = +∞$
38	35 36 37	syl2anc	$⊢ A \cdot_{𝑒} B \in ℝ \to (A \cdot_{𝑒} B) +_{𝑒} +∞ = +∞$
39	34 38	syl	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to (A \cdot_{𝑒} B) +_{𝑒} +∞ = +∞$
40	32 39	eqtr4d	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to A \cdot_{𝑒} +∞ = (A \cdot_{𝑒} B) +_{𝑒} +∞$
41	40	adantr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = +∞) \to A \cdot_{𝑒} +∞ = (A \cdot_{𝑒} B) +_{𝑒} +∞$
42		oveq2	$⊢ C = +∞ \to B +_{𝑒} C = B +_{𝑒} +∞$
43		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
44		renemnf	$⊢ B \in ℝ \to B \neq −∞$
45		xaddpnf1	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to B +_{𝑒} +∞ = +∞$
46	43 44 45	syl2anc	$⊢ B \in ℝ \to B +_{𝑒} +∞ = +∞$
47	46	adantl	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to B +_{𝑒} +∞ = +∞$
48	42 47	sylan9eqr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = +∞) \to B +_{𝑒} C = +∞$
49	48	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} +∞$
50		oveq2	$⊢ C = +∞ \to A \cdot_{𝑒} C = A \cdot_{𝑒} +∞$
51	50 32	sylan9eqr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = +∞) \to A \cdot_{𝑒} C = +∞$
52	51	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = +∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} +∞$
53	41 49 52	3eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
54		xmulmnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} −∞ = −∞$
55	29 54	sylan	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to A \cdot_{𝑒} −∞ = −∞$
56	55	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to A \cdot_{𝑒} −∞ = −∞$
57	56	adantr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to A \cdot_{𝑒} −∞ = −∞$
58	34	adantr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to A \cdot_{𝑒} B \in ℝ$
59		renepnf	$⊢ A \cdot_{𝑒} B \in ℝ \to A \cdot_{𝑒} B \neq +∞$
60		xaddmnf1	$⊢ (A \cdot_{𝑒} B \in ℝ^{*} \land A \cdot_{𝑒} B \neq +∞) \to (A \cdot_{𝑒} B) +_{𝑒} −∞ = −∞$
61	35 59 60	syl2anc	$⊢ A \cdot_{𝑒} B \in ℝ \to (A \cdot_{𝑒} B) +_{𝑒} −∞ = −∞$
62	58 61	syl	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} −∞ = −∞$
63	57 62	eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to A \cdot_{𝑒} −∞ = (A \cdot_{𝑒} B) +_{𝑒} −∞$
64		oveq2	$⊢ C = −∞ \to B +_{𝑒} C = B +_{𝑒} −∞$
65		renepnf	$⊢ B \in ℝ \to B \neq +∞$
66		xaddmnf1	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to B +_{𝑒} −∞ = −∞$
67	43 65 66	syl2anc	$⊢ B \in ℝ \to B +_{𝑒} −∞ = −∞$
68	67	adantl	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to B +_{𝑒} −∞ = −∞$
69	64 68	sylan9eqr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to B +_{𝑒} C = −∞$
70	69	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} −∞$
71		oveq2	$⊢ C = −∞ \to A \cdot_{𝑒} C = A \cdot_{𝑒} −∞$
72	71 56	sylan9eqr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to A \cdot_{𝑒} C = −∞$
73	72	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} −∞$
74	63 70 73	3eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
75		simpl3	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to C \in ℝ^{*}$
76		elxr	$⊢ C \in ℝ^{*} \leftrightarrow (C \in ℝ \lor C = +∞ \lor C = −∞)$
77	75 76	sylib	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (C \in ℝ \lor C = +∞ \lor C = −∞)$
78	77	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to (C \in ℝ \lor C = +∞ \lor C = −∞)$
79	27 53 74 78	mpjao3dan	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
80	31	ad2antrr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to A \cdot_{𝑒} +∞ = +∞$
81	1	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \to A \in ℝ$
82	23 14	eqeltrd	$⊢ (A \in ℝ \land C \in ℝ) \to A \cdot_{𝑒} C \in ℝ$
83	81 82	sylan	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to A \cdot_{𝑒} C \in ℝ$
84		rexr	$⊢ A \cdot_{𝑒} C \in ℝ \to A \cdot_{𝑒} C \in ℝ^{*}$
85		renemnf	$⊢ A \cdot_{𝑒} C \in ℝ \to A \cdot_{𝑒} C \neq −∞$
86		xaddpnf2	$⊢ (A \cdot_{𝑒} C \in ℝ^{*} \land A \cdot_{𝑒} C \neq −∞) \to +∞ +_{𝑒} (A \cdot_{𝑒} C) = +∞$
87	84 85 86	syl2anc	$⊢ A \cdot_{𝑒} C \in ℝ \to +∞ +_{𝑒} (A \cdot_{𝑒} C) = +∞$
88	83 87	syl	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to +∞ +_{𝑒} (A \cdot_{𝑒} C) = +∞$
89	80 88	eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to A \cdot_{𝑒} +∞ = +∞ +_{𝑒} (A \cdot_{𝑒} C)$
90		simpr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \to B = +∞$
91	90	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \to B +_{𝑒} C = +∞ +_{𝑒} C$
92		rexr	$⊢ C \in ℝ \to C \in ℝ^{*}$
93		renemnf	$⊢ C \in ℝ \to C \neq −∞$
94		xaddpnf2	$⊢ (C \in ℝ^{*} \land C \neq −∞) \to +∞ +_{𝑒} C = +∞$
95	92 93 94	syl2anc	$⊢ C \in ℝ \to +∞ +_{𝑒} C = +∞$
96	91 95	sylan9eq	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to B +_{𝑒} C = +∞$
97	96	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} +∞$
98		oveq2	$⊢ B = +∞ \to A \cdot_{𝑒} B = A \cdot_{𝑒} +∞$
99	98 31	sylan9eqr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \to A \cdot_{𝑒} B = +∞$
100	99	adantr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to A \cdot_{𝑒} B = +∞$
101	100	oveq1d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = +∞ +_{𝑒} (A \cdot_{𝑒} C)$
102	89 97 101	3eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
103		pnfxr	$⊢ +∞ \in ℝ^{*}$
104		pnfnemnf	$⊢ +∞ \neq −∞$
105		xaddpnf1	$⊢ (+∞ \in ℝ^{*} \land +∞ \neq −∞) \to +∞ +_{𝑒} +∞ = +∞$
106	103 104 105	mp2an	$⊢ +∞ +_{𝑒} +∞ = +∞$
107	31 31	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} +∞) = +∞ +_{𝑒} +∞$
108	106 107 31	3eqtr4a	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} +∞) = A \cdot_{𝑒} +∞$
109	108	ad2antrr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = +∞) \to (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} +∞) = A \cdot_{𝑒} +∞$
110	98 50	oveqan12d	$⊢ (B = +∞ \land C = +∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} +∞)$
111	110	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = +∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} +∞)$
112		oveq12	$⊢ (B = +∞ \land C = +∞) \to B +_{𝑒} C = +∞ +_{𝑒} +∞$
113	112 106	eqtrdi	$⊢ (B = +∞ \land C = +∞) \to B +_{𝑒} C = +∞$
114	113	oveq2d	$⊢ (B = +∞ \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} +∞$
115	114	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} +∞$
116	109 111 115	3eqtr4rd	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
117		pnfaddmnf	$⊢ +∞ +_{𝑒} −∞ = 0$
118	31 55	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} −∞) = +∞ +_{𝑒} −∞$
119		xmul01	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = 0$
120	1 28 119	3syl	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to A \cdot_{𝑒} 0 = 0$
121	117 118 120	3eqtr4a	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} −∞) = A \cdot_{𝑒} 0$
122	121	ad2antrr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = −∞) \to (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} −∞) = A \cdot_{𝑒} 0$
123	98 71	oveqan12d	$⊢ (B = +∞ \land C = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} −∞)$
124	123	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} +∞) +_{𝑒} (A \cdot_{𝑒} −∞)$
125		oveq12	$⊢ (B = +∞ \land C = −∞) \to B +_{𝑒} C = +∞ +_{𝑒} −∞$
126	125 117	eqtrdi	$⊢ (B = +∞ \land C = −∞) \to B +_{𝑒} C = 0$
127	126	oveq2d	$⊢ (B = +∞ \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} 0$
128	127	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} 0$
129	122 124 128	3eqtr4rd	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
130	77	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \to (C \in ℝ \lor C = +∞ \lor C = −∞)$
131	102 116 129 130	mpjao3dan	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
132	55	ad2antrr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to A \cdot_{𝑒} −∞ = −∞$
133	1	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \to A \in ℝ$
134	133 82	sylan	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to A \cdot_{𝑒} C \in ℝ$
135		renepnf	$⊢ A \cdot_{𝑒} C \in ℝ \to A \cdot_{𝑒} C \neq +∞$
136		xaddmnf2	$⊢ (A \cdot_{𝑒} C \in ℝ^{*} \land A \cdot_{𝑒} C \neq +∞) \to −∞ +_{𝑒} (A \cdot_{𝑒} C) = −∞$
137	84 135 136	syl2anc	$⊢ A \cdot_{𝑒} C \in ℝ \to −∞ +_{𝑒} (A \cdot_{𝑒} C) = −∞$
138	134 137	syl	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to −∞ +_{𝑒} (A \cdot_{𝑒} C) = −∞$
139	132 138	eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to A \cdot_{𝑒} −∞ = −∞ +_{𝑒} (A \cdot_{𝑒} C)$
140		simpr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \to B = −∞$
141	140	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \to B +_{𝑒} C = −∞ +_{𝑒} C$
142		renepnf	$⊢ C \in ℝ \to C \neq +∞$
143		xaddmnf2	$⊢ (C \in ℝ^{*} \land C \neq +∞) \to −∞ +_{𝑒} C = −∞$
144	92 142 143	syl2anc	$⊢ C \in ℝ \to −∞ +_{𝑒} C = −∞$
145	141 144	sylan9eq	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to B +_{𝑒} C = −∞$
146	145	oveq2d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} −∞$
147		oveq2	$⊢ B = −∞ \to A \cdot_{𝑒} B = A \cdot_{𝑒} −∞$
148	147 55	sylan9eqr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \to A \cdot_{𝑒} B = −∞$
149	148	adantr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to A \cdot_{𝑒} B = −∞$
150	149	oveq1d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = −∞ +_{𝑒} (A \cdot_{𝑒} C)$
151	139 146 150	3eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C \in ℝ) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
152	55 31	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} +∞) = −∞ +_{𝑒} +∞$
153		mnfaddpnf	$⊢ −∞ +_{𝑒} +∞ = 0$
154	152 153	eqtrdi	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} +∞) = 0$
155	120 154	eqtr4d	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to A \cdot_{𝑒} 0 = (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} +∞)$
156	155	ad2antrr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = +∞) \to A \cdot_{𝑒} 0 = (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} +∞)$
157		oveq12	$⊢ (B = −∞ \land C = +∞) \to B +_{𝑒} C = −∞ +_{𝑒} +∞$
158	157 153	eqtrdi	$⊢ (B = −∞ \land C = +∞) \to B +_{𝑒} C = 0$
159	158	oveq2d	$⊢ (B = −∞ \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} 0$
160	159	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} 0$
161	147 50	oveqan12d	$⊢ (B = −∞ \land C = +∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} +∞)$
162	161	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = +∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} +∞)$
163	156 160 162	3eqtr4d	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = +∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
164		mnfxr	$⊢ −∞ \in ℝ^{*}$
165		mnfnepnf	$⊢ −∞ \neq +∞$
166		xaddmnf1	$⊢ (−∞ \in ℝ^{*} \land −∞ \neq +∞) \to −∞ +_{𝑒} −∞ = −∞$
167	164 165 166	mp2an	$⊢ −∞ +_{𝑒} −∞ = −∞$
168	55 55	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} −∞) = −∞ +_{𝑒} −∞$
169	167 168 55	3eqtr4a	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} −∞) = A \cdot_{𝑒} −∞$
170	169	ad2antrr	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = −∞) \to (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} −∞) = A \cdot_{𝑒} −∞$
171	147 71	oveqan12d	$⊢ (B = −∞ \land C = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} −∞)$
172	171	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = −∞) \to (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C) = (A \cdot_{𝑒} −∞) +_{𝑒} (A \cdot_{𝑒} −∞)$
173		oveq12	$⊢ (B = −∞ \land C = −∞) \to B +_{𝑒} C = −∞ +_{𝑒} −∞$
174	173 167	eqtrdi	$⊢ (B = −∞ \land C = −∞) \to B +_{𝑒} C = −∞$
175	174	oveq2d	$⊢ (B = −∞ \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} −∞$
176	175	adantll	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = A \cdot_{𝑒} −∞$
177	170 172 176	3eqtr4rd	$⊢ ((((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \land C = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
178	77	adantr	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \to (C \in ℝ \lor C = +∞ \lor C = −∞)$
179	151 163 177 178	mpjao3dan	$⊢ (((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \land B = −∞) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$
180		simpl2	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to B \in ℝ^{*}$
181		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
182	180 181	sylib	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
183	79 131 179 182	mpjao3dan	$⊢ ((A \in ℝ \land B \in ℝ^{} \land C \in ℝ^{}) \land 0 < A) \to A \cdot_{𝑒} (B +_{𝑒} C) = (A \cdot_{𝑒} B) +_{𝑒} (A \cdot_{𝑒} C)$

Metamath Proof Explorer

Theorem xadddilem

Proof