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 )