let a be non trivial Nat; :: thesis: for y, n being Nat st 1 <= n & y = Py (a,n) holds
ex b, c, d, r, s, t, u, v, x being Nat st
( [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 )
let y, n be Nat; :: thesis: ( 1 <= n & y = Py (a,n) implies ex b, c, d, r, s, t, u, v, x being Nat st
( [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 ) )
assume that
A1: n >= 1 and
A2: y = Py (a,n) ; :: thesis: ex b, c, d, r, s, t, u, v, x being Nat st
( [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 )
set x = Px (a,n);
set m = (4 * n) * y;
set u = Px (a,((4 * n) * y));
set v = Py (a,((4 * n) * y));
A3: ((Px (a,n)) ^2) - (((a ^2) -' 1) * (y ^2)) = 1 by A2, HILB10_1:7;
A4: ((Px (a,((4 * n) * y))) ^2) - (((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) = 1 by HILB10_1:7;
A5: Py (a,(n * y)),(y * ((Px (a,n)) |^ (y -' 1))) * y are_congruent_mod y ^2 by A2, HILB10_1:35;
y ^2 = y * y by SQUARE_1:def 1;
then (y * ((Px (a,n)) |^ (y -' 1))) * y = (y ^2) * ((Px (a,n)) |^ (y -' 1)) ;
then (y * ((Px (a,n)) |^ (y -' 1))) * y, 0 are_congruent_mod y ^2 by INT_1:60;
then y ^2 divides (Py (a,(n * y))) - 0 by A5, INT_1:15, INT_1:def 4;
then consider R being Nat such that
A6: (y ^2) * R = Py (a,(n * y)) by NAT_D:def 3;
set r = (R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2)));
A7: Py (a,((n * y) * 2)) = (2 * (Py (a,(n * y)))) * (Px (a,(n * y))) by Th25;
A8: Py (a,(((n * y) * 2) * 2)) = (2 * (Py (a,((n * y) * 2)))) * (Px (a,((n * y) * 2))) by Th25;
( Px (a,0) = 1 & Py (a,0) = 0 ) by HILB10_1:3;
then A9: ( Px (a,(0 + 1)) = (1 * a) + (0 * ((a ^2) -' 1)) & Py (a,(0 + 1)) = 1 + (0 * a) ) by HILB10_1:6;
A10: (4 * n) * y >= 1 + 0 by A1, A2, NAT_1:13;
then A11: a <= Px (a,((4 * n) * y)) by A9, HILB10_1:10;
then Px (a,((4 * n) * y)) > 1 by NEWTON03:def 1, XXREAL_0:2;
then A12: ( a * 1 < (Px (a,((4 * n) * y))) * (Px (a,((4 * n) * y))) & (Px (a,((4 * n) * y))) ^2 = (Px (a,((4 * n) * y))) * (Px (a,((4 * n) * y))) ) by A11, XREAL_1:97, SQUARE_1:def 1;
then A13: ((Px (a,((4 * n) * y))) ^2) - a > 0 by XREAL_1:50;
then reconsider b = a + (((Px (a,((4 * n) * y))) ^2) * (((Px (a,((4 * n) * y))) ^2) - a)) as non trivial Nat by A12;
set s = Px (b,n);
set t = Py (b,n);
A14: ((Px (b,n)) ^2) - (((b ^2) -' 1) * ((Py (b,n)) ^2)) = 1 by HILB10_1:7;
b - a = (Px (a,((4 * n) * y))) * ((Px (a,((4 * n) * y))) * (((Px (a,((4 * n) * y))) ^2) - a)) by A12;
then Px (b,n), Px (a,n) are_congruent_mod Px (a,((4 * n) * y)) by Th16, INT_1:def 5;
then consider c being Integer such that
A15: (Px (a,((4 * n) * y))) * c = (Px (b,n)) - (Px (a,n)) by INT_1:def 5;
b > a + 0 by A13, A12, XREAL_1:8;
then c >= 0 by Th15, A15, XREAL_1:48;
then reconsider c = c as Element of NAT by INT_1:3;
consider D being Integer such that
A16: (b - 1) * D = (Py (b,n)) - n by INT_1:def 5, HILB10_1:24;
D >= 0 by A16, XREAL_1:48, HILB10_1:13;
then reconsider D = D as Element of NAT by INT_1:3;
set Z = ((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2);
set d = ((((((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2)))) * y) * ((a ^2) -' 1)) * (Py (a,((4 * n) * y)))) * (((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) + 2) - a)) * D;
A17: y ^2 = y * y by SQUARE_1:def 1;
A18: (Py (a,((4 * n) * y))) ^2 = (Py (a,((4 * n) * y))) * (Py (a,((4 * n) * y))) by SQUARE_1:def 1;
A19: a * a = a ^2 by SQUARE_1:def 1;
then a ^2 >= 1 + 0 by NAT_1:13;
then A20: (a ^2) -' 1 = (a ^2) - 1 by XREAL_1:233;
Py (a,((4 * n) * y)) >= (4 * n) * y by HILB10_1:13;
then ( Py (a,((4 * n) * y)) >= 1 & (Py (a,((4 * n) * y))) ^2 = (Py (a,((4 * n) * y))) * (Py (a,((4 * n) * y))) ) by A10, XXREAL_0:2, SQUARE_1:def 1;
then A21: (Py (a,((4 * n) * y))) ^2 >= 1 * 1 by XREAL_1:66;
a * a > a * 1 by XREAL_1:97, NEWTON03:def 1;
then a ^2 >= a + 1 by A19, NAT_1:13;
then (a ^2) -' 1 >= a by A20, XREAL_1:19;
then ((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2) >= a * 1 by A21, XREAL_1:66;
then (((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) - a >= 0 by XREAL_1:48;
then ((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) - a) + 2 >= 0 + 0 ;
then reconsider d = ((((((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2)))) * y) * ((a ^2) -' 1)) * (Py (a,((4 * n) * y)))) * (((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) + 2) - a)) * D as Element of NAT by INT_1:3;
take b ; :: thesis: ex c, d, r, s, t, u, v, x being Nat st
( [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 )
take c ; :: thesis: ex d, r, s, t, u, v, x being Nat st
( [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 )
take d ; :: thesis: ex r, s, t, u, v, x being Nat st
( [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 )
take (R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))) ; :: thesis: ex s, t, u, v, x being Nat st
( [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 * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & s = x + (c * u) & t = n + ((4 * d) * y) & n <= y )
take Px (b,n) ; :: thesis: ex t, u, v, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [(Px (b,n)),t] is Pell's_solution of (b ^2) -' 1 & v = (4 * ((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & Px (b,n) = x + (c * u) & t = n + ((4 * d) * y) & n <= y )
take Py (b,n) ; :: thesis: ex u, v, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [(Px (b,n)),(Py (b,n))] is Pell's_solution of (b ^2) -' 1 & v = (4 * ((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & Px (b,n) = x + (c * u) & Py (b,n) = n + ((4 * d) * y) & n <= y )
take Px (a,((4 * n) * y)) ; :: thesis: ex v, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & [(Px (a,((4 * n) * y))),v] is Pell's_solution of (a ^2) -' 1 & [(Px (b,n)),(Py (b,n))] is Pell's_solution of (b ^2) -' 1 & v = (4 * ((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + (((Px (a,((4 * n) * y))) ^2) * (((Px (a,((4 * n) * y))) ^2) - a)) & Px (b,n) = x + (c * (Px (a,((4 * n) * y)))) & Py (b,n) = n + ((4 * d) * y) & n <= y )
take Py (a,((4 * n) * y)) ; :: thesis: ex x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & [(Px (a,((4 * n) * y))),(Py (a,((4 * n) * y)))] is Pell's_solution of (a ^2) -' 1 & [(Px (b,n)),(Py (b,n))] is Pell's_solution of (b ^2) -' 1 & Py (a,((4 * n) * y)) = (4 * ((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + (((Px (a,((4 * n) * y))) ^2) * (((Px (a,((4 * n) * y))) ^2) - a)) & Px (b,n) = x + (c * (Px (a,((4 * n) * y)))) & Py (b,n) = n + ((4 * d) * y) & n <= y )
take Px (a,n) ; :: thesis: ( [(Px (a,n)),y] is Pell's_solution of (a ^2) -' 1 & [(Px (a,((4 * n) * y))),(Py (a,((4 * n) * y)))] is Pell's_solution of (a ^2) -' 1 & [(Px (b,n)),(Py (b,n))] is Pell's_solution of (b ^2) -' 1 & Py (a,((4 * n) * y)) = (4 * ((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + (((Px (a,((4 * n) * y))) ^2) * (((Px (a,((4 * n) * y))) ^2) - a)) & Px (b,n) = (Px (a,n)) + (c * (Px (a,((4 * n) * y)))) & Py (b,n) = n + ((4 * d) * y) & n <= y )
A22: b = a + (((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) + 1) * (((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) + 1) - a)) by A4
.= (((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) * (((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2))) + ((((a ^2) -' 1) * ((Py (a,((4 * n) * y))) ^2)) * (2 - a))) + 1 ;
Py (b,n) = n + ((b - 1) * D) by A16;
hence ( [(Px (a,n)),y] is Pell's_solution of (a ^2) -' 1 & [(Px (a,((4 * n) * y))),(Py (a,((4 * n) * y)))] is Pell's_solution of (a ^2) -' 1 & [(Px (b,n)),(Py (b,n))] is Pell's_solution of (b ^2) -' 1 & Py (a,((4 * n) * y)) = (4 * ((R * (Px (a,(n * y)))) * (Px (a,((n * y) * 2))))) * (y ^2) & b = a + (((Px (a,((4 * n) * y))) ^2) * (((Px (a,((4 * n) * y))) ^2) - a)) & Px (b,n) = (Px (a,n)) + (c * (Px (a,((4 * n) * y)))) & Py (b,n) = n + ((4 * d) * y) & n <= y ) by A17, A18, A3, A4, A14, Lm1, A8, A6, A7, A15, A2, HILB10_1:13, A22; :: thesis: verum