| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elxr |
|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) ) |
| 2 |
|
0re |
|- 0 e. RR |
| 3 |
|
rexadd |
|- ( ( A e. RR /\ 0 e. RR ) -> ( A +e 0 ) = ( A + 0 ) ) |
| 4 |
2 3
|
mpan2 |
|- ( A e. RR -> ( A +e 0 ) = ( A + 0 ) ) |
| 5 |
|
recn |
|- ( A e. RR -> A e. CC ) |
| 6 |
5
|
addridd |
|- ( A e. RR -> ( A + 0 ) = A ) |
| 7 |
4 6
|
eqtrd |
|- ( A e. RR -> ( A +e 0 ) = A ) |
| 8 |
|
0xr |
|- 0 e. RR* |
| 9 |
|
renemnf |
|- ( 0 e. RR -> 0 =/= -oo ) |
| 10 |
2 9
|
ax-mp |
|- 0 =/= -oo |
| 11 |
|
xaddpnf2 |
|- ( ( 0 e. RR* /\ 0 =/= -oo ) -> ( +oo +e 0 ) = +oo ) |
| 12 |
8 10 11
|
mp2an |
|- ( +oo +e 0 ) = +oo |
| 13 |
|
oveq1 |
|- ( A = +oo -> ( A +e 0 ) = ( +oo +e 0 ) ) |
| 14 |
|
id |
|- ( A = +oo -> A = +oo ) |
| 15 |
12 13 14
|
3eqtr4a |
|- ( A = +oo -> ( A +e 0 ) = A ) |
| 16 |
|
renepnf |
|- ( 0 e. RR -> 0 =/= +oo ) |
| 17 |
2 16
|
ax-mp |
|- 0 =/= +oo |
| 18 |
|
xaddmnf2 |
|- ( ( 0 e. RR* /\ 0 =/= +oo ) -> ( -oo +e 0 ) = -oo ) |
| 19 |
8 17 18
|
mp2an |
|- ( -oo +e 0 ) = -oo |
| 20 |
|
oveq1 |
|- ( A = -oo -> ( A +e 0 ) = ( -oo +e 0 ) ) |
| 21 |
|
id |
|- ( A = -oo -> A = -oo ) |
| 22 |
19 20 21
|
3eqtr4a |
|- ( A = -oo -> ( A +e 0 ) = A ) |
| 23 |
7 15 22
|
3jaoi |
|- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A +e 0 ) = A ) |
| 24 |
1 23
|
sylbi |
|- ( A e. RR* -> ( A +e 0 ) = A ) |