let a be non trivial Nat; :: thesis: for s, n, r being Nat st s > 0 & r > 0 & (((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 & s * (((s |^ n) ^2) * (s |^ n)) < a & s * ((r ^2) * r) < a holds
r = s |^ n
let s, n, r be Nat; :: thesis: ( s > 0 & r > 0 & (((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 & s * (((s |^ n) ^2) * (s |^ n)) < a & s * ((r ^2) * r) < a implies r = s |^ n )
assume that
A1: ( s > 0 & r > 0 ) and
A2: ( (((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 & s * (((s |^ n) ^2) * (s |^ n)) < a & s * ((r ^2) * r) < a ) ; :: thesis: r = s |^ n
set 2sa = (((2 * a) * s) - (s ^2)) - 1;
set P = Py (a,(n + 1));
A3: r,r are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
(((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by Th12;
then A4: ((((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1) * r,0 * r are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A3, INT_1:18;
A5: ( r ^2 = r * r & (s |^ n) ^2 = (s |^ n) * (s |^ n) ) by SQUARE_1:def 1;
A6: (((((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1) * (s |^ n)) - (((((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1) * r) = (r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1) by A5;
s |^ n,s |^ n are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
then ((((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1) * (s |^ n),0 * (s |^ n) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A2, INT_1:18;
then A7: (r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1),0 - 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A6, A4, INT_1:17;
set q = max (r,(s |^ n));
A8: r >= 1 + 0 by A1, NAT_1:13;
A9: s |^ n >= 0 + 1 by A1, NAT_1:13;
A10: |.(r - (s |^ n)).| <= (max (r,(s |^ n))) - 1

proof

per cases ( r - (s |^ n) >= 0 or r - (s |^ n) < 0 ) ;

suppose r - (s |^ n) >= 0 ; :: thesis: |.(r - (s |^ n)).| <= (max (r,(s |^ n))) - 1

then ( |.(r - (s |^ n)).| = r - (s |^ n) & r - (s |^ n) <= r - 1 ) by ABSVALUE:def 1, A9, XREAL_1:10;
hence |.(r - (s |^ n)).| <= (max (r,(s |^ n))) - 1 by XXREAL_0:def 10, XREAL_1:49; :: thesis: verum

end;

suppose A12: r - (s |^ n) < 0 ; :: thesis: |.(r - (s |^ n)).| <= (max (r,(s |^ n))) - 1

then |.(r - (s |^ n)).| = - (r - (s |^ n)) by ABSVALUE:def 1;
then ( |.(r - (s |^ n)).| = (s |^ n) - r & (s |^ n) - r <= (s |^ n) - 1 ) by A8, XREAL_1:10;
hence |.(r - (s |^ n)).| <= (max (r,(s |^ n))) - 1 by A12, XXREAL_0:def 10, XREAL_1:48; :: thesis: verum

end;

end;

end;

|.((((s ^2) * r) * (s |^ n)) + 1).| = (((s ^2) * r) * (s |^ n)) + 1 ;
then |.((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)).| = |.(r - (s |^ n)).| * ((((s ^2) * r) * (s |^ n)) + 1) by COMPLEX1:65;
then |.((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)).| <= ((max (r,(s |^ n))) - 1) * ((((s ^2) * r) * (s |^ n)) + 1) by A10, XREAL_1:64;
then A13: |.((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)).| + ((s ^2) + 1) <= (((max (r,(s |^ n))) - 1) * ((((s ^2) * r) * (s |^ n)) + 1)) + ((s ^2) + 1) by XREAL_1:7;
(s |^ n) * r >= 1 * 1 by A1, NAT_1:13, A9;
then ((s |^ n) * r) * (s ^2) >= 1 * (s ^2) by XREAL_1:64;
then A14: (s ^2) - (((s ^2) * r) * (s |^ n)) <= 0 by XREAL_1:47;
A15: ( s ^2 = s * s & r ^2 = r * r ) by SQUARE_1:def 1;
then (((s ^2) * r) * (s |^ n)) * (max (r,(s |^ n))) >= 1 * (max (r,(s |^ n))) by A1, NAT_1:14, XREAL_1:64;
then (max (r,(s |^ n))) + ((s ^2) - (((s ^2) * r) * (s |^ n))) <= ((((s ^2) * r) * (s |^ n)) * (max (r,(s |^ n)))) + 0 by A14, XREAL_1:7;
then ((((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n)) + (((max (r,(s |^ n))) + (s ^2)) - (((s ^2) * r) * (s |^ n))) <= ((((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n)) + ((((s ^2) * r) * (s |^ n)) * (max (r,(s |^ n)))) by XREAL_1:7;
then A16: |.((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)).| + ((s ^2) + 1) <= (((2 * (max (r,(s |^ n)))) * (s ^2)) * r) * (s |^ n) by A13, XXREAL_0:2;
consider I being Integer such that
A17: ((((2 * a) * s) - (s ^2)) - 1) * I = ((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)) - 0 by A7, INT_1:def 5;
(((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) < a * s

proof

A18: (s * (((s |^ n) ^2) * (s |^ n))) * s < a * s by XREAL_1:68, A1, A2;

per cases ( r <= s |^ n or r > s |^ n ) ;

suppose A19: r <= s |^ n ; :: thesis: (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) < a * s

then max (r,(s |^ n)) = s |^ n by XXREAL_0:def 10;
then (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) = (((s |^ n) * (s ^2)) * (s |^ n)) * r ;
then ( (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) <= (((s |^ n) * (s ^2)) * (s |^ n)) * (s |^ n) & (s |^ n) ^2 = (s |^ n) * (s |^ n) ) by A19, XREAL_1:64, SQUARE_1:def 1;
hence (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) < a * s by A15, A18, XXREAL_0:2; :: thesis: verum

end;

suppose A20: r > s |^ n ; :: thesis: (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) < a * s

then A21: max (r,(s |^ n)) = r by XXREAL_0:def 10;
then ( (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) = (((max (r,(s |^ n))) * (s ^2)) * (max (r,(s |^ n)))) * (s |^ n) & (((max (r,(s |^ n))) * (s ^2)) * (max (r,(s |^ n)))) * (s |^ n) <= (((max (r,(s |^ n))) * (s ^2)) * (max (r,(s |^ n)))) * (max (r,(s |^ n))) ) by A20, XREAL_1:64;
then ( (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) <= (s * ((r ^2) * r)) * s & (s * ((r ^2) * r)) * s < a * s ) by A1, A2, A21, A15, XREAL_1:68;
hence (((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n) < a * s by XXREAL_0:2; :: thesis: verum

end;

end;

end;

then ((((max (r,(s |^ n))) * (s ^2)) * r) * (s |^ n)) * 2 < (a * s) * 2 by XREAL_1:68;
then |.((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)).| + ((s ^2) + 1) < (a * s) * 2 by A16, XXREAL_0:2;
then |.((r - (s |^ n)) * ((((s ^2) * r) * (s |^ n)) + 1)).| < ((a * s) * 2) - ((s ^2) + 1) by XREAL_1:20;
then |.((((2 * a) * s) - (s ^2)) - 1).| * |.I.| < (((2 * a) * s) - (s ^2)) - 1 by A17, COMPLEX1:65;
then |.((((2 * a) * s) - (s ^2)) - 1).| * |.I.| < |.((((2 * a) * s) - (s ^2)) - 1).| * 1 by ABSVALUE:def 1;
then |.I.| < 1 + 0 by XREAL_1:66;
then I = 0 by INT_1:7;
then r - (s |^ n) = 0 by A17;
hence r = s |^ n ; :: thesis: verum