let x1, h be Nat; :: thesis: for y1 being Integer st 1 < h & x1 mod h = y1 mod h & - h < 2 * y1 & (2 * y1) ^2 = h ^2 holds
( 2 * y1 = h & ex m1 being Nat st 2 * x1 = ((2 * m1) + 1) * h )
let y1 be Integer; :: thesis: ( 1 < h & x1 mod h = y1 mod h & - h < 2 * y1 & (2 * y1) ^2 = h ^2 implies ( 2 * y1 = h & ex m1 being Nat st 2 * x1 = ((2 * m1) + 1) * h ) )
assume that
A1: 1 < h and
A2: x1 mod h = y1 mod h and
A3: - h < 2 * y1 and
A4: (2 * y1) ^2 = h ^2 ; :: thesis: ( 2 * y1 = h & ex m1 being Nat st 2 * x1 = ((2 * m1) + 1) * h )
A7: 2 * y1 = h by A3, A4, SQUARE_1:40;
reconsider h = h as Integer ;
set h1 = h;
y1 > 0 by A1, A3, A4, SQUARE_1:40;
then y1 in NAT by INT_1:3;
then h divides x1 - y1 by A1, A2, INT_4:23;
then consider m1 being Integer such that
A9: x1 - y1 = h * m1 by INT_1:def 3;
A10: x1 = (((2 * m1) + 1) * h) / 2 by A7, A9;
A12: (((2 * m1) + 1) * (h / 2)) * ((h / 2) ") >= 0 * ((h / 2) ") by A7, A9;
(h / 2) * ((h / 2) ") = 1 by A1, XCMPLX_0:def 7;
then (2 * m1) + 1 = ((2 * m1) + 1) * ((h / 2) * ((h / 2) ")) ;
then ((2 * m1) + 1) + (- 1) >= 0 + (- 1) by A12, XREAL_1:6;
then (2 * m1) * (2 ") >= (- 1) * (2 ") by XREAL_1:64;
then m1 > - 1 by XXREAL_0:2;
then m1 >= (- 1) + 1 by INT_1:7;
then m1 in NAT by INT_1:3;
hence ( 2 * y1 = h & ex m1 being Nat st 2 * x1 = ((2 * m1) + 1) * h ) by A3, A4, A10, SQUARE_1:40; :: thesis: verum