xaddeq0

Description: Two extended reals which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 13-Jun-2017)

		Ref	Expression
	Assertion	xaddeq0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A +_{𝑒} B = 0 \leftrightarrow A = - B)$

Proof

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		simpll	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A \in ℝ$
3	2	rexrd	$⊢ ((A \in ℝ \land B \in ℝ^{}) \land A +_{𝑒} B = 0) \to A \in ℝ^{}$
4		xnegneg	$⊢ A \in ℝ^{*} \to - (- A) = A$
5	3 4	syl	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to - (- A) = A$
6	3	xnegcld	$⊢ ((A \in ℝ \land B \in ℝ^{}) \land A +_{𝑒} B = 0) \to - A \in ℝ^{}$
7		xaddid2	$⊢ - A \in ℝ^{*} \to 0 +_{𝑒} (- A) = - A$
8	6 7	syl	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to 0 +_{𝑒} (- A) = - A$
9		simplr	$⊢ ((A \in ℝ \land B \in ℝ^{}) \land A +_{𝑒} B = 0) \to B \in ℝ^{}$
10		xaddcom	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A +_{𝑒} B = B +_{𝑒} A$
11	3 9 10	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A +_{𝑒} B = B +_{𝑒} A$
12	11	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to (A +_{𝑒} B) +_{𝑒} (- A) = (B +_{𝑒} A) +_{𝑒} (- A)$
13		simpr	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A +_{𝑒} B = 0$
14	13	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to (A +_{𝑒} B) +_{𝑒} (- A) = 0 +_{𝑒} (- A)$
15		xpncan	$⊢ (B \in ℝ^{*} \land A \in ℝ) \to (B +_{𝑒} A) +_{𝑒} (- A) = B$
16	15	ancoms	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (B +_{𝑒} A) +_{𝑒} (- A) = B$
17	16	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to (B +_{𝑒} A) +_{𝑒} (- A) = B$
18	12 14 17	3eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to 0 +_{𝑒} (- A) = B$
19	8 18	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to - A = B$
20		xnegeq	$⊢ - A = B \to - (- A) = - B$
21	19 20	syl	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to - (- A) = - B$
22	5 21	eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A = - B$
23	22	ex	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (A +_{𝑒} B = 0 \to A = - B)$
24		simpll	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A = +∞$
25		simplr	$⊢ ((A = +∞ \land B \in ℝ^{}) \land A +_{𝑒} B = 0) \to B \in ℝ^{}$
26	24	oveq1d	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A +_{𝑒} B = +∞ +_{𝑒} B$
27		simpr	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A +_{𝑒} B = 0$
28	26 27	eqtr3d	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to +∞ +_{𝑒} B = 0$
29		0re	$⊢ 0 \in ℝ$
30		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
31	29 30	mp1i	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to 0 \neq +∞$
32	28 31	eqnetrd	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to +∞ +_{𝑒} B \neq +∞$
33	32	neneqd	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to \neg +∞ +_{𝑒} B = +∞$
34		xaddpnf2	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to +∞ +_{𝑒} B = +∞$
35	34	stoic1a	$⊢ (B \in ℝ^{*} \land \neg +∞ +_{𝑒} B = +∞) \to \neg B \neq −∞$
36	25 33 35	syl2anc	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to \neg B \neq −∞$
37		nne	$⊢ \neg B \neq −∞ \leftrightarrow B = −∞$
38	36 37	sylib	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to B = −∞$
39		xnegeq	$⊢ B = −∞ \to - B = - −∞$
40	38 39	syl	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to - B = - −∞$
41		xnegmnf	$⊢ - −∞ = +∞$
42	40 41	eqtr2di	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to +∞ = - B$
43	24 42	eqtrd	$⊢ ((A = +∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A = - B$
44	43	ex	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A +_{𝑒} B = 0 \to A = - B)$
45		simpll	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A = −∞$
46		simplr	$⊢ ((A = −∞ \land B \in ℝ^{}) \land A +_{𝑒} B = 0) \to B \in ℝ^{}$
47	45	oveq1d	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A +_{𝑒} B = −∞ +_{𝑒} B$
48		simpr	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A +_{𝑒} B = 0$
49	47 48	eqtr3d	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to −∞ +_{𝑒} B = 0$
50		renemnf	$⊢ 0 \in ℝ \to 0 \neq −∞$
51	29 50	mp1i	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to 0 \neq −∞$
52	49 51	eqnetrd	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to −∞ +_{𝑒} B \neq −∞$
53	52	neneqd	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to \neg −∞ +_{𝑒} B = −∞$
54		xaddmnf2	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to −∞ +_{𝑒} B = −∞$
55	54	stoic1a	$⊢ (B \in ℝ^{*} \land \neg −∞ +_{𝑒} B = −∞) \to \neg B \neq +∞$
56	46 53 55	syl2anc	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to \neg B \neq +∞$
57		nne	$⊢ \neg B \neq +∞ \leftrightarrow B = +∞$
58	56 57	sylib	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to B = +∞$
59		xnegeq	$⊢ B = +∞ \to - B = - +∞$
60	58 59	syl	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to - B = - +∞$
61		xnegpnf	$⊢ - +∞ = −∞$
62	60 61	eqtr2di	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to −∞ = - B$
63	45 62	eqtrd	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land A +_{𝑒} B = 0) \to A = - B$
64	63	ex	$⊢ (A = −∞ \land B \in ℝ^{*}) \to (A +_{𝑒} B = 0 \to A = - B)$
65	23 44 64	3jaoian	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land B \in ℝ^{*}) \to (A +_{𝑒} B = 0 \to A = - B)$
66	1 65	sylanb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A +_{𝑒} B = 0 \to A = - B)$
67		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to A = - B$
68	67	oveq1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to A +_{𝑒} B = (- B) +_{𝑒} B$
69		xnegcl	$⊢ B \in ℝ^{} \to - B \in ℝ^{}$
70	69	ad2antlr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to - B \in ℝ^{*}$
71		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to B \in ℝ^{*}$
72		xaddcom	$⊢ (- B \in ℝ^{} \land B \in ℝ^{}) \to (- B) +_{𝑒} B = B +_{𝑒} (- B)$
73	70 71 72	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to (- B) +_{𝑒} B = B +_{𝑒} (- B)$
74		xnegid	$⊢ B \in ℝ^{*} \to B +_{𝑒} (- B) = 0$
75	74	ad2antlr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to B +_{𝑒} (- B) = 0$
76	68 73 75	3eqtrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A = - B) \to A +_{𝑒} B = 0$
77	76	ex	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = - B \to A +_{𝑒} B = 0)$
78	66 77	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A +_{𝑒} B = 0 \leftrightarrow A = - B)$

Metamath Proof Explorer

Theorem xaddeq0

Proof