Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Additional theorems
7odd
Next ⟩
8even
Metamath Proof Explorer
Ascii
Unicode
Theorem
7odd
Description:
7 is an odd number.
(Contributed by
AV
, 20-Jul-2020)
Ref
Expression
Assertion
7odd
⊢
7
∈
Odd
Proof
Step
Hyp
Ref
Expression
1
df-7
⊢
7
=
6
+
1
2
6even
⊢
6
∈
Even
3
evenp1odd
⊢
6
∈
Even
→
6
+
1
∈
Odd
4
2
3
ax-mp
⊢
6
+
1
∈
Odd
5
1
4
eqeltri
⊢
7
∈
Odd