let x1, h be Nat; ( 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
; 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).]
;
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;
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 )
; verum