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

Metamath Proof Explorer

Theorem 0dvds0

Description: 0 divides 0. (Contributed by SN, 15-Sep-2024)

Ref Expression
Assertion 0dvds0 
|- 0 || 0

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 dvds0 
 |-  ( 0 e. ZZ -> 0 || 0 )
3 1 2 ax-mp 
 |-  0 || 0