let a be Integer; :: thesis: for b being non zero Integer holds (a |^ 2) mod b = ((b - a) |^ 2) mod b
let b be non zero Integer; :: thesis: (a |^ 2) mod b = ((b - a) |^ 2) mod b
reconsider x = - a as Integer ;
((b - a) |^ 2) mod b = (((x + (1 * b)) mod b) |^ 2) mod b by GRCY330
.= ((x mod b) |^ 2) mod b by NAT_D:61
.= ((- a) |^ (2 * 1)) mod b by GRCY330
.= (a |^ 2) mod b by POWER:1 ;
hence (a |^ 2) mod b = ((b - a) |^ 2) mod b ; :: thesis: verum