Metamath Proof Explorer

Definition df-xmul

Description: Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion 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 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxmu 
 |-  *e
1 vx 
 |-  x
2 cxr 
 |-  RR*
3 vy 
 |-  y
4 1 cv 
 |-  x
5 cc0 
 |-  0
6 4 5 wceq 
 |-  x = 0
7 3 cv 
 |-  y
8 7 5 wceq 
 |-  y = 0
9 6 8 wo 
 |-  ( x = 0 \/ y = 0 )
10 clt 
 |-  <
11 5 7 10 wbr 
 |-  0 < y
12 cpnf 
 |-  +oo
13 4 12 wceq 
 |-  x = +oo
14 11 13 wa 
 |-  ( 0 < y /\ x = +oo )
15 7 5 10 wbr 
 |-  y < 0
16 cmnf 
 |-  -oo
17 4 16 wceq 
 |-  x = -oo
18 15 17 wa 
 |-  ( y < 0 /\ x = -oo )
19 14 18 wo 
 |-  ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) )
20 5 4 10 wbr 
 |-  0 < x
21 7 12 wceq 
 |-  y = +oo
22 20 21 wa 
 |-  ( 0 < x /\ y = +oo )
23 4 5 10 wbr 
 |-  x < 0
24 7 16 wceq 
 |-  y = -oo
25 23 24 wa 
 |-  ( x < 0 /\ y = -oo )
26 22 25 wo 
 |-  ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) )
27 19 26 wo 
 |-  ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) )
28 11 17 wa 
 |-  ( 0 < y /\ x = -oo )
29 15 13 wa 
 |-  ( y < 0 /\ x = +oo )
30 28 29 wo 
 |-  ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) )
31 20 24 wa 
 |-  ( 0 < x /\ y = -oo )
32 23 21 wa 
 |-  ( x < 0 /\ y = +oo )
33 31 32 wo 
 |-  ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) )
34 30 33 wo 
 |-  ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) )
35 cmul 
 |-  x.
36 4 7 35 co 
 |-  ( x x. y )
37 34 16 36 cif 
 |-  if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) )
38 27 12 37 cif 
 |-  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 ) ) )
39 9 5 38 cif 
 |-  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 ) ) ) )
40 1 3 2 2 39 cmpo 
 |-  ( 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 ) ) ) ) )
41 0 40 wceq 
 |-  *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 ) ) ) ) )