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 e. RR
2 4pos 
 |-  0 < 4
3 1 2 gt0ne0ii 
 |-  4 =/= 0