Step |
Hyp |
Ref |
Expression |
1 |
|
pnfxr |
|- +oo e. RR* |
2 |
|
xmulval |
|- ( ( A e. RR* /\ +oo e. RR* ) -> ( A *e +oo ) = if ( ( A = 0 \/ +oo = 0 ) , 0 , if ( ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) , +oo , if ( ( ( ( 0 < +oo /\ A = -oo ) \/ ( +oo < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ +oo = -oo ) \/ ( A < 0 /\ +oo = +oo ) ) ) , -oo , ( A x. +oo ) ) ) ) ) |
3 |
1 2
|
mpan2 |
|- ( A e. RR* -> ( A *e +oo ) = if ( ( A = 0 \/ +oo = 0 ) , 0 , if ( ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) , +oo , if ( ( ( ( 0 < +oo /\ A = -oo ) \/ ( +oo < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ +oo = -oo ) \/ ( A < 0 /\ +oo = +oo ) ) ) , -oo , ( A x. +oo ) ) ) ) ) |
4 |
3
|
adantr |
|- ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = if ( ( A = 0 \/ +oo = 0 ) , 0 , if ( ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) , +oo , if ( ( ( ( 0 < +oo /\ A = -oo ) \/ ( +oo < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ +oo = -oo ) \/ ( A < 0 /\ +oo = +oo ) ) ) , -oo , ( A x. +oo ) ) ) ) ) |
5 |
|
0xr |
|- 0 e. RR* |
6 |
|
xrltne |
|- ( ( 0 e. RR* /\ A e. RR* /\ 0 < A ) -> A =/= 0 ) |
7 |
5 6
|
mp3an1 |
|- ( ( A e. RR* /\ 0 < A ) -> A =/= 0 ) |
8 |
|
0re |
|- 0 e. RR |
9 |
|
renepnf |
|- ( 0 e. RR -> 0 =/= +oo ) |
10 |
8 9
|
ax-mp |
|- 0 =/= +oo |
11 |
10
|
necomi |
|- +oo =/= 0 |
12 |
|
neanior |
|- ( ( A =/= 0 /\ +oo =/= 0 ) <-> -. ( A = 0 \/ +oo = 0 ) ) |
13 |
7 11 12
|
sylanblc |
|- ( ( A e. RR* /\ 0 < A ) -> -. ( A = 0 \/ +oo = 0 ) ) |
14 |
13
|
iffalsed |
|- ( ( A e. RR* /\ 0 < A ) -> if ( ( A = 0 \/ +oo = 0 ) , 0 , if ( ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) , +oo , if ( ( ( ( 0 < +oo /\ A = -oo ) \/ ( +oo < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ +oo = -oo ) \/ ( A < 0 /\ +oo = +oo ) ) ) , -oo , ( A x. +oo ) ) ) ) = if ( ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) , +oo , if ( ( ( ( 0 < +oo /\ A = -oo ) \/ ( +oo < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ +oo = -oo ) \/ ( A < 0 /\ +oo = +oo ) ) ) , -oo , ( A x. +oo ) ) ) ) |
15 |
|
simpr |
|- ( ( A e. RR* /\ 0 < A ) -> 0 < A ) |
16 |
|
eqid |
|- +oo = +oo |
17 |
15 16
|
jctir |
|- ( ( A e. RR* /\ 0 < A ) -> ( 0 < A /\ +oo = +oo ) ) |
18 |
17
|
orcd |
|- ( ( A e. RR* /\ 0 < A ) -> ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) |
19 |
18
|
olcd |
|- ( ( A e. RR* /\ 0 < A ) -> ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) ) |
20 |
19
|
iftrued |
|- ( ( A e. RR* /\ 0 < A ) -> if ( ( ( ( 0 < +oo /\ A = +oo ) \/ ( +oo < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ +oo = +oo ) \/ ( A < 0 /\ +oo = -oo ) ) ) , +oo , if ( ( ( ( 0 < +oo /\ A = -oo ) \/ ( +oo < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ +oo = -oo ) \/ ( A < 0 /\ +oo = +oo ) ) ) , -oo , ( A x. +oo ) ) ) = +oo ) |
21 |
4 14 20
|
3eqtrd |
|- ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo ) |