Metamath Proof Explorer

Theorem xmulpnf1

Description: Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulpnf1 
|- ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )

Proof

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 )