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