let a be non trivial Nat; 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; ( 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
; ( 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
assume A21:
v = 0
;
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;
verum
end;
then
n1 <> 0
by A13, HILB10_1:3;
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
assume
n <> i
;
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;
verum
end;
hence
( not b is trivial & u ^2 > a & y = Py (a,n) )
by A26, A6, A25, A11; verum