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 || -u 1

Proof

Step Hyp Ref Expression
1 z0even 
 |-  2 || 0
2 ax-1cn 
 |-  1 e. CC
3 neg1cn 
 |-  -u 1 e. CC
4 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
5 2 3 4 addcomli 
 |-  ( -u 1 + 1 ) = 0
6 1 5 breqtrri 
 |-  2 || ( -u 1 + 1 )
7 neg1z 
 |-  -u 1 e. ZZ
8 oddp1even 
 |-  ( -u 1 e. ZZ -> ( -. 2 || -u 1 <-> 2 || ( -u 1 + 1 ) ) )
9 7 8 ax-mp 
 |-  ( -. 2 || -u 1 <-> 2 || ( -u 1 + 1 ) )
10 6 9 mpbir 
 |-  -. 2 || -u 1