xaddeq0 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > xaddeq0		Structured version Visualization version GIF version

Theorem xaddeq0 33401

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

**Assertion**
Ref	Expression
xaddeq0	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 ↔ 𝐴 = -_e𝐵))

**Proof of Theorem xaddeq0**
Step	Hyp	Ref	Expression
1		elxr 13258	. . 3 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		simpll 779	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 ∈ ℝ)
3	2	rexrd 11372	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 ∈ ℝ^)
4		xnegneg 13357	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → -_e -_e𝐴 = 𝐴)
5	3, 4	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → -_e -_e𝐴 = 𝐴)
6	3	xnegcld 13443	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 +_e 𝐵) = 0) → -_e𝐴 ∈ ℝ^)
7		xaddlid 13385	. . . . . . . . 9 ⊢ ( -_e𝐴 ∈ ℝ^* → (0 +_e -_e𝐴) = -_e𝐴)
8	6, 7	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (0 +_e -_e𝐴) = -_e𝐴)
9		simplr 781	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 +_e 𝐵) = 0) → 𝐵 ∈ ℝ^)
10		xaddcom 13383	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_e 𝐵) = (𝐵 +_e 𝐴))
11	3, 9, 10	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (𝐴 +_e 𝐵) = (𝐵 +_e 𝐴))
12	11	oveq1d 7445	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ((𝐴 +_e 𝐵) +_e -_e𝐴) = ((𝐵 +_e 𝐴) +_e -_e𝐴))
13		simpr 490	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (𝐴 +_e 𝐵) = 0)
14	13	oveq1d 7445	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ((𝐴 +_e 𝐵) +_e -_e𝐴) = (0 +_e -_e𝐴))
15		xpncan 13394	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ) → ((𝐵 +_e 𝐴) +_e -_e𝐴) = 𝐵)
16	15	ancoms 464	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → ((𝐵 +_e 𝐴) +_e -_e𝐴) = 𝐵)
17	16	adantr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ((𝐵 +_e 𝐴) +_e -_e𝐴) = 𝐵)
18	12, 14, 17	3eqtr3d 2806	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (0 +_e -_e𝐴) = 𝐵)
19	8, 18	eqtr3d 2800	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → -_e𝐴 = 𝐵)
20		xnegeq 13350	. . . . . . 7 ⊢ ( -_e𝐴 = 𝐵 → -_e -_e𝐴 = -_e𝐵)
21	19, 20	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → -_e -_e𝐴 = -_e𝐵)
22	5, 21	eqtr3d 2800	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 = -_e𝐵)
23	22	ex 418	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 → 𝐴 = -_e𝐵))
24		simpll 779	. . . . . 6 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 = +∞)
25		simplr 781	. . . . . . . . . 10 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 +_e 𝐵) = 0) → 𝐵 ∈ ℝ^)
26	24	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (𝐴 +_e 𝐵) = (+∞ +_e 𝐵))
27		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (𝐴 +_e 𝐵) = 0)
28	26, 27	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (+∞ +_e 𝐵) = 0)
29		0re 11323	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
30		renepnf 11370	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
31	29, 30	mp1i 14	. . . . . . . . . . . 12 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 0 ≠ +∞)
32	28, 31	eqnetrd 3026	. . . . . . . . . . 11 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (+∞ +_e 𝐵) ≠ +∞)
33	32	neneqd 2964	. . . . . . . . . 10 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ¬ (+∞ +_e 𝐵) = +∞)
34		xaddpnf2 13370	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_e 𝐵) = +∞)
35	34	stoic1a 1804	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ^* ∧ ¬ (+∞ +_e 𝐵) = +∞) → ¬ 𝐵 ≠ -∞)
36	25, 33, 35	syl2anc 596	. . . . . . . . 9 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ¬ 𝐵 ≠ -∞)
37		nne 2963	. . . . . . . . 9 ⊢ (¬ 𝐵 ≠ -∞ ↔ 𝐵 = -∞)
38	36, 37	sylib 221	. . . . . . . 8 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐵 = -∞)
39		xnegeq 13350	. . . . . . . 8 ⊢ (𝐵 = -∞ → -_e𝐵 = -_e-∞)
40	38, 39	syl 18	. . . . . . 7 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → -_e𝐵 = -_e-∞)
41		xnegmnf 13353	. . . . . . 7 ⊢ -_e-∞ = +∞
42	40, 41	eqtr2di 2815	. . . . . 6 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → +∞ = -_e𝐵)
43	24, 42	eqtrd 2798	. . . . 5 ⊢ (((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 = -_e𝐵)
44	43	ex 418	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 → 𝐴 = -_e𝐵))
45		simpll 779	. . . . . 6 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 = -∞)
46		simplr 781	. . . . . . . . . 10 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^) ∧ (𝐴 +_e 𝐵) = 0) → 𝐵 ∈ ℝ^)
47	45	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (𝐴 +_e 𝐵) = (-∞ +_e 𝐵))
48		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (𝐴 +_e 𝐵) = 0)
49	47, 48	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (-∞ +_e 𝐵) = 0)
50		renemnf 11371	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
51	29, 50	mp1i 14	. . . . . . . . . . . 12 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 0 ≠ -∞)
52	49, 51	eqnetrd 3026	. . . . . . . . . . 11 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → (-∞ +_e 𝐵) ≠ -∞)
53	52	neneqd 2964	. . . . . . . . . 10 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ¬ (-∞ +_e 𝐵) = -∞)
54		xaddmnf2 13372	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_e 𝐵) = -∞)
55	54	stoic1a 1804	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ^* ∧ ¬ (-∞ +_e 𝐵) = -∞) → ¬ 𝐵 ≠ +∞)
56	46, 53, 55	syl2anc 596	. . . . . . . . 9 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → ¬ 𝐵 ≠ +∞)
57		nne 2963	. . . . . . . . 9 ⊢ (¬ 𝐵 ≠ +∞ ↔ 𝐵 = +∞)
58	56, 57	sylib 221	. . . . . . . 8 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐵 = +∞)
59		xnegeq 13350	. . . . . . . 8 ⊢ (𝐵 = +∞ → -_e𝐵 = -_e+∞)
60	58, 59	syl 18	. . . . . . 7 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → -_e𝐵 = -_e+∞)
61		xnegpnf 13352	. . . . . . 7 ⊢ -_e+∞ = -∞
62	60, 61	eqtr2di 2815	. . . . . 6 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → -∞ = -_e𝐵)
63	45, 62	eqtrd 2798	. . . . 5 ⊢ (((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 +_e 𝐵) = 0) → 𝐴 = -_e𝐵)
64	63	ex 418	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 → 𝐴 = -_e𝐵))
65	23, 44, 64	3jaoian 1457	. . 3 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 → 𝐴 = -_e𝐵))
66	1, 65	sylanb 593	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 → 𝐴 = -_e𝐵))
67		simpr 490	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 = -_e𝐵) → 𝐴 = -_e𝐵)
68	67	oveq1d 7445	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 = -_e𝐵) → (𝐴 +_e 𝐵) = ( -_e𝐵 +_e 𝐵))
69		xnegcl 13356	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → -_e𝐵 ∈ ℝ^*)
70	69	ad2antlr 740	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 = -_e𝐵) → -_e𝐵 ∈ ℝ^)
71		simplr 781	. . . . 5 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝐴 = -_e𝐵) → 𝐵 ∈ ℝ^)
72		xaddcom 13383	. . . . 5 ⊢ (( -_e𝐵 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ( -_e𝐵 +_e 𝐵) = (𝐵 +_e -_e𝐵))
73	70, 71, 72	syl2anc 596	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 = -_e𝐵) → ( -_e𝐵 +_e 𝐵) = (𝐵 +_e -_e𝐵))
74		xnegid 13381	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (𝐵 +_e -_e𝐵) = 0)
75	74	ad2antlr 740	. . . 4 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 = -_e𝐵) → (𝐵 +_e -_e𝐵) = 0)
76	68, 73, 75	3eqtrd 2802	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝐴 = -_e𝐵) → (𝐴 +_e 𝐵) = 0)
77	76	ex 418	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 = -_e𝐵 → (𝐴 +_e 𝐵) = 0))
78	66, 77	impbid 215	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 +_e 𝐵) = 0 ↔ 𝐴 = -_e𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ w3o 1102 = wceq 1569 ∈ wcel 2146 ≠ wne 2959 (class class class)co 7430 ℝcr 11212 0cc0 11213 +∞cpnf 11353 -∞cmnf 11354 ℝ^*cxr 11355 -_ecxne 13251 +_e cxad 13252

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7761 ax-cnex 11269 ax-resscn 11270 ax-1cn 11271 ax-icn 11272 ax-addcl 11273 ax-addrcl 11274 ax-mulcl 11275 ax-mulrcl 11276 ax-mulcom 11277 ax-addass 11278 ax-mulass 11279 ax-distr 11280 ax-i2m1 11281 ax-1ne0 11282 ax-1rid 11283 ax-rnegex 11284 ax-rrecex 11285 ax-cnre 11286 ax-pre-lttri 11287 ax-pre-lttrn 11288 ax-pre-ltadd 11289

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-id 5550 df-po 5563 df-so 5564 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6501 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-1st 8011 df-2nd 8012 df-er 8731 df-en 8988 df-dom 8989 df-sdom 8990 df-pnf 11358 df-mnf 11359 df-xr 11360 df-ltxr 11361 df-sub 11556 df-neg 11557 df-xneg 13254 df-xadd 13255

This theorem is used by: xrsinvgval 33625

W3C validator