Metamath Proof Explorer


Theorem 4ne0

Description: The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018)

Ref Expression
Assertion 4ne0 4 0

Proof

Step Hyp Ref Expression
1 4nn 4
2 1 nnne0i 4 0