This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ ℂ
sn-addid0.1 ⊢ φ → A + A = A
Assertion sn-addid0 ⊢ φ → A = 0

Proof

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