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 xaddid2 ( -𝑒 𝐴 ∈ ℝ* → ( 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 ↔ 𝐴 = -𝑒 𝐵 ) )