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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
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 )