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

Proof

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