Theorem evenm1odd

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

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

Proof

Step	Hyp	Ref	Expression
1		evenz	⊢ ( 𝑍 ∈ Even → 𝑍 ∈ ℤ )
2		peano2zm	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 − 1 ) ∈ ℤ )
3	1 2	syl	⊢ ( 𝑍 ∈ Even → ( 𝑍 − 1 ) ∈ ℤ )
4		iseven	⊢ ( 𝑍 ∈ Even ↔ ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) )
5		zcn	⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ℂ )
6		npcan1	⊢ ( 𝑍 ∈ ℂ → ( ( 𝑍 − 1 ) + 1 ) = 𝑍 )
7	5 6	syl	⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 − 1 ) + 1 ) = 𝑍 )
8	7	eqcomd	⊢ ( 𝑍 ∈ ℤ → 𝑍 = ( ( 𝑍 − 1 ) + 1 ) )
9	8	oveq1d	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 / 2 ) = ( ( ( 𝑍 − 1 ) + 1 ) / 2 ) )
10	9	eleq1d	⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 / 2 ) ∈ ℤ ↔ ( ( ( 𝑍 − 1 ) + 1 ) / 2 ) ∈ ℤ ) )
11	10	biimpa	⊢ ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) → ( ( ( 𝑍 − 1 ) + 1 ) / 2 ) ∈ ℤ )
12	4 11	sylbi	⊢ ( 𝑍 ∈ Even → ( ( ( 𝑍 − 1 ) + 1 ) / 2 ) ∈ ℤ )
13		isodd	⊢ ( ( 𝑍 − 1 ) ∈ Odd ↔ ( ( 𝑍 − 1 ) ∈ ℤ ∧ ( ( ( 𝑍 − 1 ) + 1 ) / 2 ) ∈ ℤ ) )
14	3 12 13	sylanbrc	⊢ ( 𝑍 ∈ Even → ( 𝑍 − 1 ) ∈ Odd )