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