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