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 e. ZZ -> ( N e. Odd <-> ( N - 1 ) e. Even ) )

Proof

Step Hyp Ref Expression
1 isodd2 
 |-  ( N e. Odd <-> ( N e. ZZ /\ ( ( N - 1 ) / 2 ) e. ZZ ) )
2 1 baib 
 |-  ( N e. ZZ -> ( N e. Odd <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
3 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
4 3 biantrurd 
 |-  ( N e. ZZ -> ( ( ( N - 1 ) / 2 ) e. ZZ <-> ( ( N - 1 ) e. ZZ /\ ( ( N - 1 ) / 2 ) e. ZZ ) ) )
5 2 4 bitrd 
 |-  ( N e. ZZ -> ( N e. Odd <-> ( ( N - 1 ) e. ZZ /\ ( ( N - 1 ) / 2 ) e. ZZ ) ) )
6 iseven 
 |-  ( ( N - 1 ) e. Even <-> ( ( N - 1 ) e. ZZ /\ ( ( N - 1 ) / 2 ) e. ZZ ) )
7 5 6 bitr4di 
 |-  ( N e. ZZ -> ( N e. Odd <-> ( N - 1 ) e. Even ) )