This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )