Metamath Proof Explorer

Theorem zeoALTV

Description: An integer is even or odd. (Contributed by NM, 1-Jan-2006) (Revised by AV, 16-Jun-2020)

Ref Expression
Assertion zeoALTV 
|- ( Z e. ZZ -> ( Z e. Even \/ Z e. Odd ) )

Proof

Step Hyp Ref Expression
1 zeo 
 |-  ( Z e. ZZ -> ( ( Z / 2 ) e. ZZ \/ ( ( Z + 1 ) / 2 ) e. ZZ ) )
2 1 ancli 
 |-  ( Z e. ZZ -> ( Z e. ZZ /\ ( ( Z / 2 ) e. ZZ \/ ( ( Z + 1 ) / 2 ) e. ZZ ) ) )
3 andi 
 |-  ( ( Z e. ZZ /\ ( ( Z / 2 ) e. ZZ \/ ( ( Z + 1 ) / 2 ) e. ZZ ) ) <-> ( ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) \/ ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) ) )
4 2 3 sylib 
 |-  ( Z e. ZZ -> ( ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) \/ ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) ) )
5 iseven 
 |-  ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
6 isodd 
 |-  ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
7 5 6 orbi12i 
 |-  ( ( Z e. Even \/ Z e. Odd ) <-> ( ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) \/ ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) ) )
8 4 7 sylibr 
 |-  ( Z e. ZZ -> ( Z e. Even \/ Z e. Odd ) )