xmulrid

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

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

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		1re	$⊢ 1 \in ℝ$
3		rexmul	$⊢ (A \in ℝ \land 1 \in ℝ) \to A \cdot_{𝑒} 1 = A \cdot 1$
4	2 3	mpan2	$⊢ A \in ℝ \to A \cdot_{𝑒} 1 = A \cdot 1$
5		ax-1rid	$⊢ A \in ℝ \to A \cdot 1 = A$
6	4 5	eqtrd	$⊢ A \in ℝ \to A \cdot_{𝑒} 1 = A$
7		1xr	$⊢ 1 \in ℝ^{*}$
8		0lt1	$⊢ 0 < 1$
9		xmulpnf2	$⊢ (1 \in ℝ^{*} \land 0 < 1) \to +∞ \cdot_{𝑒} 1 = +∞$
10	7 8 9	mp2an	$⊢ +∞ \cdot_{𝑒} 1 = +∞$
11		oveq1	$⊢ A = +∞ \to A \cdot_{𝑒} 1 = +∞ \cdot_{𝑒} 1$
12		id	$⊢ A = +∞ \to A = +∞$
13	10 11 12	3eqtr4a	$⊢ A = +∞ \to A \cdot_{𝑒} 1 = A$
14		xmulmnf2	$⊢ (1 \in ℝ^{*} \land 0 < 1) \to −∞ \cdot_{𝑒} 1 = −∞$
15	7 8 14	mp2an	$⊢ −∞ \cdot_{𝑒} 1 = −∞$
16		oveq1	$⊢ A = −∞ \to A \cdot_{𝑒} 1 = −∞ \cdot_{𝑒} 1$
17		id	$⊢ A = −∞ \to A = −∞$
18	15 16 17	3eqtr4a	$⊢ A = −∞ \to A \cdot_{𝑒} 1 = A$
19	6 13 18	3jaoi	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \to A \cdot_{𝑒} 1 = A$
20	1 19	sylbi	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 1 = A$

Metamath Proof Explorer