let a be non trivial Nat; :: thesis: for y, n being Nat st y > 0 & n > 0 & (((a ^2) - 1) * (y ^2)) + 1 is square & y,n are_congruent_mod a - 1 & y <= Py (a,(a - 1)) & n <= a - 1 holds
y = Py (a,n)
let y, n be Nat; :: thesis: ( y > 0 & n > 0 & (((a ^2) - 1) * (y ^2)) + 1 is square & y,n are_congruent_mod a - 1 & y <= Py (a,(a - 1)) & n <= a - 1 implies y = Py (a,n) )
assume that
A1: ( y > 0 & n > 0 ) and
A2: (((a ^2) - 1) * (y ^2)) + 1 is square and
A3: y,n are_congruent_mod a - 1 and
A4: y <= Py (a,(a - 1)) and
A5: n <= a - 1 ; :: thesis: y = Py (a,n)
a * a = a ^2 by SQUARE_1:def 1;
then a ^2 >= 1 + 0 by NAT_1:13;
then A6: (a ^2) -' 1 = (a ^2) - 1 by XREAL_1:233;
consider x being Nat such that
A7: (((a ^2) - 1) * (y ^2)) + 1 = x ^2 by A2, PYTHTRIP:def 3;
(x ^2) - (((a ^2) -' 1) * (y ^2)) = 1 by A7, A6;
then [x,y] is Pell's_solution of (a ^2) -' 1 by Lm1;
then consider n1 being Nat such that
A8: ( x = Px (a,n1) & y = Py (a,n1) ) by HILB10_1:4;
A9: n1 <= a - 1 by A4, A8, HILB10_1:11;
n1,y are_congruent_mod a - 1 by INT_1:14, A8, HILB10_1:24;
then consider i being Integer such that
A10: (a - 1) * i = n1 - n by INT_1:def 5, A3, INT_1:15;
n1 <> 0 by A8, A1, HILB10_1:3;
then ( 0 - (a - 1) < n1 - n & n1 - n < (a - 1) - 0 ) by A1, A5, A9, XREAL_1:15, XREAL_1:14;
then ( (- 1) * (a - 1) < i * (a - 1) & i * (a - 1) < 1 * (a - 1) ) by A10;
then ( - 1 < i & i < 1 + 0 ) by XREAL_1:64;
then ( (- 1) + 1 <= i & i <= 0 ) by INT_1:7;
then i = 0 ;
hence y = Py (a,n) by A10, A8; :: thesis: verum