Metamath Proof Explorer

Theorem xmulf

Description: The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xmulf ·e : ( ℝ* × ℝ* ) ⟶ ℝ*

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ*
2 1 a1i ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) → 0 ∈ ℝ* )
3 pnfxr ⊢ +∞ ∈ ℝ*
4 3 a1i ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) → +∞ ∈ ℝ* )
5 mnfxr ⊢ -∞ ∈ ℝ*
6 5 a1i ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) ∧ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ) → -∞ ∈ ℝ* )
7 xmullem ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ) → 𝑥 ∈ ℝ )
8 ancom ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ↔ ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) )
9 orcom ⊢ ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) ↔ ( 𝑦 = 0 ∨ 𝑥 = 0 ) )
10 9 notbii ⊢ ( ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ↔ ¬ ( 𝑦 = 0 ∨ 𝑥 = 0 ) )
11 8 10 anbi12i ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ↔ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) ∧ ¬ ( 𝑦 = 0 ∨ 𝑥 = 0 ) ) )
12 orcom ⊢ ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ↔ ( ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ) )
13 12 notbii ⊢ ( ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ↔ ¬ ( ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ) )
14 11 13 anbi12i ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) ↔ ( ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) ∧ ¬ ( 𝑦 = 0 ∨ 𝑥 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ) ) )
15 orcom ⊢ ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ↔ ( ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ) )
16 15 notbii ⊢ ( ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ↔ ¬ ( ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ) )
17 xmullem ⊢ ( ( ( ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) ∧ ¬ ( 𝑦 = 0 ∨ 𝑥 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ) ) ∧ ¬ ( ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ∨ ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ) ) → 𝑦 ∈ ℝ )
18 14 16 17 syl2anb ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ) → 𝑦 ∈ ℝ )
19 7 18 remulcld ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
20 19 rexrd ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ* )
21 6 20 ifclda ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) ) → if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ∈ ℝ* )
22 4 21 ifclda ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) → if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ∈ ℝ* )
23 2 22 ifclda ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) ∈ ℝ* )
24 23 rgen2 ⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) ∈ ℝ*
25 df-xmul ⊢ ·e = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) )
26 25 fmpo ⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = +∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = -∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = +∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 𝑦 ∧ 𝑥 = -∞ ) ∨ ( 𝑦 < 0 ∧ 𝑥 = +∞ ) ) ∨ ( ( 0 < 𝑥 ∧ 𝑦 = -∞ ) ∨ ( 𝑥 < 0 ∧ 𝑦 = +∞ ) ) ) , -∞ , ( 𝑥 · 𝑦 ) ) ) ) ∈ ℝ* ↔ ·e : ( ℝ* × ℝ* ) ⟶ ℝ* )
27 24 26 mpbi ⊢ ·e : ( ℝ* × ℝ* ) ⟶ ℝ*