let x1, h be Nat; :: thesis: ( 1 < h implies ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h ) )
assume A1: 1 < h ; :: thesis: ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h )
reconsider h1 = h as Real ;
consider q1, r1 being Integer such that
A2: x1 = (h * q1) + r1 and
A3: 0 <= r1 and
A4: r1 < h by INT_4:13, A1;
A5: r1 in [.0,h1.[ by A3, A4, XXREAL_1:3;
h1 / 2 < h1 by A1, XREAL_1:216;
then A7: [.0,h1.[ = [.0,(h1 / 2).] \/ ].(h1 / 2),h1.[ by XXREAL_1:169;
ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h )
proof
per cases ( r1 in [.0,(h1 / 2).] or r1 in ].(h1 / 2),h1.[ ) by A5, A7, XBOOLE_0:def 3;
suppose A9: r1 in [.0,(h1 / 2).] ; :: thesis: ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h )
then A10: ( 0 <= r1 & r1 <= h1 / 2 ) by XXREAL_1:1;
( r1 <= h1 / 2 & 0 <= 2 ) by A9, XXREAL_1:1;
then A12: 2 * r1 <= 2 * (h1 / 2) by XREAL_1:64;
A13: r1 in NAT by A10, INT_1:3;
consider y1 being Integer such that
A14: y1 = r1 ;
A15: ( 0 <= y1 & 2 * y1 <= h1 ) by A9, A12, A14, XXREAL_1:1;
h divides x1 - y1 by A2, A14, INT_1:def 3;
then A17: x1 mod h = y1 mod h by A1, A13, A14, INT_4:23;
(x1 ^2) mod h = ((x1 mod h) * (x1 mod h)) mod h by NAT_D:67
.= (y1 ^2) mod h by NAT_D:67, A17 ;
hence ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h ) by A1, A15, A17; :: thesis: verum
end;
suppose A19: r1 in ].(h1 / 2),h1.[ ; :: thesis: ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h )
then A20: ( h1 / 2 < r1 & r1 < h1 ) by XXREAL_1:4;
r1 > 0 by A19, XXREAL_1:4;
then A22: r1 in NAT by INT_1:3;
set y1 = r1 - h;
h divides x1 - ((r1 - h) + h) by A2, INT_1:def 3;
then A24: x1 mod h = ((r1 - h) + h) mod h by A1, A22, INT_4:23
.= (((r1 - h) mod h) + (h mod h)) mod h by NAT_D:66
.= (((r1 - h) mod h) + 0) mod h by NAT_D:25
.= (r1 - h) mod h by NAT_D:65 ;
A25: (x1 ^2) mod h = ((x1 mod h) * (x1 mod h)) mod h by NAT_D:67
.= ((r1 - h) ^2) mod h by NAT_D:67, A24 ;
A26: (h1 / 2) - h < r1 - h by A20, XREAL_1:9;
r1 - h < h1 - h by A20, XREAL_1:9;
then ( 2 * (- (h1 / 2)) < 2 * (r1 - h) & 2 * (r1 - h) <= 2 * (h1 / 2) ) by A26, XREAL_1:68;
hence ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h ) by A24, A25; :: thesis: verum
end;
end;
end;
hence ex y1 being Integer st
( x1 mod h = y1 mod h & - h < 2 * y1 & 2 * y1 <= h & (x1 ^2) mod h = (y1 ^2) mod h ) ; :: thesis: verum