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	syl6eq	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 )