Metamath Proof Explorer


Theorem isodd3

Description: The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion isodd3 ZOddZ¬2Z

Proof

Step Hyp Ref Expression
1 breq2 z=Z2z2Z
2 1 notbid z=Z¬2z¬2Z
3 dfodd3 Odd=z|¬2z
4 2 3 elrab2 ZOddZ¬2Z