Theorem xnegdi 13234

Description: Extended real version of negdi 11524. (Contributed by Mario Carneiro, 20-Aug-2015.)

Assertion

Ref	Expression
xnegdi	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))

Proof of Theorem xnegdi

Step	Hyp	Ref	Expression
1		elxr 13103	. 2 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13103	. . . 4 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 11206	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 11206	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		negdi 11524	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
6	3, 4, 5	syl2an 595	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
7		readdcl 11199	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
8		rexneg 13197	. . . . . . . 8 ⊢ ((𝐴 + 𝐵) ∈ ℝ → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
9	7, 8	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
10		renegcl 11530	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
11		renegcl 11530	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
12		rexadd 13218	. . . . . . . 8 ⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
13	10, 11, 12	syl2an 595	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
14	6, 9, 13	3eqtr4d 2781	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = (-𝐴 +𝑒 -𝐵))
15		rexadd 13218	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
16		xnegeq 13193	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = (𝐴 + 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
17	15, 16	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
18		rexneg 13197	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
19		rexneg 13197	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → -𝑒𝐵 = -𝐵)
20	18, 19	oveqan12d 7431	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝐴 +𝑒 -𝐵))
21	14, 17, 20	3eqtr4d 2781	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
22		xnegpnf 13195	. . . . . 6 ⊢ -𝑒+∞ = -∞
23		oveq2 7420	. . . . . . . 8 ⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 +∞))
24		rexr 11267	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
25		renemnf 11270	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
26		xaddpnf1 13212	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
27	24, 25, 26	syl2anc 583	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞) = +∞)
28	23, 27	sylan9eqr 2793	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞)
29		xnegeq 13193	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = +∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
30	28, 29	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
31		xnegeq 13193	. . . . . . . . 9 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -𝑒+∞)
32	31, 22	eqtrdi 2787	. . . . . . . 8 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -∞)
33	32	oveq2d 7428	. . . . . . 7 ⊢ (𝐵 = +∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 -∞))
34	18, 10	eqeltrd 2832	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
35		rexr 11267	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ*)
36		renepnf 11269	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ +∞)
37		xaddmnf1 13214	. . . . . . . . 9 ⊢ ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ +∞) → (-𝑒𝐴 +𝑒 -∞) = -∞)
38	35, 36, 37	syl2anc 583	. . . . . . . 8 ⊢ (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
39	34, 38	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
40	33, 39	sylan9eqr 2793	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = -∞)
41	22, 30, 40	3eqtr4a 2797	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
42		xnegmnf 13196	. . . . . 6 ⊢ -𝑒-∞ = +∞
43		oveq2 7420	. . . . . . . 8 ⊢ (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 -∞))
44		renepnf 11269	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
45		xaddmnf1 13214	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
46	24, 44, 45	syl2anc 583	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞) = -∞)
47	43, 46	sylan9eqr 2793	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞)
48		xnegeq 13193	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = -∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
49	47, 48	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
50		xnegeq 13193	. . . . . . . . 9 ⊢ (𝐵 = -∞ → -𝑒𝐵 = -𝑒-∞)
51	50, 42	eqtrdi 2787	. . . . . . . 8 ⊢ (𝐵 = -∞ → -𝑒𝐵 = +∞)
52	51	oveq2d 7428	. . . . . . 7 ⊢ (𝐵 = -∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 +∞))
53		renemnf 11270	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ -∞)
54		xaddpnf1 13212	. . . . . . . . 9 ⊢ ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ -∞) → (-𝑒𝐴 +𝑒 +∞) = +∞)
55	35, 53, 54	syl2anc 583	. . . . . . . 8 ⊢ (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
56	34, 55	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
57	52, 56	sylan9eqr 2793	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = +∞)
58	42, 49, 57	3eqtr4a 2797	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
59	21, 41, 58	3jaodan 1429	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
60	2, 59	sylan2b 593	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
61		xneg0 13198	. . . . . . 7 ⊢ -𝑒0 = 0
62		simpr 484	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → 𝐵 = -∞)
63	62	oveq2d 7428	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (+∞ +𝑒 𝐵) = (+∞ +𝑒 -∞))
64		pnfaddmnf 13216	. . . . . . . . 9 ⊢ (+∞ +𝑒 -∞) = 0
65	63, 64	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (+∞ +𝑒 𝐵) = 0)
66		xnegeq 13193	. . . . . . . 8 ⊢ ((+∞ +𝑒 𝐵) = 0 → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
67	65, 66	syl 17	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
68	51	adantl 481	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒𝐵 = +∞)
69	68	oveq2d 7428	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = (-∞ +𝑒 +∞))
70		mnfaddpnf 13217	. . . . . . . 8 ⊢ (-∞ +𝑒 +∞) = 0
71	69, 70	eqtrdi 2787	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = 0)
72	61, 67, 71	3eqtr4a 2797	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
73		xaddpnf2 13213	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
74		xnegeq 13193	. . . . . . . 8 ⊢ ((+∞ +𝑒 𝐵) = +∞ → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
75	73, 74	syl 17	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
76		xnegcl 13199	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → -𝑒𝐵 ∈ ℝ*)
77		xnegeq 13193	. . . . . . . . . . . 12 ⊢ (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -𝑒+∞)
78	77, 22	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -∞)
79		xnegneg 13200	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ* → -𝑒-𝑒𝐵 = 𝐵)
80	79	eqeq1d 2733	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = -∞ ↔ 𝐵 = -∞))
81	78, 80	imbitrid 243	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (-𝑒𝐵 = +∞ → 𝐵 = -∞))
82	81	necon3d 2960	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → (𝐵 ≠ -∞ → -𝑒𝐵 ≠ +∞))
83	82	imp 406	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒𝐵 ≠ +∞)
84		xaddmnf2 13215	. . . . . . . 8 ⊢ ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ +∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
85	76, 83, 84	syl2an2r 682	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
86	22, 75, 85	3eqtr4a 2797	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
87	72, 86	pm2.61dane 3028	. . . . 5 ⊢ (𝐵 ∈ ℝ* → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
88	87	adantl 481	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
89		simpl 482	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = +∞)
90	89	oveq1d 7427	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
91		xnegeq 13193	. . . . 5 ⊢ ((𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
92	90, 91	syl 17	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
93		xnegeq 13193	. . . . . . 7 ⊢ (𝐴 = +∞ → -𝑒𝐴 = -𝑒+∞)
94	93	adantr 480	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒+∞)
95	94, 22	eqtrdi 2787	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -∞)
96	95	oveq1d 7427	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-∞ +𝑒 -𝑒𝐵))
97	88, 92, 96	3eqtr4d 2781	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
98		simpr 484	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → 𝐵 = +∞)
99	98	oveq2d 7428	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (-∞ +𝑒 𝐵) = (-∞ +𝑒 +∞))
100	99, 70	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (-∞ +𝑒 𝐵) = 0)
101		xnegeq 13193	. . . . . . . 8 ⊢ ((-∞ +𝑒 𝐵) = 0 → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
102	100, 101	syl 17	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
103	32	adantl 481	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒𝐵 = -∞)
104	103	oveq2d 7428	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = (+∞ +𝑒 -∞))
105	104, 64	eqtrdi 2787	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = 0)
106	61, 102, 105	3eqtr4a 2797	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
107		xaddmnf2 13215	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
108		xnegeq 13193	. . . . . . . 8 ⊢ ((-∞ +𝑒 𝐵) = -∞ → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
109	107, 108	syl 17	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
110		xnegeq 13193	. . . . . . . . . . . 12 ⊢ (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = -𝑒-∞)
111	110, 42	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = +∞)
112	79	eqeq1d 2733	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = +∞ ↔ 𝐵 = +∞))
113	111, 112	imbitrid 243	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (-𝑒𝐵 = -∞ → 𝐵 = +∞))
114	113	necon3d 2960	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → (𝐵 ≠ +∞ → -𝑒𝐵 ≠ -∞))
115	114	imp 406	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒𝐵 ≠ -∞)
116		xaddpnf2 13213	. . . . . . . 8 ⊢ ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ -∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
117	76, 115, 116	syl2an2r 682	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
118	42, 109, 117	3eqtr4a 2797	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
119	106, 118	pm2.61dane 3028	. . . . 5 ⊢ (𝐵 ∈ ℝ* → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
120	119	adantl 481	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
121		simpl 482	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = -∞)
122	121	oveq1d 7427	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
123		xnegeq 13193	. . . . 5 ⊢ ((𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
124	122, 123	syl 17	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
125		xnegeq 13193	. . . . . . 7 ⊢ (𝐴 = -∞ → -𝑒𝐴 = -𝑒-∞)
126	125	adantr 480	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒-∞)
127	126, 42	eqtrdi 2787	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = +∞)
128	127	oveq1d 7427	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (+∞ +𝑒 -𝑒𝐵))
129	120, 124, 128	3eqtr4d 2781	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
130	60, 97, 129	3jaoian 1428	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
131	1, 130	sylanb 580	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   = wceq 1540   ∈ wcel 2105   ≠ wne 2939  (class class class)co 7412  ℂcc 11114  ℝcr 11115  0cc0 11116   + caddc 11119  +∞cpnf 11252  -∞cmnf 11253  ℝ^*cxr 11254  -cneg 11452  -_𝑒cxne 13096   +_𝑒 cxad 13097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-sub 11453  df-neg 11454  df-xneg 13099  df-xadd 13100

This theorem is referenced by:  xaddass2  13236  xposdif  13248  xadddi  13281  xrsxmet  24645