Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Definitions and basic properties
oddp1eveni
Next ⟩
oddm1eveni
Metamath Proof Explorer
Ascii
Unicode
Theorem
oddp1eveni
Description:
The successor of an odd number is even.
(Contributed by
AV
, 16-Jun-2020)
Ref
Expression
Assertion
oddp1eveni
⊢
Z
∈
Odd
→
Z
+
1
∈
Even
Proof
Step
Hyp
Ref
Expression
1
oddz
⊢
Z
∈
Odd
→
Z
∈
ℤ
2
1
peano2zd
⊢
Z
∈
Odd
→
Z
+
1
∈
ℤ
3
oddp1div2z
⊢
Z
∈
Odd
→
Z
+
1
2
∈
ℤ
4
iseven
⊢
Z
+
1
∈
Even
↔
Z
+
1
∈
ℤ
∧
Z
+
1
2
∈
ℤ
5
2
3
4
sylanbrc
⊢
Z
∈
Odd
→
Z
+
1
∈
Even