Metamath Proof Explorer

Theorem oddm1evenALTV

Description: An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

Ref Expression
Assertion oddm1evenALTV ⊢ N ∈ ℤ → N ∈ Odd ↔ N − 1 ∈ Even

Proof

Step Hyp Ref Expression
1 isodd2 ⊢ N ∈ Odd ↔ N ∈ ℤ ∧ N − 1 2 ∈ ℤ
2 1 baib ⊢ N ∈ ℤ → N ∈ Odd ↔ N − 1 2 ∈ ℤ
3 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
4 3 biantrurd ⊢ N ∈ ℤ → N − 1 2 ∈ ℤ ↔ N − 1 ∈ ℤ ∧ N − 1 2 ∈ ℤ
5 2 4 bitrd ⊢ N ∈ ℤ → N ∈ Odd ↔ N − 1 ∈ ℤ ∧ N − 1 2 ∈ ℤ
6 iseven ⊢ N − 1 ∈ Even ↔ N − 1 ∈ ℤ ∧ N − 1 2 ∈ ℤ
7 5 6 bitr4di ⊢ N ∈ ℤ → N ∈ Odd ↔ N − 1 ∈ Even