let a be Nat; for k being Integer st a <> 0 & a gcd k = 1 holds
ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
let k be Integer; ( a <> 0 & a gcd k = 1 implies ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) )
assume that
A1:
a <> 0
and
A2:
a gcd k = 1
; ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
A3:
a >= 1
by A1, NAT_1:14;
per cases
( a = 1 or a > 1 )
by A3, XXREAL_0:1;
suppose A5:
a > 1
;
ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )A6:
sqrt a > 0
by A1, SQUARE_1:25;
set d =
[\(sqrt a)/];
A7:
[\(sqrt a)/] <= sqrt a
by INT_1:def 6;
sqrt a < a
by A5, Lm21;
then A8:
[\(sqrt a)/] < a
by A7, XXREAL_0:2;
set d1 =
[\(sqrt a)/] + 1;
A9:
[\(sqrt a)/] > (sqrt a) - 1
by INT_1:def 6;
sqrt a > 1
by A5, SQUARE_1:18, SQUARE_1:27;
then A10:
(sqrt a) - 1
> 0
by XREAL_1:50;
then reconsider d =
[\(sqrt a)/] as
Element of
NAT by A9, INT_1:3;
A11:
d + 1
>= 1
by Lm1;
then reconsider d1 =
[\(sqrt a)/] + 1 as
Element of
NAT ;
set e1 =
d1 ^2 ;
d1 ^2 = d1 * d1
;
then reconsider e1 =
d1 ^2 as
Element of
NAT ;
A12:
(e1 - 1) / d1 = d1 - (1 / d1)
by A11, XCMPLX_1:127;
deffunc H1(
Nat)
-> set = 1
+ (((k * (($1 - 1) div d1)) + (($1 - 1) mod d1)) mod a);
consider fs being
FinSequence such that A13:
(
len fs = e1 & ( for
b being
Nat st
b in dom fs holds
fs . b = H1(
b) ) )
from FINSEQ_1:sch 2();
A14:
rng fs c= Seg a
sqrt a < d1
by A9, XREAL_1:19;
then
(sqrt a) ^2 < e1
by A6, SQUARE_1:16;
then A19:
a < e1
by SQUARE_1:def 2;
then A20:
Seg a c= Seg e1
by FINSEQ_1:5;
A21:
Seg e1 = dom fs
by A13, FINSEQ_1:def 3;
then
rng fs <> dom fs
by A19, A14, FINSEQ_1:5;
then
not
fs is
one-to-one
by A21, A14, A20, FINSEQ_4:59, XBOOLE_1:1;
then consider v1,
v2 being
object such that A22:
v1 in dom fs
and A23:
v2 in dom fs
and A24:
fs . v1 = fs . v2
and A25:
v1 <> v2
by FUNCT_1:def 4;
reconsider v1 =
v1,
v2 =
v2 as
Element of
NAT by A22, A23;
set x1 =
(v1 - 1) div d1;
set x2 =
(v2 - 1) div d1;
set x =
((v1 - 1) div d1) - ((v2 - 1) div d1);
set y1 =
(v1 - 1) mod d1;
set y2 =
(v2 - 1) mod d1;
set y =
((v1 - 1) mod d1) - ((v2 - 1) mod d1);
A26:
(v1 - 1) mod d1 >= 0
by NEWTON:64;
(
fs . v1 = 1
+ (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod a) &
fs . v2 = 1
+ (((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod a) )
by A13, A22, A23;
then A27:
(((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))) mod a = 0
by A24, Lm19, XCMPLX_1:2;
then A28:
a divides ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))
by A1, Lm20;
1
/ d1 > 0
by A9, A10, XREAL_1:139;
then A29:
(e1 - 1) / d1 < d1
by A12, Lm1;
A30:
(v2 - 1) div d1 = [\((v2 - 1) / d1)/]
by INT_1:def 9;
then A31:
(v2 - 1) div d1 <= (v2 - 1) / d1
by INT_1:def 6;
v2 <= e1
by A13, A23, FINSEQ_3:25;
then
v2 - 1
<= e1 - 1
by XREAL_1:9;
then
(v2 - 1) / d1 <= (e1 - 1) / d1
by XREAL_1:72;
then
(v2 - 1) / d1 < d1
by A29, XXREAL_0:2;
then
(v2 - 1) div d1 < d1
by A31, XXREAL_0:2;
then A32:
(v2 - 1) div d1 <= d
by Lm9;
set d2 =
(k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1));
A33:
[\0/] = 0
by INT_1:25;
A34:
(v1 - 1) div d1 = [\((v1 - 1) / d1)/]
by INT_1:def 9;
then A35:
(v1 - 1) div d1 <= (v1 - 1) / d1
by INT_1:def 6;
1
<= v1
by A22, FINSEQ_3:25;
then
v1 - 1
>= 0
by XREAL_1:48;
then
(v1 - 1) div d1 >= 0
by A34, A33, PRE_FF:9;
then
((v2 - 1) div d1) - ((v1 - 1) div d1) <= d
by A32, Lm2;
then A36:
- (((v2 - 1) div d1) - ((v1 - 1) div d1)) >= - d
by XREAL_1:24;
A37:
(
((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 or
((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 )
v1 <= e1
by A13, A22, FINSEQ_3:25;
then
v1 - 1
<= e1 - 1
by XREAL_1:9;
then
(v1 - 1) / d1 <= (e1 - 1) / d1
by XREAL_1:72;
then
(v1 - 1) / d1 < d1
by A29, XXREAL_0:2;
then
(v1 - 1) div d1 < d1
by A35, XXREAL_0:2;
then A38:
(v1 - 1) div d1 <= d
by Lm9;
A39:
((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))
;
(v2 - 1) mod d1 < d1
by A9, A10, NEWTON:65;
then
((v2 - 1) mod d1) - ((v1 - 1) mod d1) < d1
by A26, Lm3;
then
((v2 - 1) mod d1) - ((v1 - 1) mod d1) <= d
by Lm9;
then A40:
- (((v2 - 1) mod d1) - ((v1 - 1) mod d1)) >= - d
by XREAL_1:24;
take b =
|.(((v1 - 1) div d1) - ((v2 - 1) div d1)).|;
ex e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )take e =
|.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).|;
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )A41:
(v2 - 1) mod d1 >= 0
by NEWTON:64;
1
<= v2
by A23, FINSEQ_3:25;
then
v2 - 1
>= 0
by XREAL_1:48;
then
(v2 - 1) div d1 >= 0
by A30, A33, PRE_FF:9;
then
((v1 - 1) div d1) - ((v2 - 1) div d1) <= d
by A38, Lm2;
then A42:
|.(((v1 - 1) div d1) - ((v2 - 1) div d1)).| <= d
by A36, ABSVALUE:5;
then A43:
|.(((v1 - 1) div d1) - ((v2 - 1) div d1)).| < a
by A8, XXREAL_0:2;
(v1 - 1) mod d1 < d1
by A9, A10, NEWTON:65;
then
((v1 - 1) mod d1) - ((v2 - 1) mod d1) < d1
by A41, Lm3;
then
((v1 - 1) mod d1) - ((v2 - 1) mod d1) <= d
by Lm9;
then A46:
|.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).| <= d
by A40, ABSVALUE:5;
then A47:
|.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).| < a
by A8, XXREAL_0:2;
hence
(
b <> 0 &
e <> 0 )
by A44, ABSVALUE:2;
( b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )thus
b <= sqrt a
by A7, A42, XXREAL_0:2;
( e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )thus
e <= sqrt a
by A7, A46, XXREAL_0:2;
( a divides (k * b) + e or a divides (k * b) - e )A49:
(
b = ((v1 - 1) div d1) - ((v2 - 1) div d1) or
b = - (((v1 - 1) div d1) - ((v2 - 1) div d1)) )
by ABSVALUE:1;
A50:
(
e = ((v1 - 1) mod d1) - ((v2 - 1) mod d1) or
e = - (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) )
by ABSVALUE:1;
- ((k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) = (k * (- (((v1 - 1) div d1) - ((v2 - 1) div d1)))) + (- (((v1 - 1) mod d1) - ((v2 - 1) mod d1)))
;
hence
(
a divides (k * b) + e or
a divides (k * b) - e )
by A28, A49, A50, INT_2:10;
verum end; end;