Metamath Proof Explorer


Theorem n2dvds3

Description: 2 does not divide 3. That means 3 is odd. (Contributed by AV, 28-Feb-2021) (Proof shortened by Steven Nguyen, 3-May-2023)

Ref Expression
Assertion n2dvds3 ¬ 2 ∥ 3

Proof

Step Hyp Ref Expression
1 3halfnz ¬ ( 3 / 2 ) ∈ ℤ
2 3z 3 ∈ ℤ
3 evend2 ( 3 ∈ ℤ → ( 2 ∥ 3 ↔ ( 3 / 2 ) ∈ ℤ ) )
4 2 3 ax-mp ( 2 ∥ 3 ↔ ( 3 / 2 ) ∈ ℤ )
5 1 4 mtbir ¬ 2 ∥ 3