This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 +𝑒 𝐵 ) = 0 ↔ 𝐴 = -𝑒 𝐵 ) )

Proof

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