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−12∈ℤ
2 1 baib ⊢N∈ℤ→N∈Odd↔N−12∈ℤ
3 peano2zm ⊢N∈ℤ→N−1∈ℤ
4 3 biantrurd ⊢N∈ℤ→N−12∈ℤ↔N−1∈ℤ∧N−12∈ℤ
5 2 4 bitrd ⊢N∈ℤ→N∈Odd↔N−1∈ℤ∧N−12∈ℤ
6 iseven ⊢N−1∈Even↔N−1∈ℤ∧N−12∈ℤ
7 5 6 bitr4di ⊢N∈ℤ→N∈Odd↔N−1∈Even