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 )