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

Metamath Proof Explorer

Theorem oddneven

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

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

Proof

Step Hyp Ref Expression
1 isodd 
 |-  ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z + 1 ) / 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 con2d 
 |-  ( Z e. ZZ -> ( ( ( Z + 1 ) / 2 ) e. ZZ -> -. ( Z / 2 ) e. ZZ ) )
5 4 imp 
 |-  ( ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) -> -. ( Z / 2 ) e. ZZ )
6 1 5 sylbi 
 |-  ( Z e. Odd -> -. ( Z / 2 ) e. ZZ )
7 6 olcd 
 |-  ( Z e. Odd -> ( -. Z e. ZZ \/ -. ( Z / 2 ) e. ZZ ) )
8 ianor 
 |-  ( -. ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) <-> ( -. Z e. ZZ \/ -. ( Z / 2 ) e. ZZ ) )
9 iseven 
 |-  ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
10 8 9 xchnxbir 
 |-  ( -. Z e. Even <-> ( -. Z e. ZZ \/ -. ( Z / 2 ) e. ZZ ) )
11 7 10 sylibr 
 |-  ( Z e. Odd -> -. Z e. Even )