Metamath Proof Explorer

Theorem 2ndvdsodd

Description: 2 does not divide an odd number. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion 2ndvdsodd 
|- ( Z e. Odd -> -. 2 || Z )

Proof

Step Hyp Ref Expression
1 isodd3 
 |-  ( Z e. Odd <-> ( Z e. ZZ /\ -. 2 || Z ) )
2 1 simprbi 
 |-  ( Z e. Odd -> -. 2 || Z )