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 Lm1, A4;

consider i being Nat such that

A11: ( x = Px (a,i) & y = Py (a,i) ) by A2, HILB10_1:4;

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 A3, HILB10_1:4;

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

then n1 >= 1 + 0 by NAT_1:13;

then A24: a <= u by A13, A17, HILB10_1:10;

u > 1 by NEWTON03:def 1, A24, XXREAL_0:2;

then A25: ( a * 1 < u * u & u ^2 = u * u ) by A24, XREAL_1:97, SQUARE_1:def 1;

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 A4, HILB10_1:4;

r > 0 by A5, A20;

then A28: r >= 0 + 1 by NAT_1:13;

y >= 1 by A9, A1, XXREAL_0:2;

then y * y >= y * 1 by XREAL_1:66;

then r * (y * y) >= y * 1 by A28, XREAL_1:66;

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 Th16, A13, INT_1:def 5;

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 A11, A13, A27, INT_1:def 5;

then Px (a,i), Px (a,j) are_congruent_mod Px (a,n1) by A30, INT_1:15;

then A32: ( j,i are_congruent_mod 4 * n1 or j, - i are_congruent_mod 4 * n1 ) by A31, A29, A5, HILB10_1:11, A13, Th24, A11, A19;

(Py (a,i)) ^2 divides Py (a,n1) by A5, A11, A13, INT_1:def 3;

then consider divN being Nat such that

A33: (Py (a,i)) * divN = n1 by NAT_D:def 3, HILB10_1:37;

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 A32, INT_1:20;

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 HILB10_1:24, A11, INT_1:20;

(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 INT_1:14, INT_1:def 5;

then n,j are_congruent_mod 4 * (Py (a,i)) by A35, INT_1:15;

then A36: ( n,i are_congruent_mod 4 * (Py (a,i)) or n, - i are_congruent_mod 4 * (Py (a,i)) ) by A34, INT_1:15;

A37: 1 * (Py (a,i)) < 4 * (Py (a,i)) by A9, A1, A11, XREAL_1:97;

A38: n < 4 * (Py (a,i)) by A11, A9, A37, XXREAL_0:2;

A39: i <= Py (a,i) by HILB10_1:13;

then reconsider Pi = (4 * (Py (a,i))) - i as Nat by NAT_1:21, A37, XXREAL_0:2;

A40: i < 4 * (Py (a,i)) by A39, A37, XXREAL_0:2;

A41: (4 * (Py (a,i))) + (- i) < (4 * (Py (a,i))) + 0 by A31, XREAL_1:8;

n = i

( 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 Lm1, A4;

consider i being Nat such that

A11: ( x = Px (a,i) & y = Py (a,i) ) by A2, HILB10_1:4;

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 A3, HILB10_1:4;

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

then
n1 <> 0
by A13, HILB10_1:3;
assume A21:
v = 0
; :: thesis: contradiction

then A22: u = 1 by A18, A13, A14, NAT_1:15;

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 A23, A6, XREAL_1:232;

then s * s = 1 by A10, SQUARE_1:def 1;

then 1 = x + (c * 1) by A22, A7, NAT_1:15;

then x = 1 by A11, GAUSSINT:1;

then y * y = 0 by A19, A12, A11;

hence contradiction by A9, A1; :: thesis: verum

end;then A22: u = 1 by A18, A13, A14, NAT_1:15;

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 A23, A6, XREAL_1:232;

then s * s = 1 by A10, SQUARE_1:def 1;

then 1 = x + (c * 1) by A22, A7, NAT_1:15;

then x = 1 by A11, GAUSSINT:1;

then y * y = 0 by A19, A12, A11;

hence contradiction by A9, A1; :: thesis: verum

then n1 >= 1 + 0 by NAT_1:13;

then A24: a <= u by A13, A17, HILB10_1:10;

u > 1 by NEWTON03:def 1, A24, XXREAL_0:2;

then A25: ( a * 1 < u * u & u ^2 = u * u ) by A24, XREAL_1:97, SQUARE_1:def 1;

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 A4, HILB10_1:4;

r > 0 by A5, A20;

then A28: r >= 0 + 1 by NAT_1:13;

y >= 1 by A9, A1, XXREAL_0:2;

then y * y >= y * 1 by XREAL_1:66;

then r * (y * y) >= y * 1 by A28, XREAL_1:66;

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 Th16, A13, INT_1:def 5;

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 A11, A13, A27, INT_1:def 5;

then Px (a,i), Px (a,j) are_congruent_mod Px (a,n1) by A30, INT_1:15;

then A32: ( j,i are_congruent_mod 4 * n1 or j, - i are_congruent_mod 4 * n1 ) by A31, A29, A5, HILB10_1:11, A13, Th24, A11, A19;

(Py (a,i)) ^2 divides Py (a,n1) by A5, A11, A13, INT_1:def 3;

then consider divN being Nat such that

A33: (Py (a,i)) * divN = n1 by NAT_D:def 3, HILB10_1:37;

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 A32, INT_1:20;

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 HILB10_1:24, A11, INT_1:20;

(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 INT_1:14, INT_1:def 5;

then n,j are_congruent_mod 4 * (Py (a,i)) by A35, INT_1:15;

then A36: ( n,i are_congruent_mod 4 * (Py (a,i)) or n, - i are_congruent_mod 4 * (Py (a,i)) ) by A34, INT_1:15;

A37: 1 * (Py (a,i)) < 4 * (Py (a,i)) by A9, A1, A11, XREAL_1:97;

A38: n < 4 * (Py (a,i)) by A11, A9, A37, XXREAL_0:2;

A39: i <= Py (a,i) by HILB10_1:13;

then reconsider Pi = (4 * (Py (a,i))) - i as Nat by NAT_1:21, A37, XXREAL_0:2;

A40: i < 4 * (Py (a,i)) by A39, A37, XXREAL_0:2;

A41: (4 * (Py (a,i))) + (- i) < (4 * (Py (a,i))) + 0 by A31, XREAL_1:8;

n = i

proof

hence
( not b is trivial & u ^2 > a & y = Py (a,n) )
by A26, A6, A25, A11; :: thesis: verum
assume
n <> i
; :: thesis: contradiction

then - i,n are_congruent_mod 4 * (Py (a,i)) by INT_1:14, A36, A38, A40, Lm7;

then A42: Pi = n by A41, A38, Lm7, INT_1:21;

A43: (4 * (Py (a,i))) - i >= (4 * (Py (a,i))) - (Py (a,i)) by HILB10_1:13, XREAL_1:10;

((Py (a,i)) + (Py (a,i))) + (Py (a,i)) > (Py (a,i)) + 0 by A9, A1, XREAL_1:8, A11;

hence contradiction by A42, A11, A9, A43, XXREAL_0:2; :: thesis: verum

end;then - i,n are_congruent_mod 4 * (Py (a,i)) by INT_1:14, A36, A38, A40, Lm7;

then A42: Pi = n by A41, A38, Lm7, INT_1:21;

A43: (4 * (Py (a,i))) - i >= (4 * (Py (a,i))) - (Py (a,i)) by HILB10_1:13, XREAL_1:10;

((Py (a,i)) + (Py (a,i))) + (Py (a,i)) > (Py (a,i)) + 0 by A9, A1, XREAL_1:8, A11;

hence contradiction by A42, A11, A9, A43, XXREAL_0:2; :: thesis: verum