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

Metamath Proof Explorer

Theorem xmul01

Description: Extended real version of mul01 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmul01 ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ*
2 xmulval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐴 ·e 0 ) = if ( ( 𝐴 = 0 ∨ 0 = 0 ) , 0 , if ( ( ( ( 0 < 0 ∧ 𝐴 = +∞ ) ∨ ( 0 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 0 = +∞ ) ∨ ( 𝐴 < 0 ∧ 0 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 0 ∧ 𝐴 = -∞ ) ∨ ( 0 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 0 = -∞ ) ∨ ( 𝐴 < 0 ∧ 0 = +∞ ) ) ) , -∞ , ( 𝐴 · 0 ) ) ) ) )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = if ( ( 𝐴 = 0 ∨ 0 = 0 ) , 0 , if ( ( ( ( 0 < 0 ∧ 𝐴 = +∞ ) ∨ ( 0 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 0 = +∞ ) ∨ ( 𝐴 < 0 ∧ 0 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 0 ∧ 𝐴 = -∞ ) ∨ ( 0 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 0 = -∞ ) ∨ ( 𝐴 < 0 ∧ 0 = +∞ ) ) ) , -∞ , ( 𝐴 · 0 ) ) ) ) )
4 eqid ⊢ 0 = 0
5 4 olci ⊢ ( 𝐴 = 0 ∨ 0 = 0 )
6 5 iftruei ⊢ if ( ( 𝐴 = 0 ∨ 0 = 0 ) , 0 , if ( ( ( ( 0 < 0 ∧ 𝐴 = +∞ ) ∨ ( 0 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 0 = +∞ ) ∨ ( 𝐴 < 0 ∧ 0 = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < 0 ∧ 𝐴 = -∞ ) ∨ ( 0 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 0 = -∞ ) ∨ ( 𝐴 < 0 ∧ 0 = +∞ ) ) ) , -∞ , ( 𝐴 · 0 ) ) ) ) = 0
7 3 6 eqtrdi ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 )