Description: A complex number whose sine is zero is an integer multiple of _pi . The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html . The Metamath form of the proof is sineq0ALT . The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 . The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/sineq0altro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sineq0ALT | |