| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elxr |
|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) ) |
| 2 |
|
rexneg |
|- ( A e. RR -> -e A = -u A ) |
| 3 |
2
|
oveq2d |
|- ( A e. RR -> ( A +e -e A ) = ( A +e -u A ) ) |
| 4 |
|
renegcl |
|- ( A e. RR -> -u A e. RR ) |
| 5 |
|
rexadd |
|- ( ( A e. RR /\ -u A e. RR ) -> ( A +e -u A ) = ( A + -u A ) ) |
| 6 |
4 5
|
mpdan |
|- ( A e. RR -> ( A +e -u A ) = ( A + -u A ) ) |
| 7 |
|
recn |
|- ( A e. RR -> A e. CC ) |
| 8 |
7
|
negidd |
|- ( A e. RR -> ( A + -u A ) = 0 ) |
| 9 |
3 6 8
|
3eqtrd |
|- ( A e. RR -> ( A +e -e A ) = 0 ) |
| 10 |
|
id |
|- ( A = +oo -> A = +oo ) |
| 11 |
|
xnegeq |
|- ( A = +oo -> -e A = -e +oo ) |
| 12 |
|
xnegpnf |
|- -e +oo = -oo |
| 13 |
11 12
|
eqtrdi |
|- ( A = +oo -> -e A = -oo ) |
| 14 |
10 13
|
oveq12d |
|- ( A = +oo -> ( A +e -e A ) = ( +oo +e -oo ) ) |
| 15 |
|
pnfaddmnf |
|- ( +oo +e -oo ) = 0 |
| 16 |
14 15
|
eqtrdi |
|- ( A = +oo -> ( A +e -e A ) = 0 ) |
| 17 |
|
id |
|- ( A = -oo -> A = -oo ) |
| 18 |
|
xnegeq |
|- ( A = -oo -> -e A = -e -oo ) |
| 19 |
|
xnegmnf |
|- -e -oo = +oo |
| 20 |
18 19
|
eqtrdi |
|- ( A = -oo -> -e A = +oo ) |
| 21 |
17 20
|
oveq12d |
|- ( A = -oo -> ( A +e -e A ) = ( -oo +e +oo ) ) |
| 22 |
|
mnfaddpnf |
|- ( -oo +e +oo ) = 0 |
| 23 |
21 22
|
eqtrdi |
|- ( A = -oo -> ( A +e -e A ) = 0 ) |
| 24 |
9 16 23
|
3jaoi |
|- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A +e -e A ) = 0 ) |
| 25 |
1 24
|
sylbi |
|- ( A e. RR* -> ( A +e -e A ) = 0 ) |