Theorem sn-addid1

Description: addid1 without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-addid1	$$⊢A\in ℂ\to A+0=A$$

Proof

Step	Hyp	Ref	Expression
1		sn-negex2	$$⊢A\in ℂ\to \exists x\in ℂx+A=0$$
2		simprr	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to x+A=0$$
3	2	oveq1d	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to x+A+0=0+0$$
4		sn-00id	$$⊢0+0=0$$
5	3 4	eqtrdi	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to x+A+0=0$$
6		simprl	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to x\in ℂ$$
7		simpl	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to A\in ℂ$$
8		0cnd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to 0\in ℂ$$
9	6 7 8	addassd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to x+A+0=x+A+0$$
10	2 5 9	3eqtr2rd	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to x+A+0=x+A$$
11	7 8	addcld	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to A+0\in ℂ$$
12	6 11 7	sn-addcand	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to \left(x+A+0=x+A\leftrightarrow A+0=A\right)$$
13	10 12	mpbid	$$⊢\left(A\in ℂ\wedge \left(x\in ℂ\wedge x+A=0\right)\right)\to A+0=A$$
14	1 13	rexlimddv	$$⊢A\in ℂ\to A+0=A$$