let A be non trivial Nat; :: thesis: for C, B, e being Nat st 0 < B & C = Py (A,B) holds
ex i, j, D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
let C, B be Nat; :: thesis: for e being Nat st 0 < B & C = Py (A,B) holds
ex i, j, D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
let e be Nat; :: thesis: ( 0 < B & C = Py (A,B) implies ex i, j, D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )
assume that
A1: B > 0 and
A2: C = Py (A,B) ; :: thesis: ex i, j, D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
set x = Px (A,B);
set D = (Px (A,B)) ^2 ;
( Px (A,0) = 1 & Py (A,0) = 0 ) by HILB10_1:3;
then A3: ( Px (A,(0 + 1)) = (1 * A) + (0 * ((A ^2) -' 1)) & Py (A,(0 + 1)) = 1 + (0 * A) ) by HILB10_1:6;
A4: (Px (A,B)) * (Px (A,B)) <> 0 ;
A5: (Px (A,B)) ^2 > 0 by A4, SQUARE_1:def 1;
ex q, i being Nat st (((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * (i + 1) = Py (A,q)

proof

set t = e + 1;
A6: ( 2 ^2 = 2 * 2 & ((Px (A,B)) ^2) ^2 = ((Px (A,B)) ^2) * ((Px (A,B)) ^2) & (e + 1) ^2 = (e + 1) * (e + 1) & (C ^2) ^2 = (C ^2) * (C ^2) & C ^2 = C * C ) by SQUARE_1:def 1;
then reconsider dd = (((((A ^2) -' 1) * (2 ^2)) * (((Px (A,B)) ^2) ^2)) * ((e + 1) ^2)) * ((C ^2) ^2) as non square Nat by A5, A1, A2;
consider x, y being Nat such that
A7: ( (x ^2) - (dd * (y ^2)) = 1 & y <> 0 ) by PELLS_EQ:14;
reconsider i = y - 1 as Nat by A7;
A8: ((((2 ^2) * (((Px (A,B)) ^2) ^2)) * ((e + 1) ^2)) * ((C ^2) ^2)) * (y ^2) = ((((2 * 2) * (((Px (A,B)) ^2) * ((Px (A,B)) ^2))) * ((e + 1) * (e + 1))) * ((C ^2) * (C ^2))) * (y * y) by A6, SQUARE_1:def 1
.= ((((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * y) * ((((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * y)
.= ((((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * y) ^2 by SQUARE_1:def 1 ;
(x ^2) - (((A ^2) -' 1) * (((((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * y) ^2)) = 1 by A7, A8;
then [x,((((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * y)] is Pell's_solution of (A ^2) -' 1 by Lm1;
then consider n being Nat such that
A9: ( x = Px (A,n) & (((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * y = Py (A,n) ) by HILB10_1:4;
take n ; :: thesis: ex i being Nat st (((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * (i + 1) = Py (A,n)
take i ; :: thesis: (((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * (i + 1) = Py (A,n)
thus (((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * (i + 1) = Py (A,n) by A9; :: thesis: verum

end;

then consider q, i being Nat such that
A10: (((2 * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2)) * (i + 1) = Py (A,q) ;
set E = Py (A,q);
set F = (Px (A,q)) ^2 ;
((Px (A,B)) ^2) - (((A ^2) -' 1) * (C ^2)) = 1 by A2, HILB10_1:7;
then A11: (Px (A,B)) ^2 = (((A ^2) -' 1) * (C ^2)) + 1 ;
A12: ((Px (A,q)) ^2) - (((A ^2) -' 1) * ((Py (A,q)) ^2)) = 1 by HILB10_1:7;
then A13: (Px (A,q)) ^2 = (((A ^2) -' 1) * ((Py (A,q)) ^2)) + 1 ;
A14: C ^2 = C * C by SQUARE_1:def 1;
q <> 0 by A5, A1, A2, A14, HILB10_1:3, A10;
then q >= 1 + 0 by NAT_1:13;
then A15: A <= Px (A,q) by A3, HILB10_1:10;
then Px (A,q) > 1 by NEWTON03:def 1, XXREAL_0:2;
then A16: ( A * 1 < (Px (A,q)) * (Px (A,q)) & (Px (A,q)) * (Px (A,q)) = (Px (A,q)) ^2 ) by A15, XREAL_1:97, SQUARE_1:def 1;
then ((Px (A,q)) ^2) - A > 0 by XREAL_1:50;
then reconsider G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) as non trivial Nat by A16;
set H = Py (G,B);
set I = (Px (G,B)) ^2 ;
A17: ((Px (G,B)) ^2) - (((G ^2) -' 1) * ((Py (G,B)) ^2)) = 1 by HILB10_1:7;
Py (G,B),B are_congruent_mod 2 * C

proof

A18: (Py (A,q)) ^2 = (Py (A,q)) * (Py (A,q)) by SQUARE_1:def 1;
A19: ((A ^2) -' 1) * (Py (A,q)),((A ^2) -' 1) * (Py (A,q)) are_congruent_mod 2 * C by INT_1:11;
A20: 1,1 are_congruent_mod 2 * C by INT_1:11;
A21: A,A are_congruent_mod 2 * C by INT_1:11;
C ^2 = C * C by SQUARE_1:def 1;
then ((((i + 1) * ((Px (A,B)) ^2)) * (e + 1)) * C) * (2 * C) = (Py (A,q)) - 0 by A10;
then Py (A,q), 0 are_congruent_mod 2 * C by INT_1:def 5;
then (((A ^2) -' 1) * (Py (A,q))) * (Py (A,q)),(((A ^2) -' 1) * (Py (A,q))) * 0 are_congruent_mod 2 * C by A19, INT_1:18;
then A22: (((A ^2) -' 1) * ((Py (A,q)) ^2)) + 1,0 + 1 are_congruent_mod 2 * C by A18, A20, INT_1:16;
then ((Px (A,q)) ^2) - A,1 - A are_congruent_mod 2 * C by A12, A21, INT_1:17;
then ((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A),1 * (1 - A) are_congruent_mod 2 * C by A22, A12, INT_1:18;
then A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)),A + (1 * (1 - A)) are_congruent_mod 2 * C by A21, INT_1:16;
then ex i4 being Integer st (2 * C) * i4 = G - 1 by INT_1:def 5;
hence Py (G,B),B are_congruent_mod 2 * C by HILB10_1:24, INT_1:20; :: thesis: verum

end;

then consider j being Integer such that
A23: (Py (G,B)) - B = (2 * C) * j by INT_1:def 5;
j * (2 * C) >= B - B by A23, HILB10_1:13, XREAL_1:9;
then j >= 0 by A1, A2;
then reconsider j = j as Element of NAT by INT_1:3;
A * A = A ^2 by SQUARE_1:def 1;
then A24: A ^2 >= 1 + 0 by NAT_1:13;
G * G = G ^2 by SQUARE_1:def 1;
then A25: G ^2 >= 1 + 0 by NAT_1:13;
(A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A))) - A = ((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A) ;
then A26: Py (G,B),C are_congruent_mod (Px (A,q)) ^2 by A2, HILB10_1:26, INT_1:def 5;
take i ; :: thesis: ex j, D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take j ; :: thesis: ex D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take (Px (A,B)) ^2 ; :: thesis: ex E, F, G, H, I being Nat st
( (((Px (A,B)) ^2) * F) * I is square & F divides H - C & B <= C & (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take Py (A,q) ; :: thesis: ex F, G, H, I being Nat st
( (((Px (A,B)) ^2) * F) * I is square & F divides H - C & B <= C & (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take (Px (A,q)) ^2 ; :: thesis: ex G, H, I being Nat st
( (((Px (A,B)) ^2) * ((Px (A,q)) ^2)) * I is square & (Px (A,q)) ^2 divides H - C & B <= C & (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & (Px (A,q)) ^2 = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take G ; :: thesis: ex H, I being Nat st
( (((Px (A,B)) ^2) * ((Px (A,q)) ^2)) * I is square & (Px (A,q)) ^2 divides H - C & B <= C & (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & (Px (A,q)) ^2 = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take Py (G,B) ; :: thesis: ex I being Nat st
( (((Px (A,B)) ^2) * ((Px (A,q)) ^2)) * I is square & (Px (A,q)) ^2 divides (Py (G,B)) - C & B <= C & (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & (Px (A,q)) ^2 = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) & Py (G,B) = B + ((2 * j) * C) & I = (((G ^2) - 1) * ((Py (G,B)) ^2)) + 1 )
take (Px (G,B)) ^2 ; :: thesis: ( (((Px (A,B)) ^2) * ((Px (A,q)) ^2)) * ((Px (G,B)) ^2) is square & (Px (A,q)) ^2 divides (Py (G,B)) - C & B <= C & (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & (Px (A,q)) ^2 = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) & Py (G,B) = B + ((2 * j) * C) & (Px (G,B)) ^2 = (((G ^2) - 1) * ((Py (G,B)) ^2)) + 1 )
thus ( (((Px (A,B)) ^2) * ((Px (A,q)) ^2)) * ((Px (G,B)) ^2) is square & (Px (A,q)) ^2 divides (Py (G,B)) - C & B <= C ) by A2, HILB10_1:13, A26, INT_1:def 4; :: thesis: ( (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & (Px (A,q)) ^2 = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) & Py (G,B) = B + ((2 * j) * C) & (Px (G,B)) ^2 = (((G ^2) - 1) * ((Py (G,B)) ^2)) + 1 )
((Px (G,B)) ^2) - (((G ^2) - 1) * ((Py (G,B)) ^2)) = 1 by A17, A25, XREAL_1:233;
hence ( (Px (A,B)) ^2 = (((A ^2) - 1) * (C ^2)) + 1 & Py (A,q) = (((2 * (i + 1)) * ((Px (A,B)) ^2)) * (e + 1)) * (C ^2) & (Px (A,q)) ^2 = (((A ^2) - 1) * ((Py (A,q)) ^2)) + 1 & G = A + (((Px (A,q)) ^2) * (((Px (A,q)) ^2) - A)) & Py (G,B) = B + ((2 * j) * C) & (Px (G,B)) ^2 = (((G ^2) - 1) * ((Py (G,B)) ^2)) + 1 ) by A11, A24, A10, A13, A23, XREAL_1:233; :: thesis: verum