Step |
Hyp |
Ref |
Expression |
1 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
2 |
|
simpl1 |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> A e. ( 0 [,] +oo ) ) |
3 |
1 2
|
sselid |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> A e. RR* ) |
4 |
|
simpr |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> B = +oo ) |
5 |
|
simpl3 |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> B <_ A ) |
6 |
4 5
|
eqbrtrrd |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> +oo <_ A ) |
7 |
|
xgepnf |
|- ( A e. RR* -> ( +oo <_ A <-> A = +oo ) ) |
8 |
7
|
biimpa |
|- ( ( A e. RR* /\ +oo <_ A ) -> A = +oo ) |
9 |
3 6 8
|
syl2anc |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> A = +oo ) |
10 |
|
xnegeq |
|- ( B = +oo -> -e B = -e +oo ) |
11 |
4 10
|
syl |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> -e B = -e +oo ) |
12 |
9 11
|
oveq12d |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( A +e -e B ) = ( +oo +e -e +oo ) ) |
13 |
|
pnfxr |
|- +oo e. RR* |
14 |
|
xnegid |
|- ( +oo e. RR* -> ( +oo +e -e +oo ) = 0 ) |
15 |
13 14
|
ax-mp |
|- ( +oo +e -e +oo ) = 0 |
16 |
12 15
|
eqtrdi |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( A +e -e B ) = 0 ) |
17 |
16
|
oveq1d |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( ( A +e -e B ) +e B ) = ( 0 +e B ) ) |
18 |
4
|
oveq2d |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( 0 +e B ) = ( 0 +e +oo ) ) |
19 |
|
xaddid2 |
|- ( +oo e. RR* -> ( 0 +e +oo ) = +oo ) |
20 |
13 19
|
mp1i |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( 0 +e +oo ) = +oo ) |
21 |
17 18 20
|
3eqtrd |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( ( A +e -e B ) +e B ) = +oo ) |
22 |
21 9
|
eqtr4d |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ B = +oo ) -> ( ( A +e -e B ) +e B ) = A ) |
23 |
|
simpl1 |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> A e. ( 0 [,] +oo ) ) |
24 |
1 23
|
sselid |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> A e. RR* ) |
25 |
|
xrge0neqmnf |
|- ( A e. ( 0 [,] +oo ) -> A =/= -oo ) |
26 |
23 25
|
syl |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> A =/= -oo ) |
27 |
|
simpl2 |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> B e. ( 0 [,] +oo ) ) |
28 |
1 27
|
sselid |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> B e. RR* ) |
29 |
28
|
xnegcld |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> -e B e. RR* ) |
30 |
|
simpr |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> -. B = +oo ) |
31 |
|
xnegneg |
|- ( B e. RR* -> -e -e B = B ) |
32 |
|
xnegeq |
|- ( -e B = -oo -> -e -e B = -e -oo ) |
33 |
31 32
|
sylan9req |
|- ( ( B e. RR* /\ -e B = -oo ) -> B = -e -oo ) |
34 |
|
xnegmnf |
|- -e -oo = +oo |
35 |
33 34
|
eqtrdi |
|- ( ( B e. RR* /\ -e B = -oo ) -> B = +oo ) |
36 |
35
|
stoic1a |
|- ( ( B e. RR* /\ -. B = +oo ) -> -. -e B = -oo ) |
37 |
36
|
neqned |
|- ( ( B e. RR* /\ -. B = +oo ) -> -e B =/= -oo ) |
38 |
28 30 37
|
syl2anc |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> -e B =/= -oo ) |
39 |
|
xrge0neqmnf |
|- ( B e. ( 0 [,] +oo ) -> B =/= -oo ) |
40 |
27 39
|
syl |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> B =/= -oo ) |
41 |
|
xaddass |
|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( -e B e. RR* /\ -e B =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( ( A +e -e B ) +e B ) = ( A +e ( -e B +e B ) ) ) |
42 |
24 26 29 38 28 40 41
|
syl222anc |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> ( ( A +e -e B ) +e B ) = ( A +e ( -e B +e B ) ) ) |
43 |
|
xnegcl |
|- ( B e. RR* -> -e B e. RR* ) |
44 |
|
xaddcom |
|- ( ( -e B e. RR* /\ B e. RR* ) -> ( -e B +e B ) = ( B +e -e B ) ) |
45 |
43 44
|
mpancom |
|- ( B e. RR* -> ( -e B +e B ) = ( B +e -e B ) ) |
46 |
|
xnegid |
|- ( B e. RR* -> ( B +e -e B ) = 0 ) |
47 |
45 46
|
eqtrd |
|- ( B e. RR* -> ( -e B +e B ) = 0 ) |
48 |
47
|
oveq2d |
|- ( B e. RR* -> ( A +e ( -e B +e B ) ) = ( A +e 0 ) ) |
49 |
|
xaddid1 |
|- ( A e. RR* -> ( A +e 0 ) = A ) |
50 |
48 49
|
sylan9eqr |
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e ( -e B +e B ) ) = A ) |
51 |
24 28 50
|
syl2anc |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> ( A +e ( -e B +e B ) ) = A ) |
52 |
42 51
|
eqtrd |
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) /\ -. B = +oo ) -> ( ( A +e -e B ) +e B ) = A ) |
53 |
22 52
|
pm2.61dan |
|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ A ) -> ( ( A +e -e B ) +e B ) = A ) |