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
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A +e B ) = 0 <-> A = -e B ) )

Proof

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