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 ) ) ) ) )