Theorem oddm1eveni

Description: The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020)

	Ref	Expression
Assertion	oddm1eveni	⊢ ( 𝑍 ∈ Odd → ( 𝑍 − 1 ) ∈ Even )

Proof

Step	Hyp	Ref	Expression
1		oddz	⊢ ( 𝑍 ∈ Odd → 𝑍 ∈ ℤ )
2		peano2zm	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 − 1 ) ∈ ℤ )
3	1 2	syl	⊢ ( 𝑍 ∈ Odd → ( 𝑍 − 1 ) ∈ ℤ )
4		oddm1div2z	⊢ ( 𝑍 ∈ Odd → ( ( 𝑍 − 1 ) / 2 ) ∈ ℤ )
5		iseven	⊢ ( ( 𝑍 − 1 ) ∈ Even ↔ ( ( 𝑍 − 1 ) ∈ ℤ ∧ ( ( 𝑍 − 1 ) / 2 ) ∈ ℤ ) )
6	3 4 5	sylanbrc	⊢ ( 𝑍 ∈ Odd → ( 𝑍 − 1 ) ∈ Even )