This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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