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 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) )

Detailed syntax breakdown

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 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) )