Step |
Hyp |
Ref |
Expression |
0 |
|
cxmu |
⊢ ·e |
1 |
|
vx |
⊢ 𝑥 |
2 |
|
cxr |
⊢ ℝ* |
3 |
|
vy |
⊢ 𝑦 |
4 |
1
|
cv |
⊢ 𝑥 |
5 |
|
cc0 |
⊢ 0 |
6 |
4 5
|
wceq |
⊢ 𝑥 = 0 |
7 |
3
|
cv |
⊢ 𝑦 |
8 |
7 5
|
wceq |
⊢ 𝑦 = 0 |
9 |
6 8
|
wo |
⊢ ( 𝑥 = 0 ∨ 𝑦 = 0 ) |
10 |
|
clt |
⊢ < |
11 |
5 7 10
|
wbr |
⊢ 0 < 𝑦 |
12 |
|
cpnf |
⊢ +∞ |
13 |
4 12
|
wceq |
⊢ 𝑥 = +∞ |
14 |
11 13
|
wa |
⊢ ( 0 < 𝑦 ∧ 𝑥 = +∞ ) |
15 |
7 5 10
|
wbr |
⊢ 𝑦 < 0 |
16 |
|
cmnf |
⊢ -∞ |
17 |
4 16
|
wceq |
⊢ 𝑥 = -∞ |
18 |
15 17
|
wa |
⊢ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) |
19 |
14 18
|
wo |
⊢ ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) |
20 |
5 4 10
|
wbr |
⊢ 0 < 𝑥 |
21 |
7 12
|
wceq |
⊢ 𝑦 = +∞ |
22 |
20 21
|
wa |
⊢ ( 0 < 𝑥 ∧ 𝑦 = +∞ ) |
23 |
4 5 10
|
wbr |
⊢ 𝑥 < 0 |
24 |
7 16
|
wceq |
⊢ 𝑦 = -∞ |
25 |
23 24
|
wa |
⊢ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) |
26 |
22 25
|
wo |
⊢ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) |
27 |
19 26
|
wo |
⊢ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) |
28 |
11 17
|
wa |
⊢ ( 0 < 𝑦 ∧ 𝑥 = -∞ ) |
29 |
15 13
|
wa |
⊢ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) |
30 |
28 29
|
wo |
⊢ ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) |
31 |
20 24
|
wa |
⊢ ( 0 < 𝑥 ∧ 𝑦 = -∞ ) |
32 |
23 21
|
wa |
⊢ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) |
33 |
31 32
|
wo |
⊢ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) |
34 |
30 33
|
wo |
⊢ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) |
35 |
|
cmul |
⊢ · |
36 |
4 7 35
|
co |
⊢ ( 𝑥 · 𝑦 ) |
37 |
34 16 36
|
cif |
⊢ if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) |
38 |
27 12 37
|
cif |
⊢ if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) |
39 |
9 5 38
|
cif |
⊢ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) |
40 |
1 3 2 2 39
|
cmpo |
⊢ ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) ) |
41 |
0 40
|
wceq |
⊢ ·e = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) ) |