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	|- ( ph -> A e. CC )
	sn-addid0.1	|- ( ph -> ( A + A ) = A )
Assertion	sn-addid0	|- ( ph -> A = 0 )

Proof

Step	Hyp	Ref	Expression
1		sn-addid0.a	|- ( ph -> A e. CC )
2		sn-addid0.1	|- ( ph -> ( A + A ) = A )
3		sn-addid1	|- ( A e. CC -> ( A + 0 ) = A )
4	1 3	syl	|- ( ph -> ( A + 0 ) = A )
5	2 4	eqtr4d	|- ( ph -> ( A + A ) = ( A + 0 ) )
6		0cnd	|- ( ph -> 0 e. CC )
7	1 1 6	sn-addcand	|- ( ph -> ( ( A + A ) = ( A + 0 ) <-> A = 0 ) )
8	5 7	mpbid	|- ( ph -> A = 0 )