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

Metamath Proof Explorer

Theorem xaddlid

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

		Ref	Expression
	Assertion	xaddlid	$⊢ A \in ℝ^{*} \to 0 +_{𝑒} A = A$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		xaddcom	$⊢ (0 \in ℝ^{} \land A \in ℝ^{}) \to 0 +_{𝑒} A = A +_{𝑒} 0$
3	1 2	mpan	$⊢ A \in ℝ^{*} \to 0 +_{𝑒} A = A +_{𝑒} 0$
4		xaddrid	$⊢ A \in ℝ^{*} \to A +_{𝑒} 0 = A$
5	3 4	eqtrd	$⊢ A \in ℝ^{*} \to 0 +_{𝑒} A = A$