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 xaddlid 
 |-  ( -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 ) )