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 4re 4
2 4pos 0 < 4
3 1 2 gt0ne0ii 4 0