let A be non trivial Nat; :: thesis: for C, B, e being Nat st 0 < B holds
for i, j being Nat
for D, E, F, G, H, I being Integer 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 holds
C = Py (A,B)
let C, B be Nat; :: thesis: for e being Nat st 0 < B holds
for i, j being Nat
for D, E, F, G, H, I being Integer 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 holds
C = Py (A,B)
let e be Nat; :: thesis: ( 0 < B implies for i, j being Nat
for D, E, F, G, H, I being Integer 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 holds
C = Py (A,B) )
assume A1: 0 < B ; :: thesis: for i, j being Nat
for D, E, F, G, H, I being Integer 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 holds
C = Py (A,B)
let i, j be Nat; :: thesis: for D, E, F, G, H, I being Integer 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 holds
C = Py (A,B)
let D, E, F, G, H, I be Integer; :: thesis: ( (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 implies C = Py (A,B) )
assume that
A2: ( (D * F) * I is square & F divides H - C & B <= C ) and
A3: D = (((A ^2) - 1) * (C ^2)) + 1 and
A4: E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) and
A5: F = (((A ^2) - 1) * (E ^2)) + 1 and
A6: G = A + (F * (F - A)) and
A7: H = B + ((2 * j) * C) and
A8: I = (((G ^2) - 1) * (H ^2)) + 1 ; :: thesis: C = Py (A,B)
A9: A * A = A ^2 by SQUARE_1:def 1;
then A ^2 >= 1 + 0 by NAT_1:13;
then A10: (A ^2) -' 1 = (A ^2) - 1 by XREAL_1:233;
A11: ( C ^2 = C * C & C * C > 0 ) by A1, A2, SQUARE_1:def 1;
reconsider D = D as Element of NAT by INT_1:3, A9, A3;
reconsider E = E as Element of NAT by A9, A3, A4, INT_1:3;
( E ^2 = E * E & E * E > 0 ) by A9, A3, A11, A4, SQUARE_1:def 1;
then A12: E ^2 >= 1 by NAT_1:14;
reconsider F = F as Element of NAT by A9, A5, INT_1:3;
A13: A >= 2 by NAT_2:29;
A - 1 >= 2 - 1 by NAT_2:29, XREAL_1:9;
then (A - 1) * (A + 1) >= 1 * (A + 1) by XREAL_1:64;
then ((A - 1) * (A + 1)) * (E ^2) >= (1 * (A + 1)) * 1 by A12, XREAL_1:66;
then (((A - 1) * (A + 1)) * (E ^2)) + 1 >= (A + 1) + 0 by XREAL_1:7;
then A14: F > A by A9, A5, NAT_1:13;
then A15: F - A > A - A by XREAL_1:14;
then G > 0 + A by A6, XREAL_1:8, A9, A5;
then A16: G > 1 + 1 by A13, XXREAL_0:2;
reconsider G = G as Element of NAT by A15, A6, INT_1:3;
G > 1 by NAT_1:13, A16;
then reconsider G = G as non trivial Element of NAT by NEWTON03:def 1;
reconsider H = H as Element of NAT by A7, INT_1:3;
A17: G * G = G ^2 by SQUARE_1:def 1;
then G ^2 >= 1 + 0 by NAT_1:13;
then A18: (G ^2) -' 1 = (G ^2) - 1 by XREAL_1:233;
reconsider I = I as Element of NAT by A17, A8, INT_1:3;
A19: E ^2 = E * E by SQUARE_1:def 1;
A20: ((A ^2) -' 1) * E,((A ^2) -' 1) * E are_congruent_mod 2 * C by INT_1:11;
A21: 1,1 are_congruent_mod 2 * C by INT_1:11;
A22: A,A are_congruent_mod 2 * C by INT_1:11;
A23: ((A ^2) -' 1) * E,((A ^2) -' 1) * E are_congruent_mod D by INT_1:11;
A24: 1,1 are_congruent_mod D by INT_1:11;
A25: F - A,F - A are_congruent_mod D by INT_1:11;
A26: A,A are_congruent_mod D by INT_1:11;
A27: H ^2 ,H ^2 are_congruent_mod D by INT_1:11;
A28: 1,1 are_congruent_mod F by INT_1:11;
E - 0 = (((2 * (i + 1)) * (e + 1)) * (C ^2)) * D by A4;
then A29: E, 0 are_congruent_mod D by INT_1:def 5;
(((A ^2) -' 1) * E) * E,(((A ^2) -' 1) * E) * 0 are_congruent_mod D by A29, A23, INT_1:18;
then A30: (((A ^2) -' 1) * (E ^2)) + 1,0 + 1 are_congruent_mod D by A19, A24, INT_1:16;
then F * (F - A),1 * (F - A) are_congruent_mod D by A10, A5, A25, INT_1:18;
then G,(1 * (F - A)) + A are_congruent_mod D by A6, A26, INT_1:16;
then G,1 are_congruent_mod D by A30, A10, A5, INT_1:15;
then G * G,1 * 1 are_congruent_mod D by INT_1:18;
then G ^2 ,1 are_congruent_mod D by SQUARE_1:def 1;
then (G ^2) - 1,1 - 1 are_congruent_mod D by A24, INT_1:17;
then ((G ^2) - 1) * (H ^2),0 * (H ^2) are_congruent_mod D by A27, INT_1:18;
then A31: I,0 + 1 are_congruent_mod D by A24, A8, INT_1:16;
A32: G - A = F * (F - A) by A6;
then A33: G,A are_congruent_mod F by INT_1:def 5;
A34: H * H = H ^2 by SQUARE_1:def 1;
A35: H,C are_congruent_mod F by A2, INT_1:def 4;
then A36: ( H ^2 ,C ^2 are_congruent_mod F & G ^2 ,A ^2 are_congruent_mod F ) by A11, A9, A17, A34, A33, INT_1:18;
then (G ^2) - 1,(A ^2) - 1 are_congruent_mod F by INT_1:17, A28;
then A37: ((G ^2) - 1) * (H ^2),((A ^2) - 1) * (C ^2) are_congruent_mod F by A36, INT_1:18;
A38: ( F gcd D = 1 gcd D & 1 gcd D = 1 ) by WSIERP_1:8, WSIERP_1:43, A30, A10, A5;
then A39: F,D are_coprime by INT_2:def 3;
I gcd D = 1 gcd D by WSIERP_1:43, A31;
then I,D are_coprime by WSIERP_1:8, INT_2:def 3;
then A40: F * I,D are_coprime by A39, INT_2:26;
I gcd F = D gcd F by WSIERP_1:43, A37, A3, A8, A28, INT_1:16;
then A41: I,F are_coprime by A38, INT_2:def 3;
(F * I) * D is square by A2;
then A42: ( F * I is square & D is square ) by A40, PYTHTRIP:1;
then A43: ( F is square & I is square ) by A41, PYTHTRIP:1;
consider d being Nat such that
A44: d ^2 = D by A42, PYTHTRIP:def 3;
consider f being Nat such that
A45: f ^2 = F by A43, PYTHTRIP:def 3;
consider ii being Nat such that
A46: ii ^2 = I by A43, PYTHTRIP:def 3;
(d ^2) - (((A ^2) -' 1) * (C ^2)) = 1 by A44, A3, A10;
then [d,C] is Pell's_solution of (A ^2) -' 1 by Lm1;
then consider i1 being Nat such that
A47: ( d = Px (A,i1) & C = Py (A,i1) ) by HILB10_1:4;
(f ^2) - (((A ^2) -' 1) * (E ^2)) = 1 by A5, A45, A10;
then [f,E] is Pell's_solution of (A ^2) -' 1 by Lm1;
then consider n1 being Nat such that
A48: ( f = Px (A,n1) & E = Py (A,n1) ) by HILB10_1:4;
(ii ^2) - (((G ^2) -' 1) * (H ^2)) = 1 by A18, A46, A8;
then [ii,H] is Pell's_solution of (G ^2) -' 1 by Lm1;
then consider j1 being Nat such that
A49: ( ii = Px (G,j1) & H = Py (G,j1) ) by HILB10_1:4;
A50: Py (G,j1),j1 are_congruent_mod 2 * C
proof
C ^2 = C * C by SQUARE_1:def 1;
then ((((i + 1) * D) * (e + 1)) * C) * (2 * C) = E - 0 by A4;
then E, 0 are_congruent_mod 2 * C by INT_1:def 5;
then (((A ^2) -' 1) * E) * E,(((A ^2) -' 1) * E) * 0 are_congruent_mod 2 * C by A20, INT_1:18;
then A51: (((A ^2) -' 1) * (E ^2)) + 1,0 + 1 are_congruent_mod 2 * C by A19, A21, INT_1:16;
then F - A,1 - A are_congruent_mod 2 * C by A10, A5, A22, INT_1:17;
then F * (F - A),1 * (1 - A) are_congruent_mod 2 * C by A10, A51, A5, INT_1:18;
then A + (F * (F - A)),A + (1 * (1 - A)) are_congruent_mod 2 * C by A22, INT_1:16;
then ex i4 being Integer st (2 * C) * i4 = G - 1 by A6, INT_1:def 5;
hence Py (G,j1),j1 are_congruent_mod 2 * C by INT_1:20, HILB10_1:24; :: thesis: verum
end;
B - H = (2 * C) * (- j) by A7;
then B, Py (G,j1) are_congruent_mod 2 * C by A49, INT_1:def 5;
then A52: B,j1 are_congruent_mod 2 * C by A50, INT_1:15;
Py (G,j1), Py (A,j1) are_congruent_mod F by A32, INT_1:def 5, HILB10_1:26;
then A53: Py (A,j1), Py (G,j1) are_congruent_mod F by INT_1:14;
A54: F divides (Py (A,j1)) - (Py (A,i1)) by A35, A47, A49, A53, INT_1:15, INT_1:def 4;
( Px (A,n1) divides (Px (A,n1)) * (Px (A,n1)) & (Px (A,n1)) * (Px (A,n1)) = (Px (A,n1)) ^2 & (Px (A,n1)) ^2 = F ) by A48, SQUARE_1:def 1, INT_1:def 3, A45;
then A55: Py (A,j1), Py (A,i1) are_congruent_mod Px (A,n1) by A54, INT_2:9, INT_1:def 4;
Py (A,i1) divides n1 by A47, A48, HILB10_1:37, A4, INT_1:def 3;
then A57: 2 * (Py (A,i1)) divides 2 * n1 by PYTHTRIP:7;
( f * f = F & F > 2 ) by A13, A14, XXREAL_0:2, A45, SQUARE_1:def 1;
then ( f <> 1 & 1 = Px (A,0) ) by HILB10_1:3;
then n1 <> 0 by A48;
then ( j1,i1 are_congruent_mod 2 * n1 or j1, - i1 are_congruent_mod 2 * n1 ) by A55, HILB10_1:33;
then ( 2 * n1 divides j1 - i1 or 2 * n1 divides j1 - (- i1) ) by INT_1:def 4;
then A58: ( j1,i1 are_congruent_mod 2 * (Py (A,i1)) or j1, - i1 are_congruent_mod 2 * (Py (A,i1)) ) by INT_1:def 4, INT_2:9, A57;
A59: i1 <= C by A47, HILB10_1:13;
per cases ( B,i1 are_congruent_mod 2 * C or B, - i1 are_congruent_mod 2 * C ) by A58, A47, A52, INT_1:15;
suppose B,i1 are_congruent_mod 2 * C ; :: thesis: C = Py (A,B)
then consider z being Integer such that
A60: (2 * C) * z = B - i1 by INT_1:def 5;
A61: 1 * C < 2 * C by A2, A1, XREAL_1:68;
then A62: (- 1) * (2 * C) < (- 1) * C by XREAL_1:69;
( 0 - C <= B - i1 & B - i1 <= C - 0 ) by A2, A59, XREAL_1:13;
then ( (- 1) * (2 * C) < (2 * C) * z & (2 * C) * z < (2 * C) * 1 ) by A60, A62, A61, XXREAL_0:2;
then ( - 1 < z & z < 1 + 0 ) by XREAL_1:64;
then ( (- 1) + 1 <= z & z <= 0 ) by INT_1:7;
then z = 0 ;
hence C = Py (A,B) by A60, A47; :: thesis: verum
end;
suppose B, - i1 are_congruent_mod 2 * C ; :: thesis: C = Py (A,B)
then consider z being Integer such that
A63: (2 * C) * z = B - (- i1) by INT_1:def 5;
( 0 + 0 < B + i1 & B + i1 <= C + C ) by A2, A1, A59, XREAL_1:7;
then ( 0 * (2 * C) < z * (2 * C) & z * (2 * C) <= (2 * C) * 1 ) by A63;
then ( 0 < z & z <= 1 ) by XREAL_1:68;
then ( 0 + 1 <= z & z <= 1 ) by INT_1:7;
then A64: z = 1 by XXREAL_0:1;
then A65: B + i1 = C + C by A63;
B = C hence C = Py (A,B) by A64, A63, A47; :: thesis: verum
end;
end;