Theorem sn-addid0

Description: A number that sums to itself is zero. Compare addid0 , readdid1addid2d . (Contributed by SN, 5-May-2024)

	Ref	Expression
Hypotheses	sn-addid0.a	$$⊢\phi \to A\in ℂ$$
	sn-addid0.1	$$⊢\phi \to A+A=A$$
Assertion	sn-addid0	$$⊢\phi \to A=0$$

Proof

Step	Hyp	Ref	Expression
1		sn-addid0.a	$$⊢\phi \to A\in ℂ$$
2		sn-addid0.1	$$⊢\phi \to A+A=A$$
3		sn-addid1	$$⊢A\in ℂ\to A+0=A$$
4	1 3	syl	$$⊢\phi \to A+0=A$$
5	2 4	eqtr4d	$$⊢\phi \to A+A=A+0$$
6		0cnd	$$⊢\phi \to 0\in ℂ$$
7	1 1 6	sn-addcand	$$⊢\phi \to \left(A+A=A+0\leftrightarrow A=0\right)$$
8	5 7	mpbid	$$⊢\phi \to A=0$$