Metamath Proof Explorer


Theorem n2dvdsm1

Description: 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021)

Ref Expression
Assertion n2dvdsm1 ¬ 2 ∥ - 1

Proof

Step Hyp Ref Expression
1 z0even 2 ∥ 0
2 ax-1cn 1 ∈ ℂ
3 neg1cn - 1 ∈ ℂ
4 1pneg1e0 ( 1 + - 1 ) = 0
5 2 3 4 addcomli ( - 1 + 1 ) = 0
6 1 5 breqtrri 2 ∥ ( - 1 + 1 )
7 neg1z - 1 ∈ ℤ
8 oddp1even ( - 1 ∈ ℤ → ( ¬ 2 ∥ - 1 ↔ 2 ∥ ( - 1 + 1 ) ) )
9 7 8 ax-mp ( ¬ 2 ∥ - 1 ↔ 2 ∥ ( - 1 + 1 ) )
10 6 9 mpbir ¬ 2 ∥ - 1