Metamath Proof Explorer

Theorem xmulval

Description: Value of the extended real multiplication operation. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulval ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 = 𝐴 )
2 1 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 0 ↔ 𝐴 = 0 ) )
3 simpr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
4 3 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 = 0 ↔ 𝐵 = 0 ) )
5 2 4 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) ↔ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) )
6 3 breq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 0 < 𝑦 ↔ 0 < 𝐵 ) )
7 1 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = +∞ ↔ 𝐴 = +∞ ) )
8 6 7 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ↔ ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ) )
9 3 breq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 < 0 ↔ 𝐵 < 0 ) )
10 1 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = -∞ ↔ 𝐴 = -∞ ) )
11 9 10 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ↔ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) )
12 8 11 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ↔ ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ) )
13 1 breq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 0 < 𝑥 ↔ 0 < 𝐴 ) )
14 3 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 = +∞ ↔ 𝐵 = +∞ ) )
15 13 14 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ↔ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) )
16 1 breq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 < 0 ↔ 𝐴 < 0 ) )
17 3 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 = -∞ ↔ 𝐵 = -∞ ) )
18 16 17 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ↔ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) )
19 15 18 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ↔ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) )
20 12 19 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ↔ ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ) )
21 6 10 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ↔ ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ) )
22 9 7 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ↔ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) )
23 21 22 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ↔ ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ) )
24 13 17 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ↔ ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ) )
25 16 14 anbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ↔ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) )
26 24 25 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ↔ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
27 23 26 orbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ↔ ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) )
28 oveq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 · 𝑦 ) = ( 𝐴 · 𝐵 ) )
29 27 28 ifbieq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) = if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) )
30 20 29 ifbieq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) = if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) )
31 5 30 ifbieq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) )
32 df-xmul ⊢ ·e = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) )
33 c0ex ⊢ 0 ∈ V
34 pnfex ⊢ +∞ ∈ V
35 mnfxr ⊢ -∞ ∈ ℝ*
36 35 elexi ⊢ -∞ ∈ V
37 ovex ⊢ ( 𝐴 · 𝐵 ) ∈ V
38 36 37 ifex ⊢ if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ∈ V
39 34 38 ifex ⊢ if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ∈ V
40 33 39 ifex ⊢ if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) ∈ V
41 31 32 40 ovmpoa ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) = if ( ( 𝐴 = 0 ∨ 𝐵 = 0 ) , 0 , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) , -∞ , ( 𝐴 · 𝐵 ) ) ) ) )