let a be non trivial Nat; :: thesis: for y, n, b, c, d, r, s, t, u, v, x being Nat st 1 <= n & [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [s,t] is Pell's_solution of (b ^2) -' 1 & v = (4 * r) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & s = x + (c * u) & t = n + ((4 * d) * y) & n <= y holds
( not b is trivial & u ^2 > a & y = Py (a,n) )

let y, n, b, c, d, r, s, t, u, v, x be Nat; :: thesis: ( 1 <= n & [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [s,t] is Pell's_solution of (b ^2) -' 1 & v = (4 * r) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & s = x + (c * u) & t = n + ((4 * d) * y) & n <= y implies ( not b is trivial & u ^2 > a & y = Py (a,n) ) )
assume that
A1: 1 <= n and
A2: [x,y] is Pell's_solution of (a ^2) -' 1 and
A3: [u,v] is Pell's_solution of (a ^2) -' 1 and
A4: [s,t] is Pell's_solution of (b ^2) -' 1 and
A5: v = (4 * r) * (y ^2) and
A6: b = a + ((u ^2) * ((u ^2) - a)) and
A7: s = x + (c * u) and
A8: t = n + ((4 * d) * y) and
A9: n <= y ; :: thesis: ( not b is trivial & u ^2 > a & y = Py (a,n) )
A10: (s ^2) - (((b ^2) -' 1) * (t ^2)) = 1 by ;
consider i being Nat such that
A11: ( x = Px (a,i) & y = Py (a,i) ) by ;
A12: ((Px (a,i)) ^2) - (((a ^2) -' 1) * ((Py (a,i)) ^2)) = 1 by HILB10_1:7;
consider n1 being Nat such that
A13: ( u = Px (a,n1) & v = Py (a,n1) ) by ;
A14: ((Px (a,n1)) ^2) - (((a ^2) -' 1) * ((Py (a,n1)) ^2)) = 1 by HILB10_1:7;
then (Px (a,n1)) ^2 = (((a ^2) -' 1) * ((Py (a,n1)) ^2)) + 1 ;
then A15: u ^2 = (((a ^2) -' 1) * (v ^2)) + 1 by A13;
A16: ( Px (a,0) = 1 & Py (a,0) = 0 ) by HILB10_1:3;
then A17: ( Px (a,(0 + 1)) = (1 * a) + (0 * ((a ^2) -' 1)) & Py (a,(0 + 1)) = 1 + (0 * a) ) by HILB10_1:6;
A18: ( (Px (a,n1)) ^2 = (Px (a,n1)) * (Px (a,n1)) & (Py (a,n1)) ^2 = (Py (a,n1)) * (Py (a,n1)) ) by SQUARE_1:def 1;
A19: ( (Px (a,i)) ^2 = (Px (a,i)) * (Px (a,i)) & (Py (a,i)) ^2 = (Py (a,i)) * (Py (a,i)) ) by SQUARE_1:def 1;
A20: v <> 0
proof
assume A21: v = 0 ; :: thesis: contradiction
then A22: u = 1 by ;
A23: u ^2 = 1 * 1 by A21, A18, A13, A14;
b ^2 = b * b by SQUARE_1:def 1;
then (b ^2) -' 1 = 0 by ;
then s * s = 1 by ;
then 1 = x + (c * 1) by ;
then x = 1 by ;
then y * y = 0 by ;
hence contradiction by A9, A1; :: thesis: verum
end;
then n1 <> 0 by ;
then n1 >= 1 + 0 by NAT_1:13;
then A24: a <= u by ;
u > 1 by ;
then A25: ( a * 1 < u * u & u ^2 = u * u ) by ;
then A26: ( (u ^2) - a > 0 & u ^2 > 0 ) by XREAL_1:50;
then reconsider B = b as non trivial Nat by A6;
consider j being Nat such that
A27: ( s = Px (B,j) & t = Py (B,j) ) by ;
r > 0 by ;
then A28: r >= 0 + 1 by NAT_1:13;
y >= 1 by ;
then y * y >= y * 1 by XREAL_1:66;
then r * (y * y) >= y * 1 by ;
then A29: 4 * (r * (y * y)) >= y * 1 by XREAL_1:66;
u ^2 = u * u by SQUARE_1:def 1;
then b - a = u * (u * ((u ^2) - a)) by A6;
then A30: Px (B,j), Px (a,j) are_congruent_mod Px (a,n1) by ;
A31: i > 0 by A9, A1, A16, A11;
x - s = u * (- c) by A7;
then Px (a,i), Px (B,j) are_congruent_mod Px (a,n1) by ;
then Px (a,i), Px (a,j) are_congruent_mod Px (a,n1) by ;
then A32: ( j,i are_congruent_mod 4 * n1 or j, - i are_congruent_mod 4 * n1 ) by ;
(Py (a,i)) ^2 divides Py (a,n1) by ;
then consider divN being Nat such that
A33: (Py (a,i)) * divN = n1 by ;
4 * n1 = (4 * (Py (a,i))) * divN by A33;
then A34: ( j,i are_congruent_mod 4 * (Py (a,i)) or j, - i are_congruent_mod 4 * (Py (a,i)) ) by ;
b - 1 = (4 * y) * (((((a ^2) -' 1) * ((4 * r) * (y ^2))) * (r * y)) * (((((a ^2) -' 1) * (((4 * r) * (y ^2)) ^2)) + 2) - a)) by A6, A15, A5, A11, A13, A18, A19;
then A35: Py (B,j),j are_congruent_mod 4 * (Py (a,i)) by ;
(Py (B,j)) - n = (4 * (Py (a,i))) * d by A11, A27, A8;
then n, Py (B,j) are_congruent_mod 4 * (Py (a,i)) by ;
then n,j are_congruent_mod 4 * (Py (a,i)) by ;
then A36: ( n,i are_congruent_mod 4 * (Py (a,i)) or n, - i are_congruent_mod 4 * (Py (a,i)) ) by ;
A37: 1 * (Py (a,i)) < 4 * (Py (a,i)) by ;
A38: n < 4 * (Py (a,i)) by ;
A39: i <= Py (a,i) by HILB10_1:13;
then reconsider Pi = (4 * (Py (a,i))) - i as Nat by ;
A40: i < 4 * (Py (a,i)) by ;
A41: (4 * (Py (a,i))) + (- i) < (4 * (Py (a,i))) + 0 by ;
n = i
proof
assume n <> i ; :: thesis: contradiction
then - i,n are_congruent_mod 4 * (Py (a,i)) by ;
then A42: Pi = n by ;
A43: (4 * (Py (a,i))) - i >= (4 * (Py (a,i))) - (Py (a,i)) by ;
((Py (a,i)) + (Py (a,i))) + (Py (a,i)) > (Py (a,i)) + 0 by ;
hence contradiction by A42, A11, A9, A43, XXREAL_0:2; :: thesis: verum
end;
hence ( not b is trivial & u ^2 > a & y = Py (a,n) ) by A26, A6, A25, A11; :: thesis: verum