Metamath Proof Explorer


Theorem n2dvds1

Description: 2 does not divide 1. That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018) (Proof shortened by Steven Nguyen, 3-May-2023)

Ref Expression
Assertion n2dvds1
|- -. 2 || 1

Proof

Step Hyp Ref Expression
1 halfnz
 |-  -. ( 1 / 2 ) e. ZZ
2 1z
 |-  1 e. ZZ
3 evend2
 |-  ( 1 e. ZZ -> ( 2 || 1 <-> ( 1 / 2 ) e. ZZ ) )
4 2 3 ax-mp
 |-  ( 2 || 1 <-> ( 1 / 2 ) e. ZZ )
5 1 4 mtbir
 |-  -. 2 || 1