Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
9ne0
Next ⟩
sn-1ne2
Metamath Proof Explorer
Ascii
Unicode
Theorem
9ne0
Description:
The number 9 is nonzero.
(Contributed by
SN
, 22-Oct-2025)
Ref
Expression
Assertion
9ne0
⊢
9
≠
0
Proof
Step
Hyp
Ref
Expression
1
9nn
⊢
9
∈
ℕ
2
1
nnne0i
⊢
9
≠
0