Theorem xadddi2 12444

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

Assertion

Ref	Expression
xadddi2	⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))

Proof of Theorem xadddi2

Step	Hyp	Ref	Expression
1		simpr 479	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)
2		simp2l 1213	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → 𝐵 ∈ ℝ*)
3	2	ad2antrr 716	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈ ℝ*)
4		simp3l 1215	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → 𝐶 ∈ ℝ*)
5	4	ad2antrr 716	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐶 ∈ ℝ*)
6		xadddi 12442	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
7	1, 3, 5, 6	syl3anc 1439	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
8		pnfxr 10432	. . . . . 6 ⊢ +∞ ∈ ℝ*
9	4	adantr 474	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 𝐶 ∈ ℝ*)
10		xmulcl 12420	. . . . . 6 ⊢ ((+∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (+∞ ·e 𝐶) ∈ ℝ*)
11	8, 9, 10	sylancr 581	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (+∞ ·e 𝐶) ∈ ℝ*)
12		simpl3r 1260	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 0 ≤ 𝐶)
13		0lepnf 12282	. . . . . . . . 9 ⊢ 0 ≤ +∞
14		xmulge0 12431	. . . . . . . . 9 ⊢ (((+∞ ∈ ℝ* ∧ 0 ≤ +∞) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → 0 ≤ (+∞ ·e 𝐶))
15	8, 13, 14	mpanl12 692	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶) → 0 ≤ (+∞ ·e 𝐶))
16	4, 12, 15	syl2an2r 675	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 0 ≤ (+∞ ·e 𝐶))
17		ge0nemnf 12321	. . . . . . 7 ⊢ (((+∞ ·e 𝐶) ∈ ℝ* ∧ 0 ≤ (+∞ ·e 𝐶)) → (+∞ ·e 𝐶) ≠ -∞)
18	11, 16, 17	syl2anc 579	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (+∞ ·e 𝐶) ≠ -∞)
19	18	adantr 474	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞ ·e 𝐶) ≠ -∞)
20		xaddpnf2 12375	. . . . 5 ⊢ (((+∞ ·e 𝐶) ∈ ℝ* ∧ (+∞ ·e 𝐶) ≠ -∞) → (+∞ +𝑒 (+∞ ·e 𝐶)) = +∞)
21	11, 19, 20	syl2an2r 675	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞ +𝑒 (+∞ ·e 𝐶)) = +∞)
22		oveq1 6931	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐴 ·e 𝐵) = (+∞ ·e 𝐵))
23		oveq1 6931	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐴 ·e 𝐶) = (+∞ ·e 𝐶))
24	22, 23	oveq12d 6942	. . . . 5 ⊢ (𝐴 = +∞ → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((+∞ ·e 𝐵) +𝑒 (+∞ ·e 𝐶)))
25		xmulpnf2 12422	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 0 < 𝐵) → (+∞ ·e 𝐵) = +∞)
26	2, 25	sylan 575	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (+∞ ·e 𝐵) = +∞)
27	26	oveq1d 6939	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → ((+∞ ·e 𝐵) +𝑒 (+∞ ·e 𝐶)) = (+∞ +𝑒 (+∞ ·e 𝐶)))
28	24, 27	sylan9eqr 2836	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (+∞ +𝑒 (+∞ ·e 𝐶)))
29		oveq1 6931	. . . . 5 ⊢ (𝐴 = +∞ → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (+∞ ·e (𝐵 +𝑒 𝐶)))
30		xaddcl 12387	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
31	2, 4, 30	syl2anc 579	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
32		0xr 10425	. . . . . . . 8 ⊢ 0 ∈ ℝ*
33	32	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 0 ∈ ℝ*)
34	2	adantr 474	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 𝐵 ∈ ℝ*)
35	31	adantr 474	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
36		simpr 479	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 0 < 𝐵)
37	34	xaddid1d 12391	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 0) = 𝐵)
38		xleadd2a 12401	. . . . . . . . 9 ⊢ (((0 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 0 ≤ 𝐶) → (𝐵 +𝑒 0) ≤ (𝐵 +𝑒 𝐶))
39	33, 9, 34, 12, 38	syl31anc 1441	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 0) ≤ (𝐵 +𝑒 𝐶))
40	37, 39	eqbrtrrd 4912	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 𝐵 ≤ (𝐵 +𝑒 𝐶))
41	33, 34, 35, 36, 40	xrltletrd 12309	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 0 < (𝐵 +𝑒 𝐶))
42		xmulpnf2 12422	. . . . . 6 ⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ* ∧ 0 < (𝐵 +𝑒 𝐶)) → (+∞ ·e (𝐵 +𝑒 𝐶)) = +∞)
43	31, 41, 42	syl2an2r 675	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (+∞ ·e (𝐵 +𝑒 𝐶)) = +∞)
44	29, 43	sylan9eqr 2836	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = +∞)
45	21, 28, 44	3eqtr4rd 2825	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
46		mnfxr 10436	. . . . . . 7 ⊢ -∞ ∈ ℝ*
47		xmulcl 12420	. . . . . . 7 ⊢ ((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (-∞ ·e 𝐶) ∈ ℝ*)
48	46, 9, 47	sylancr 581	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-∞ ·e 𝐶) ∈ ℝ*)
49		xnegmnf 12358	. . . . . . . . . . . 12 ⊢ -𝑒-∞ = +∞
50	49	oveq1i 6934	. . . . . . . . . . 11 ⊢ (-𝑒-∞ ·e 𝐶) = (+∞ ·e 𝐶)
51		xmulneg1 12416	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (-𝑒-∞ ·e 𝐶) = -𝑒(-∞ ·e 𝐶))
52	46, 9, 51	sylancr 581	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-𝑒-∞ ·e 𝐶) = -𝑒(-∞ ·e 𝐶))
53	50, 52	syl5reqr 2829	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → -𝑒(-∞ ·e 𝐶) = (+∞ ·e 𝐶))
54		xnegpnf 12357	. . . . . . . . . . 11 ⊢ -𝑒+∞ = -∞
55	54	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → -𝑒+∞ = -∞)
56	53, 55	eqeq12d 2793	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔ (+∞ ·e 𝐶) = -∞))
57		xneg11 12363	. . . . . . . . . 10 ⊢ (((-∞ ·e 𝐶) ∈ ℝ* ∧ +∞ ∈ ℝ*) → (-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔ (-∞ ·e 𝐶) = +∞))
58	48, 8, 57	sylancl 580	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔ (-∞ ·e 𝐶) = +∞))
59	56, 58	bitr3d 273	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → ((+∞ ·e 𝐶) = -∞ ↔ (-∞ ·e 𝐶) = +∞))
60	59	necon3bid 3013	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → ((+∞ ·e 𝐶) ≠ -∞ ↔ (-∞ ·e 𝐶) ≠ +∞))
61	18, 60	mpbid 224	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-∞ ·e 𝐶) ≠ +∞)
62		xaddmnf2 12377	. . . . . 6 ⊢ (((-∞ ·e 𝐶) ∈ ℝ* ∧ (-∞ ·e 𝐶) ≠ +∞) → (-∞ +𝑒 (-∞ ·e 𝐶)) = -∞)
63	48, 61, 62	syl2anc 579	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-∞ +𝑒 (-∞ ·e 𝐶)) = -∞)
64	63	adantr 474	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (-∞ +𝑒 (-∞ ·e 𝐶)) = -∞)
65		oveq1 6931	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐴 ·e 𝐵) = (-∞ ·e 𝐵))
66		oveq1 6931	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐴 ·e 𝐶) = (-∞ ·e 𝐶))
67	65, 66	oveq12d 6942	. . . . 5 ⊢ (𝐴 = -∞ → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((-∞ ·e 𝐵) +𝑒 (-∞ ·e 𝐶)))
68		xmulmnf2 12424	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 0 < 𝐵) → (-∞ ·e 𝐵) = -∞)
69	2, 68	sylan 575	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-∞ ·e 𝐵) = -∞)
70	69	oveq1d 6939	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → ((-∞ ·e 𝐵) +𝑒 (-∞ ·e 𝐶)) = (-∞ +𝑒 (-∞ ·e 𝐶)))
71	67, 70	sylan9eqr 2836	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (-∞ +𝑒 (-∞ ·e 𝐶)))
72		oveq1 6931	. . . . 5 ⊢ (𝐴 = -∞ → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (-∞ ·e (𝐵 +𝑒 𝐶)))
73		xmulmnf2 12424	. . . . . 6 ⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ* ∧ 0 < (𝐵 +𝑒 𝐶)) → (-∞ ·e (𝐵 +𝑒 𝐶)) = -∞)
74	31, 41, 73	syl2an2r 675	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (-∞ ·e (𝐵 +𝑒 𝐶)) = -∞)
75	72, 74	sylan9eqr 2836	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = -∞)
76	64, 71, 75	3eqtr4rd 2825	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
77		simpl1 1199	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → 𝐴 ∈ ℝ*)
78		elxr 12266	. . . 4 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
79	77, 78	sylib 210	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
80	7, 45, 76, 79	mpjao3dan 1505	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 < 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
81		simp1 1127	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → 𝐴 ∈ ℝ*)
82		xmulcl 12420	. . . . . 6 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 𝐶) ∈ ℝ*)
83	81, 4, 82	syl2anc 579	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e 𝐶) ∈ ℝ*)
84	83	adantr 474	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐶) ∈ ℝ*)
85		xaddid2 12390	. . . 4 ⊢ ((𝐴 ·e 𝐶) ∈ ℝ* → (0 +𝑒 (𝐴 ·e 𝐶)) = (𝐴 ·e 𝐶))
86	84, 85	syl 17	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → (0 +𝑒 (𝐴 ·e 𝐶)) = (𝐴 ·e 𝐶))
87		oveq2 6932	. . . . . 6 ⊢ (0 = 𝐵 → (𝐴 ·e 0) = (𝐴 ·e 𝐵))
88	87	eqcomd 2784	. . . . 5 ⊢ (0 = 𝐵 → (𝐴 ·e 𝐵) = (𝐴 ·e 0))
89		xmul01 12414	. . . . . 6 ⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0)
90	89	3ad2ant1 1124	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e 0) = 0)
91	88, 90	sylan9eqr 2836	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐵) = 0)
92	91	oveq1d 6939	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (0 +𝑒 (𝐴 ·e 𝐶)))
93		oveq1 6931	. . . . . 6 ⊢ (0 = 𝐵 → (0 +𝑒 𝐶) = (𝐵 +𝑒 𝐶))
94	93	eqcomd 2784	. . . . 5 ⊢ (0 = 𝐵 → (𝐵 +𝑒 𝐶) = (0 +𝑒 𝐶))
95		xaddid2 12390	. . . . . 6 ⊢ (𝐶 ∈ ℝ* → (0 +𝑒 𝐶) = 𝐶)
96	4, 95	syl 17	. . . . 5 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (0 +𝑒 𝐶) = 𝐶)
97	94, 96	sylan9eqr 2836	. . . 4 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → (𝐵 +𝑒 𝐶) = 𝐶)
98	97	oveq2d 6940	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 𝐶))
99	86, 92, 98	3eqtr4rd 2825	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
100		simp2r 1214	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → 0 ≤ 𝐵)
101		xrleloe 12292	. . . 4 ⊢ ((0 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵)))
102	32, 2, 101	sylancr 581	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵)))
103	100, 102	mpbid 224	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (0 < 𝐵 ∨ 0 = 𝐵))
104	80, 99, 103	mpjaodan 944	1 ⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   ∨ w3o 1070   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107   ≠ wne 2969   class class class wbr 4888  (class class class)co 6924  ℝcr 10273  0cc0 10274  +∞cpnf 10410  -∞cmnf 10411  ℝ^*cxr 10412   < clt 10413   ≤ cle 10414  -_𝑒cxne 12259   +_𝑒 cxad 12260   ·_e cxmu 12261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-po 5276  df-so 5277  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-1st 7447  df-2nd 7448  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-xneg 12262  df-xadd 12263  df-xmul 12264

This theorem is referenced by:  xadddi2r  12445