Metamath Proof Explorer

Theorem zeo2ALTV

Description: An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015) (Revised by AV, 16-Jun-2020)

Ref Expression
Assertion zeo2ALTV 
|- ( Z e. ZZ -> ( Z e. Even <-> -. Z e. Odd ) )

Proof

Step Hyp Ref Expression
1 evennodd 
 |-  ( Z e. Even -> -. Z e. Odd )
2 zeoALTV 
 |-  ( Z e. ZZ -> ( Z e. Even \/ Z e. Odd ) )
3 ax-1 
 |-  ( Z e. Even -> ( -. Z e. Odd -> Z e. Even ) )
4 pm2.24 
 |-  ( Z e. Odd -> ( -. Z e. Odd -> Z e. Even ) )
5 3 4 jaoi 
 |-  ( ( Z e. Even \/ Z e. Odd ) -> ( -. Z e. Odd -> Z e. Even ) )
6 2 5 syl 
 |-  ( Z e. ZZ -> ( -. Z e. Odd -> Z e. Even ) )
7 1 6 impbid2 
 |-  ( Z e. ZZ -> ( Z e. Even <-> -. Z e. Odd ) )