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