Metamath Proof Explorer

Theorem xmulval

Description: Value of the extended real multiplication operation. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulval 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( x = A /\ y = B ) -> x = A )
2 1 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( x = 0 <-> A = 0 ) )
3 simpr 
 |-  ( ( x = A /\ y = B ) -> y = B )
4 3 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( y = 0 <-> B = 0 ) )
5 2 4 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( x = 0 \/ y = 0 ) <-> ( A = 0 \/ B = 0 ) ) )
6 3 breq2d 
 |-  ( ( x = A /\ y = B ) -> ( 0 < y <-> 0 < B ) )
7 1 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( x = +oo <-> A = +oo ) )
8 6 7 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( 0 < y /\ x = +oo ) <-> ( 0 < B /\ A = +oo ) ) )
9 3 breq1d 
 |-  ( ( x = A /\ y = B ) -> ( y < 0 <-> B < 0 ) )
10 1 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( x = -oo <-> A = -oo ) )
11 9 10 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( y < 0 /\ x = -oo ) <-> ( B < 0 /\ A = -oo ) ) )
12 8 11 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) <-> ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) ) )
13 1 breq2d 
 |-  ( ( x = A /\ y = B ) -> ( 0 < x <-> 0 < A ) )
14 3 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( y = +oo <-> B = +oo ) )
15 13 14 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( 0 < x /\ y = +oo ) <-> ( 0 < A /\ B = +oo ) ) )
16 1 breq1d 
 |-  ( ( x = A /\ y = B ) -> ( x < 0 <-> A < 0 ) )
17 3 eqeq1d 
 |-  ( ( x = A /\ y = B ) -> ( y = -oo <-> B = -oo ) )
18 16 17 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( x < 0 /\ y = -oo ) <-> ( A < 0 /\ B = -oo ) ) )
19 15 18 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) <-> ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) )
20 12 19 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) <-> ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) )
21 6 10 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( 0 < y /\ x = -oo ) <-> ( 0 < B /\ A = -oo ) ) )
22 9 7 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( y < 0 /\ x = +oo ) <-> ( B < 0 /\ A = +oo ) ) )
23 21 22 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) <-> ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
24 13 17 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( 0 < x /\ y = -oo ) <-> ( 0 < A /\ B = -oo ) ) )
25 16 14 anbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( x < 0 /\ y = +oo ) <-> ( A < 0 /\ B = +oo ) ) )
26 24 25 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) <-> ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) )
27 23 26 orbi12d 
 |-  ( ( x = A /\ y = B ) -> ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) <-> ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) )
28 oveq12 
 |-  ( ( x = A /\ y = B ) -> ( x x. y ) = ( A x. B ) )
29 27 28 ifbieq2d 
 |-  ( ( x = A /\ y = B ) -> if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) = if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) )
30 20 29 ifbieq2d 
 |-  ( ( x = A /\ y = B ) -> if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) = if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) )
31 5 30 ifbieq2d 
 |-  ( ( x = A /\ y = B ) -> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )
32 df-xmul 
 |-  *e = ( x e. RR* , y e. RR* |-> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) )
33 c0ex 
 |-  0 e. _V
34 pnfex 
 |-  +oo e. _V
35 mnfxr 
 |-  -oo e. RR*
36 35 elexi 
 |-  -oo e. _V
37 ovex 
 |-  ( A x. B ) e. _V
38 36 37 ifex 
 |-  if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) e. _V
39 34 38 ifex 
 |-  if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) e. _V
40 33 39 ifex 
 |-  if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) e. _V
41 31 32 40 ovmpoa 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) = if ( ( A = 0 \/ B = 0 ) , 0 , if ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) , +oo , if ( ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) , -oo , ( A x. B ) ) ) ) )