Metamath Proof Explorer


Theorem msq0d

Description: A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis msq0d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
Assertion msq0d ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ด ) = 0 โ†” ๐ด = 0 ) )

Proof

Step Hyp Ref Expression
1 msq0d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 mul0or โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ด ) = 0 โ†” ( ๐ด = 0 โˆจ ๐ด = 0 ) ) )
3 1 1 2 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ด ) = 0 โ†” ( ๐ด = 0 โˆจ ๐ด = 0 ) ) )
4 oridm โŠข ( ( ๐ด = 0 โˆจ ๐ด = 0 ) โ†” ๐ด = 0 )
5 3 4 bitrdi โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ด ) = 0 โ†” ๐ด = 0 ) )