Theorem sn-addid0

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

	Ref	Expression
Hypotheses	sn-addid0.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	sn-addid0.1	⊢ ( 𝜑 → ( 𝐴 + 𝐴 ) = 𝐴 )
Assertion	sn-addid0	⊢ ( 𝜑 → 𝐴 = 0 )

Proof

Step	Hyp	Ref	Expression
1		sn-addid0.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		sn-addid0.1	⊢ ( 𝜑 → ( 𝐴 + 𝐴 ) = 𝐴 )
3		sn-addrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )
4	1 3	syl	⊢ ( 𝜑 → ( 𝐴 + 0 ) = 𝐴 )
5	2 4	eqtr4d	⊢ ( 𝜑 → ( 𝐴 + 𝐴 ) = ( 𝐴 + 0 ) )
6		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
7	1 1 6	sn-addcand	⊢ ( 𝜑 → ( ( 𝐴 + 𝐴 ) = ( 𝐴 + 0 ) ↔ 𝐴 = 0 ) )
8	5 7	mpbid	⊢ ( 𝜑 → 𝐴 = 0 )