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 20
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-12-1+1
9 7 8 ax-mp ¬2-12-1+1
10 6 9 mpbir ¬2-1