Theorem xnegdi 10060

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

Assertion

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

Proof of Theorem xnegdi

Step	Hyp	Ref	Expression
1		elxr 9968	. 2 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 9968	. . . 4 ⊢ (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 8128	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 8128	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		negdi 8399	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
6	3, 4, 5	syl2an 289	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
7		readdcl 8121	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
8		rexneg 10022	. . . . . . . 8 ⊢ ((𝐴 + 𝐵) ∈ ℝ → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
9	7, 8	syl 14	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
10		renegcl 8403	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
11		renegcl 8403	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
12		rexadd 10044	. . . . . . . 8 ⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
13	10, 11, 12	syl2an 289	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
14	6, 9, 13	3eqtr4d 2272	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = (-𝐴 +𝑒 -𝐵))
15		rexadd 10044	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
16		xnegeq 10019	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = (𝐴 + 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
17	15, 16	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
18		rexneg 10022	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
19		rexneg 10022	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → -𝑒𝐵 = -𝐵)
20	18, 19	oveqan12d 6019	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝐴 +𝑒 -𝐵))
21	14, 17, 20	3eqtr4d 2272	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
22		xnegpnf 10020	. . . . . 6 ⊢ -𝑒+∞ = -∞
23		oveq2 6008	. . . . . . . 8 ⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 +∞))
24		rexr 8188	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
25		renemnf 8191	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
26		xaddpnf1 10038	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
27	24, 25, 26	syl2anc 411	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞) = +∞)
28	23, 27	sylan9eqr 2284	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞)
29		xnegeq 10019	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = +∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
30	28, 29	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
31		xnegeq 10019	. . . . . . . . 9 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -𝑒+∞)
32	31, 22	eqtrdi 2278	. . . . . . . 8 ⊢ (𝐵 = +∞ → -𝑒𝐵 = -∞)
33	32	oveq2d 6016	. . . . . . 7 ⊢ (𝐵 = +∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 -∞))
34	18, 10	eqeltrd 2306	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
35		rexr 8188	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ*)
36		renepnf 8190	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ +∞)
37		xaddmnf1 10040	. . . . . . . . 9 ⊢ ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ +∞) → (-𝑒𝐴 +𝑒 -∞) = -∞)
38	35, 36, 37	syl2anc 411	. . . . . . . 8 ⊢ (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
39	34, 38	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
40	33, 39	sylan9eqr 2284	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = -∞)
41	22, 30, 40	3eqtr4a 2288	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
42		xnegmnf 10021	. . . . . 6 ⊢ -𝑒-∞ = +∞
43		oveq2 6008	. . . . . . . 8 ⊢ (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 -∞))
44		renepnf 8190	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
45		xaddmnf1 10040	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
46	24, 44, 45	syl2anc 411	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞) = -∞)
47	43, 46	sylan9eqr 2284	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞)
48		xnegeq 10019	. . . . . . 7 ⊢ ((𝐴 +𝑒 𝐵) = -∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
49	47, 48	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
50		xnegeq 10019	. . . . . . . . 9 ⊢ (𝐵 = -∞ → -𝑒𝐵 = -𝑒-∞)
51	50, 42	eqtrdi 2278	. . . . . . . 8 ⊢ (𝐵 = -∞ → -𝑒𝐵 = +∞)
52	51	oveq2d 6016	. . . . . . 7 ⊢ (𝐵 = -∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 +∞))
53		renemnf 8191	. . . . . . . . 9 ⊢ (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ -∞)
54		xaddpnf1 10038	. . . . . . . . 9 ⊢ ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ -∞) → (-𝑒𝐴 +𝑒 +∞) = +∞)
55	35, 53, 54	syl2anc 411	. . . . . . . 8 ⊢ (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
56	34, 55	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
57	52, 56	sylan9eqr 2284	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = +∞)
58	42, 49, 57	3eqtr4a 2288	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
59	21, 41, 58	3jaodan 1340	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
60	2, 59	sylan2b 287	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
61		xneg0 10023	. . . . . . 7 ⊢ -𝑒0 = 0
62		simpr 110	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → 𝐵 = -∞)
63	62	oveq2d 6016	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (+∞ +𝑒 𝐵) = (+∞ +𝑒 -∞))
64		pnfaddmnf 10042	. . . . . . . . 9 ⊢ (+∞ +𝑒 -∞) = 0
65	63, 64	eqtrdi 2278	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (+∞ +𝑒 𝐵) = 0)
66		xnegeq 10019	. . . . . . . 8 ⊢ ((+∞ +𝑒 𝐵) = 0 → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
67	65, 66	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
68	51	adantl 277	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒𝐵 = +∞)
69	68	oveq2d 6016	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = (-∞ +𝑒 +∞))
70		mnfaddpnf 10043	. . . . . . . 8 ⊢ (-∞ +𝑒 +∞) = 0
71	69, 70	eqtrdi 2278	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = 0)
72	61, 67, 71	3eqtr4a 2288	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
73		xaddpnf2 10039	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
74		xnegeq 10019	. . . . . . . 8 ⊢ ((+∞ +𝑒 𝐵) = +∞ → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
75	73, 74	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
76		xnegcl 10024	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → -𝑒𝐵 ∈ ℝ*)
77		xnegeq 10019	. . . . . . . . . . . 12 ⊢ (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -𝑒+∞)
78	77, 22	eqtrdi 2278	. . . . . . . . . . 11 ⊢ (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -∞)
79		xnegneg 10025	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ* → -𝑒-𝑒𝐵 = 𝐵)
80	79	eqeq1d 2238	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = -∞ ↔ 𝐵 = -∞))
81	78, 80	imbitrid 154	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (-𝑒𝐵 = +∞ → 𝐵 = -∞))
82	81	necon3d 2444	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → (𝐵 ≠ -∞ → -𝑒𝐵 ≠ +∞))
83	82	imp 124	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒𝐵 ≠ +∞)
84		xaddmnf2 10041	. . . . . . . 8 ⊢ ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ +∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
85	76, 83, 84	syl2an2r 597	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
86	22, 75, 85	3eqtr4a 2288	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
87		xrmnfdc 10035	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = -∞)
88		exmiddc 841	. . . . . . . 8 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
89	87, 88	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
90		df-ne 2401	. . . . . . . 8 ⊢ (𝐵 ≠ -∞ ↔ ¬ 𝐵 = -∞)
91	90	orbi2i 767	. . . . . . 7 ⊢ ((𝐵 = -∞ ∨ 𝐵 ≠ -∞) ↔ (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
92	89, 91	sylibr 134	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
93	72, 86, 92	mpjaodan 803	. . . . 5 ⊢ (𝐵 ∈ ℝ* → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
94	93	adantl 277	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
95		simpl 109	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = +∞)
96	95	oveq1d 6015	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
97		xnegeq 10019	. . . . 5 ⊢ ((𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
98	96, 97	syl 14	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
99		xnegeq 10019	. . . . . . 7 ⊢ (𝐴 = +∞ → -𝑒𝐴 = -𝑒+∞)
100	99	adantr 276	. . . . . 6 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒+∞)
101	100, 22	eqtrdi 2278	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -∞)
102	101	oveq1d 6015	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-∞ +𝑒 -𝑒𝐵))
103	94, 98, 102	3eqtr4d 2272	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
104		simpr 110	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → 𝐵 = +∞)
105	104	oveq2d 6016	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (-∞ +𝑒 𝐵) = (-∞ +𝑒 +∞))
106	105, 70	eqtrdi 2278	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (-∞ +𝑒 𝐵) = 0)
107		xnegeq 10019	. . . . . . . 8 ⊢ ((-∞ +𝑒 𝐵) = 0 → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
108	106, 107	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
109	32	adantl 277	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒𝐵 = -∞)
110	109	oveq2d 6016	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = (+∞ +𝑒 -∞))
111	110, 64	eqtrdi 2278	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = 0)
112	61, 108, 111	3eqtr4a 2288	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
113		xaddmnf2 10041	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
114		xnegeq 10019	. . . . . . . 8 ⊢ ((-∞ +𝑒 𝐵) = -∞ → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
115	113, 114	syl 14	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
116		xnegeq 10019	. . . . . . . . . . . 12 ⊢ (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = -𝑒-∞)
117	116, 42	eqtrdi 2278	. . . . . . . . . . 11 ⊢ (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = +∞)
118	79	eqeq1d 2238	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = +∞ ↔ 𝐵 = +∞))
119	117, 118	imbitrid 154	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (-𝑒𝐵 = -∞ → 𝐵 = +∞))
120	119	necon3d 2444	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ* → (𝐵 ≠ +∞ → -𝑒𝐵 ≠ -∞))
121	120	imp 124	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒𝐵 ≠ -∞)
122		xaddpnf2 10039	. . . . . . . 8 ⊢ ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ -∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
123	76, 121, 122	syl2an2r 597	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
124	42, 115, 123	3eqtr4a 2288	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
125		xrpnfdc 10034	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → DECID 𝐵 = +∞)
126		exmiddc 841	. . . . . . . 8 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
127	125, 126	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
128		df-ne 2401	. . . . . . . 8 ⊢ (𝐵 ≠ +∞ ↔ ¬ 𝐵 = +∞)
129	128	orbi2i 767	. . . . . . 7 ⊢ ((𝐵 = +∞ ∨ 𝐵 ≠ +∞) ↔ (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
130	127, 129	sylibr 134	. . . . . 6 ⊢ (𝐵 ∈ ℝ* → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
131	112, 124, 130	mpjaodan 803	. . . . 5 ⊢ (𝐵 ∈ ℝ* → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
132	131	adantl 277	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
133		simpl 109	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = -∞)
134	133	oveq1d 6015	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
135		xnegeq 10019	. . . . 5 ⊢ ((𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
136	134, 135	syl 14	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
137		xnegeq 10019	. . . . . . 7 ⊢ (𝐴 = -∞ → -𝑒𝐴 = -𝑒-∞)
138	137	adantr 276	. . . . . 6 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒-∞)
139	138, 42	eqtrdi 2278	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = +∞)
140	139	oveq1d 6015	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (+∞ +𝑒 -𝑒𝐵))
141	132, 136, 140	3eqtr4d 2272	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
142	60, 103, 141	3jaoian 1339	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
143	1, 142	sylanb 284	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713  DECID wdc 839   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200   ≠ wne 2400  (class class class)co 6000  ℂcc 7993  ℝcr 7994  0cc0 7995   + caddc 7998  +∞cpnf 8174  -∞cmnf 8175  ℝ^*cxr 8176  -cneg 8314  -_𝑒cxne 9961   +_𝑒 cxad 9962

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-distr 8099  ax-i2m1 8100  ax-0id 8103  ax-rnegex 8104  ax-cnre 8106

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-iota 5277  df-fun 5319  df-fv 5325  df-riota 5953  df-ov 6003  df-oprab 6004  df-mpo 6005  df-pnf 8179  df-mnf 8180  df-xr 8181  df-sub 8315  df-neg 8316  df-xneg 9964  df-xadd 9965

This theorem is referenced by:  xaddass2  10062  xrminadd  11781