Metamath Proof Explorer

Theorem xmul01

Description: Extended real version of mul01 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmul01 
|- ( A e. RR* -> ( A *e 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 xmulval 
 |-  ( ( A e. RR* /\ 0 e. RR* ) -> ( A *e 0 ) = if ( ( A = 0 \/ 0 = 0 ) , 0 , if ( ( ( ( 0 < 0 /\ A = +oo ) \/ ( 0 < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ 0 = +oo ) \/ ( A < 0 /\ 0 = -oo ) ) ) , +oo , if ( ( ( ( 0 < 0 /\ A = -oo ) \/ ( 0 < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ 0 = -oo ) \/ ( A < 0 /\ 0 = +oo ) ) ) , -oo , ( A x. 0 ) ) ) ) )
3 1 2 mpan2 
 |-  ( A e. RR* -> ( A *e 0 ) = if ( ( A = 0 \/ 0 = 0 ) , 0 , if ( ( ( ( 0 < 0 /\ A = +oo ) \/ ( 0 < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ 0 = +oo ) \/ ( A < 0 /\ 0 = -oo ) ) ) , +oo , if ( ( ( ( 0 < 0 /\ A = -oo ) \/ ( 0 < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ 0 = -oo ) \/ ( A < 0 /\ 0 = +oo ) ) ) , -oo , ( A x. 0 ) ) ) ) )
4 eqid 
 |-  0 = 0
5 4 olci 
 |-  ( A = 0 \/ 0 = 0 )
6 5 iftruei 
 |-  if ( ( A = 0 \/ 0 = 0 ) , 0 , if ( ( ( ( 0 < 0 /\ A = +oo ) \/ ( 0 < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ 0 = +oo ) \/ ( A < 0 /\ 0 = -oo ) ) ) , +oo , if ( ( ( ( 0 < 0 /\ A = -oo ) \/ ( 0 < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ 0 = -oo ) \/ ( A < 0 /\ 0 = +oo ) ) ) , -oo , ( A x. 0 ) ) ) ) = 0
7 3 6 syl6eq 
 |-  ( A e. RR* -> ( A *e 0 ) = 0 )