Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
5ne0
Next ⟩
6ne0
Metamath Proof Explorer
Unicode
Structured
Theorem
5ne0
Description:
The number 5 is nonzero.
(Contributed by
SN
, 22-Oct-2025)
Ref
Expression
Assertion
5ne0
|- 5 =/= 0
Proof
Step
Hyp
Ref
Expression
1
5nn
|- 5 e. NN
2
1
nnne0i
|- 5 =/= 0