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

Metamath Proof Explorer

Theorem msq0i

Description: A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by NM, 28-Jul-1999)

Ref Expression
Hypothesis msq0i.1 ⊢ 𝐴 ∈ ℂ
Assertion msq0i ( ( 𝐴 · 𝐴 ) = 0 ↔ 𝐴 = 0 )

Proof

Step Hyp Ref Expression
1 msq0i.1 ⊢ 𝐴 ∈ ℂ
2 1 1 mul0ori ⊢ ( ( 𝐴 · 𝐴 ) = 0 ↔ ( 𝐴 = 0 ∨ 𝐴 = 0 ) )
3 oridm ⊢ ( ( 𝐴 = 0 ∨ 𝐴 = 0 ) ↔ 𝐴 = 0 )
4 2 3 bitri ⊢ ( ( 𝐴 · 𝐴 ) = 0 ↔ 𝐴 = 0 )