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$$

Proof

Step	Hyp	Ref	Expression
1		0xr	$$⊢0\in {ℝ}^{*}$$
2		xaddcom	$$⊢\left(0\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\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$$