Theorem oddp1eveni

Description: The successor of an odd number is even. (Contributed by AV, 16-Jun-2020)

	Ref	Expression
Assertion	oddp1eveni	⊢ ( 𝑍 ∈ Odd → ( 𝑍 + 1 ) ∈ Even )

Proof

Step	Hyp	Ref	Expression
1		oddz	⊢ ( 𝑍 ∈ Odd → 𝑍 ∈ ℤ )
2	1	peano2zd	⊢ ( 𝑍 ∈ Odd → ( 𝑍 + 1 ) ∈ ℤ )
3		oddp1div2z	⊢ ( 𝑍 ∈ Odd → ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ )
4		iseven	⊢ ( ( 𝑍 + 1 ) ∈ Even ↔ ( ( 𝑍 + 1 ) ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) )
5	2 3 4	sylanbrc	⊢ ( 𝑍 ∈ Odd → ( 𝑍 + 1 ) ∈ Even )