Metamath Proof Explorer


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 )