Theorem xnegdi 9855

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

Assertion

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

Proof of Theorem xnegdi

Step	Hyp	Ref	Expression
1		elxr 9763	. 2 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 9763	. . . 4 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 7935	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 7935	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		negdi 8204	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
6	3, 4, 5	syl2an 289	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
7		readdcl 7928	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
8		rexneg 9817	. . . . . . . 8 ⊢ ((𝐴 + 𝐵) ∈ ℝ → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
9	7, 8	syl 14	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
10		renegcl 8208	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
11		renegcl 8208	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
12		rexadd 9839	. . . . . . . 8 ⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
13	10, 11, 12	syl2an 289	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
14	6, 9, 13	3eqtr4d 2220	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = (-𝐴 +𝑒 -𝐵))
15		rexadd 9839	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
16		xnegeq 9814	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = (𝐴 + 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
17	15, 16	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
18		rexneg 9817	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
19		rexneg 9817	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → -𝑒𝐵 = -𝐵)
20	18, 19	oveqan12d 5888	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝐴 +𝑒 -𝐵))
21	14, 17, 20	3eqtr4d 2220	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
22		xnegpnf 9815	. . . . . 6 ⊢ -𝑒+∞ = -∞
23		oveq2 5877	. . . . . . . 8 ⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 +∞))
24		rexr 7993	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
25		renemnf 7996	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
26		xaddpnf1 9833	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
27	24, 25, 26	syl2anc 411	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞) = +∞)
28	23, 27	sylan9eqr 2232	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞)
29		xnegeq 9814	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = +∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
30	28, 29	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
31		xnegeq 9814	. . . . . . . . 9 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -𝑒+∞)
32	31, 22	eqtrdi 2226	. . . . . . . 8 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -∞)
33	32	oveq2d 5885	. . . . . . 7 ⊢ (𝐵 = +∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 -∞))
34	18, 10	eqeltrd 2254	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
35		rexr 7993	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ*)
36		renepnf 7995	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ +∞)
37		xaddmnf1 9835	. . . . . . . . 9 ⊢ ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ +∞) → (-𝑒𝐴 +𝑒 -∞) = -∞)
38	35, 36, 37	syl2anc 411	. . . . . . . 8 ⊢ (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
39	34, 38	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
40	33, 39	sylan9eqr 2232	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = -∞)
41	22, 30, 40	3eqtr4a 2236	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
42		xnegmnf 9816	. . . . . 6 ⊢ -𝑒-∞ = +∞
43		oveq2 5877	. . . . . . . 8 ⊢ (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 -∞))
44		renepnf 7995	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
45		xaddmnf1 9835	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
46	24, 44, 45	syl2anc 411	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞) = -∞)
47	43, 46	sylan9eqr 2232	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞)
48		xnegeq 9814	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = -∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
49	47, 48	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
50		xnegeq 9814	. . . . . . . . 9 ⊢ (𝐵 = -∞ → -𝑒𝐵 = -𝑒-∞)
51	50, 42	eqtrdi 2226	. . . . . . . 8 ⊢ (𝐵 = -∞ → -𝑒𝐵 = +∞)
52	51	oveq2d 5885	. . . . . . 7 ⊢ (𝐵 = -∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 +∞))
53		renemnf 7996	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ -∞)
54		xaddpnf1 9833	. . . . . . . . 9 ⊢ ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ -∞) → (-𝑒𝐴 +𝑒 +∞) = +∞)
55	35, 53, 54	syl2anc 411	. . . . . . . 8 ⊢ (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
56	34, 55	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
57	52, 56	sylan9eqr 2232	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = +∞)
58	42, 49, 57	3eqtr4a 2236	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
59	21, 41, 58	3jaodan 1306	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
60	2, 59	sylan2b 287	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
61		xneg0 9818	. . . . . . 7 ⊢ -𝑒0 = 0
62		simpr 110	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → 𝐵 = -∞)
63	62	oveq2d 5885	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (+∞ +𝑒 𝐵) = (+∞ +𝑒 -∞))
64		pnfaddmnf 9837	. . . . . . . . 9 ⊢ (+∞ +𝑒 -∞) = 0
65	63, 64	eqtrdi 2226	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (+∞ +𝑒 𝐵) = 0)
66		xnegeq 9814	. . . . . . . 8 ⊢ ((+∞ +𝑒 𝐵) = 0 → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
67	65, 66	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
68	51	adantl 277	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒𝐵 = +∞)
69	68	oveq2d 5885	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = (-∞ +𝑒 +∞))
70		mnfaddpnf 9838	. . . . . . . 8 ⊢ (-∞ +𝑒 +∞) = 0
71	69, 70	eqtrdi 2226	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = 0)
72	61, 67, 71	3eqtr4a 2236	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
73		xaddpnf2 9834	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
74		xnegeq 9814	. . . . . . . 8 ⊢ ((+∞ +𝑒 𝐵) = +∞ → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
75	73, 74	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
76		xnegcl 9819	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → -𝑒𝐵 ∈ ℝ*)
77		xnegeq 9814	. . . . . . . . . . . 12 ⊢ (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -𝑒+∞)
78	77, 22	eqtrdi 2226	. . . . . . . . . . 11 ⊢ (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -∞)
79		xnegneg 9820	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ* → -𝑒-𝑒𝐵 = 𝐵)
80	79	eqeq1d 2186	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = -∞ ↔ 𝐵 = -∞))
81	78, 80	imbitrid 154	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (-𝑒𝐵 = +∞ → 𝐵 = -∞))
82	81	necon3d 2391	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → (𝐵 ≠ -∞ → -𝑒𝐵 ≠ +∞))
83	82	imp 124	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒𝐵 ≠ +∞)
84		xaddmnf2 9836	. . . . . . . 8 ⊢ ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ +∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
85	76, 83, 84	syl2an2r 595	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
86	22, 75, 85	3eqtr4a 2236	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
87		xrmnfdc 9830	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
88		exmiddc 836	. . . . . . . 8 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
89	87, 88	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
90		df-ne 2348	. . . . . . . 8 ⊢ (𝐵 ≠ -∞ ↔ ¬ 𝐵 = -∞)
91	90	orbi2i 762	. . . . . . 7 ⊢ ((𝐵 = -∞ ∨ 𝐵 ≠ -∞) ↔ (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
92	89, 91	sylibr 134	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
93	72, 86, 92	mpjaodan 798	. . . . 5 ⊢ (𝐵 ∈ ℝ* → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
94	93	adantl 277	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
95		simpl 109	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = +∞)
96	95	oveq1d 5884	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
97		xnegeq 9814	. . . . 5 ⊢ ((𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
98	96, 97	syl 14	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
99		xnegeq 9814	. . . . . . 7 ⊢ (𝐴 = +∞ → -𝑒𝐴 = -𝑒+∞)
100	99	adantr 276	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒+∞)
101	100, 22	eqtrdi 2226	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -∞)
102	101	oveq1d 5884	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-∞ +𝑒 -𝑒𝐵))
103	94, 98, 102	3eqtr4d 2220	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
104		simpr 110	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → 𝐵 = +∞)
105	104	oveq2d 5885	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (-∞ +𝑒 𝐵) = (-∞ +𝑒 +∞))
106	105, 70	eqtrdi 2226	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (-∞ +𝑒 𝐵) = 0)
107		xnegeq 9814	. . . . . . . 8 ⊢ ((-∞ +𝑒 𝐵) = 0 → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
108	106, 107	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
109	32	adantl 277	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒𝐵 = -∞)
110	109	oveq2d 5885	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = (+∞ +𝑒 -∞))
111	110, 64	eqtrdi 2226	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = 0)
112	61, 108, 111	3eqtr4a 2236	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
113		xaddmnf2 9836	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
114		xnegeq 9814	. . . . . . . 8 ⊢ ((-∞ +𝑒 𝐵) = -∞ → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
115	113, 114	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
116		xnegeq 9814	. . . . . . . . . . . 12 ⊢ (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = -𝑒-∞)
117	116, 42	eqtrdi 2226	. . . . . . . . . . 11 ⊢ (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = +∞)
118	79	eqeq1d 2186	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = +∞ ↔ 𝐵 = +∞))
119	117, 118	imbitrid 154	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (-𝑒𝐵 = -∞ → 𝐵 = +∞))
120	119	necon3d 2391	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → (𝐵 ≠ +∞ → -𝑒𝐵 ≠ -∞))
121	120	imp 124	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒𝐵 ≠ -∞)
122		xaddpnf2 9834	. . . . . . . 8 ⊢ ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ -∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
123	76, 121, 122	syl2an2r 595	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
124	42, 115, 123	3eqtr4a 2236	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
125		xrpnfdc 9829	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
126		exmiddc 836	. . . . . . . 8 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
127	125, 126	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
128		df-ne 2348	. . . . . . . 8 ⊢ (𝐵 ≠ +∞ ↔ ¬ 𝐵 = +∞)
129	128	orbi2i 762	. . . . . . 7 ⊢ ((𝐵 = +∞ ∨ 𝐵 ≠ +∞) ↔ (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
130	127, 129	sylibr 134	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
131	112, 124, 130	mpjaodan 798	. . . . 5 ⊢ (𝐵 ∈ ℝ* → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
132	131	adantl 277	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
133		simpl 109	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = -∞)
134	133	oveq1d 5884	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
135		xnegeq 9814	. . . . 5 ⊢ ((𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
136	134, 135	syl 14	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
137		xnegeq 9814	. . . . . . 7 ⊢ (𝐴 = -∞ → -𝑒𝐴 = -𝑒-∞)
138	137	adantr 276	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒-∞)
139	138, 42	eqtrdi 2226	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = +∞)
140	139	oveq1d 5884	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (+∞ +𝑒 -𝑒𝐵))
141	132, 136, 140	3eqtr4d 2220	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
142	60, 103, 141	3jaoian 1305	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
143	1, 142	sylanb 284	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 708  DECID wdc 834   ∨ w3o 977   = wceq 1353   ∈ wcel 2148   ≠ wne 2347  (class class class)co 5869  ℂcc 7800  ℝcr 7801  0cc0 7802   + caddc 7805  +∞cpnf 7979  -∞cmnf 7980  ℝ^*cxr 7981  -cneg 8119  -_𝑒cxne 9756   +_𝑒 cxad 9757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-addcom 7902  ax-addass 7904  ax-distr 7906  ax-i2m1 7907  ax-0id 7910  ax-rnegex 7911  ax-cnre 7913

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-iota 5174  df-fun 5214  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-pnf 7984  df-mnf 7985  df-xr 7986  df-sub 8120  df-neg 8121  df-xneg 9759  df-xadd 9760

This theorem is referenced by:  xaddass2  9857  xrminadd  11267