let a be Integer; :: thesis: for b being odd Integer st not b divides a holds
( a mod b is odd iff (- a) mod b is even )
let b be odd Integer; :: thesis: ( not b divides a implies ( a mod b is odd iff (- a) mod b is even ) )
assume A1: not b divides a ; :: thesis: ( a mod b is odd iff (- a) mod b is even )
(a mod b) + ((- a) mod b) is odd by A1, MOD;
hence ( a mod b is odd iff (- a) mod b is even ) ; :: thesis: verum