xmul01

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

		Ref	Expression
	Assertion	xmul01	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = 0$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		xmulval	$⊢ (A \in ℝ^{} \land 0 \in ℝ^{}) \to A \cdot_{𝑒} 0 = if ((A = 0 \lor 0 = 0), 0, if ((((0 < 0 \land A = +∞) \lor (0 < 0 \land A = −∞)) \lor ((0 < A \land 0 = +∞) \lor (A < 0 \land 0 = −∞))), +∞, if ((((0 < 0 \land A = −∞) \lor (0 < 0 \land A = +∞)) \lor ((0 < A \land 0 = −∞) \lor (A < 0 \land 0 = +∞))), −∞, A \cdot 0)))$
3	1 2	mpan2	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = if ((A = 0 \lor 0 = 0), 0, if ((((0 < 0 \land A = +∞) \lor (0 < 0 \land A = −∞)) \lor ((0 < A \land 0 = +∞) \lor (A < 0 \land 0 = −∞))), +∞, if ((((0 < 0 \land A = −∞) \lor (0 < 0 \land A = +∞)) \lor ((0 < A \land 0 = −∞) \lor (A < 0 \land 0 = +∞))), −∞, A \cdot 0)))$
4		eqid	$⊢ 0 = 0$
5	4	olci	$⊢ (A = 0 \lor 0 = 0)$
6	5	iftruei	$⊢ if ((A = 0 \lor 0 = 0), 0, if ((((0 < 0 \land A = +∞) \lor (0 < 0 \land A = −∞)) \lor ((0 < A \land 0 = +∞) \lor (A < 0 \land 0 = −∞))), +∞, if ((((0 < 0 \land A = −∞) \lor (0 < 0 \land A = +∞)) \lor ((0 < A \land 0 = −∞) \lor (A < 0 \land 0 = +∞))), −∞, A \cdot 0))) = 0$
7	3 6	syl6eq	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = 0$

Metamath Proof Explorer