Metamath Proof Explorer

Theorem evennodd

Description: An even number is not an odd number. (Contributed by AV, 16-Jun-2020)

Ref Expression
Assertion evennodd 
|- ( Z e. Even -> -. Z e. Odd )

Proof

Step Hyp Ref Expression
1 iseven 
 |-  ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
2 zeo2 
 |-  ( Z e. ZZ -> ( ( Z / 2 ) e. ZZ <-> -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
3 2 biimpd 
 |-  ( Z e. ZZ -> ( ( Z / 2 ) e. ZZ -> -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
4 3 imp 
 |-  ( ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) -> -. ( ( Z + 1 ) / 2 ) e. ZZ )
5 1 4 sylbi 
 |-  ( Z e. Even -> -. ( ( Z + 1 ) / 2 ) e. ZZ )
6 5 olcd 
 |-  ( Z e. Even -> ( -. Z e. ZZ \/ -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
7 isodd 
 |-  ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
8 7 notbii 
 |-  ( -. Z e. Odd <-> -. ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
9 ianor 
 |-  ( -. ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) <-> ( -. Z e. ZZ \/ -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
10 8 9 bitri 
 |-  ( -. Z e. Odd <-> ( -. Z e. ZZ \/ -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
11 6 10 sylibr 
 |-  ( Z e. Even -> -. Z e. Odd )