let y, z, a be Nat; :: thesis: ( ( y = Py (a,z) & a > 1 ) iff ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) )
thus ( y = Py (a,z) & a > 1 implies ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) ) :: thesis: ( ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) implies ( y = Py (a,z) & a > 1 ) )
proof
assume A1: ( y = Py (a,z) & a > 1 ) ; :: thesis: ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 )
then A2: not a is trivial by NAT_2:28;
set x = Px (a,z);
A3: a >= 1 + 1 by NAT_1:13, A1;
A4: (a ^2) -' 1 = (a ^2) - 1 by XREAL_1:233, NAT_1:14, A1;
((Px (a,z)) ^2) - (((a ^2) -' 1) * (y ^2)) = 1 by A1, Th10, A2;
then A5: ( [(Px (a,z)),y] is Pell's_solution of (a ^2) -' 1 & a > 1 ) by A1, Lm3;
A6: y >= z by Th16, A1, A2;
per cases ( y = 0 or y > 0 ) ;
suppose A7: y = 0 ; :: thesis: ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 )
then A8: z = 0 by A1, A2;
then A9: Px (a,z) = 1 by Th6, A2;
set x1 = Px (a,z);
set y1 = y;
set y2 = y;
set A = 1;
(1 ^2) -' 1 = 1 - 1 by XREAL_1:233;
then A10: (1 ^2) - (((1 ^2) -' 1) * (y ^2)) = 1 ;
( 1 in INT & 0 in INT ) by INT_1:def 2;
then A11: [1,0] in [:INT,INT:] by ZFMISC_1:87;
( [1,0] `1 = 1 & [1,0] `2 = 0 ) ;
then A12: [1,y] is Pell's_solution of (1 ^2) -' 1 by A10, A11, A7, PELLS_EQ:def 1;
A13: y,y are_congruent_mod Px (a,z) by INT_1:11;
A14: 1,a are_congruent_mod Px (a,z) by INT_1:13, A9;
A15: 1,1 are_congruent_mod 2 * y by INT_1:11;
y, 0 are_congruent_mod y ^2 by A7, INT_1:11;
hence ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) by A5, A12, A13, A14, A8, A7, A15; :: thesis: verum
end;
suppose A16: y > 0 ; :: thesis: ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 )
reconsider B = ((a ^2) -' 1) * ((2 * (y ^2)) ^2) as non square Nat by A2, A16;
set M = min_Pell's_solution_of B;
set x1 = (min_Pell's_solution_of B) `1 ;
set Y1 = (min_Pell's_solution_of B) `2 ;
A17: (((min_Pell's_solution_of B) `1) ^2) - (B * (((min_Pell's_solution_of B) `2) ^2)) = 1 by PELLS_EQ:def 1;
set y1 = (2 * (y ^2)) * ((min_Pell's_solution_of B) `2);
A18: ( (min_Pell's_solution_of B) `1 = [((min_Pell's_solution_of B) `1),((2 * (y ^2)) * ((min_Pell's_solution_of B) `2))] `1 & (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) = [((min_Pell's_solution_of B) `1),((2 * (y ^2)) * ((min_Pell's_solution_of B) `2))] `2 ) ;
( (min_Pell's_solution_of B) `1 in INT & (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) in INT ) by INT_1:def 2;
then A19: [((min_Pell's_solution_of B) `1),((2 * (y ^2)) * ((min_Pell's_solution_of B) `2))] in [:INT,INT:] by ZFMISC_1:87;
A20: (((min_Pell's_solution_of B) `1) ^2) - (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2)) = (1 + (B * (((min_Pell's_solution_of B) `2) ^2))) - (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2)) by PELLS_EQ:def 1
.= 1 ;
then A21: [((min_Pell's_solution_of B) `1),((2 * (y ^2)) * ((min_Pell's_solution_of B) `2))] is Pell's_solution of (a ^2) -' 1 by A18, A19, PELLS_EQ:def 1;
(2 * ((min_Pell's_solution_of B) `2)) * y >= 1 * 1 by A16, NAT_1:14;
then A22: ((2 * ((min_Pell's_solution_of B) `2)) * y) * y >= 1 * y by XREAL_1:66;
A23: (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) > 0 by A22;
then A24: ( ((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2 >= 1 & (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) >= 1 ) by NAT_1:14;
( (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) = (y ^2) * (2 * ((min_Pell's_solution_of B) `2)) & (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) = (2 * y) * (y * ((min_Pell's_solution_of B) `2)) ) ;
then A25: ( y ^2 divides ((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) - 0 & 2 * y divides (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) ) by INT_1:def 3;
then A26: (2 * (y ^2)) * ((min_Pell's_solution_of B) `2), 0 are_congruent_mod y ^2 by INT_1:def 4;
( a ^2 >= 2 * a & a + a > a + 1 ) by A2, A1, NAT_2:29, XREAL_1:8, XREAL_1:64;
then a ^2 > a + 1 by XXREAL_0:2;
then A27: (a ^2) -' 1 > a by A4, XREAL_1:20;
then A28: B > a * 1 by A16, NAT_1:14, XREAL_1:97;
((min_Pell's_solution_of B) `2) ^2 >= 1 ^2 by NAT_1:14;
then 1 + (B * (((min_Pell's_solution_of B) `2) ^2)) > a by NAT_1:13, A28, XREAL_1:66;
then (((min_Pell's_solution_of B) `1) ^2) - a >= a - a by A17, XREAL_1:9;
then reconsider x1a = (((min_Pell's_solution_of B) `1) ^2) - a as Element of NAT by INT_1:3;
set A = a + ((((min_Pell's_solution_of B) `1) ^2) * x1a);
a + ((((min_Pell's_solution_of B) `1) ^2) * x1a) >= 2 + 0 by A3, XREAL_1:7;
then ( a + ((((min_Pell's_solution_of B) `1) ^2) * x1a) <> 1 & not a + ((((min_Pell's_solution_of B) `1) ^2) * x1a) is empty ) ;
then reconsider A = a + ((((min_Pell's_solution_of B) `1) ^2) * x1a) as non trivial Nat by NAT_2:28;
A - a = ((min_Pell's_solution_of B) `1) * (((min_Pell's_solution_of B) `1) * x1a) ;
then A29: A,a are_congruent_mod (min_Pell's_solution_of B) `1 by INT_1:def 4, INT_1:def 3;
A = a + ((1 + (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2))) * ((1 + (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2))) - a)) by A20;
then A30: A - 1 = ((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) * ((((a ^2) -' 1) + ((1 + (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2))) * ((a ^2) -' 1))) - (a * ((a ^2) -' 1)))) ;
then A31: (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) divides A - 1 by INT_1:def 3;
then A32: 2 * y divides A - 1 by A25, INT_2:9;
A33: A,1 are_congruent_mod 2 * y by A31, A25, INT_2:9, INT_1:def 4;
((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2) >= a * 1 by A27, A24, XREAL_1:66;
then 2 + (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2)) > (a * 1) + 0 by XREAL_1:8;
then (2 + (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2))) - a > a - a by XREAL_1:9;
then ((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) * (((a ^2) -' 1) * ((2 + (((a ^2) -' 1) * (((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) ^2))) - a)) >= 1 * 1 by A2, A23, NAT_1:14;
then ( A - 1 >= 1 * ((2 * (y ^2)) * ((min_Pell's_solution_of B) `2)) & A - 0 > A - 1 ) by A30, XREAL_1:66, XREAL_1:10;
then A > (2 * (y ^2)) * ((min_Pell's_solution_of B) `2) by XXREAL_0:2;
then A34: A > y by A22, XXREAL_0:2;
set x2 = Px (A,z);
set y2 = Py (A,z);
((Px (A,z)) ^2) - (((A ^2) -' 1) * ((Py (A,z)) ^2)) = 1 by Th10;
then A35: [(Px (A,z)),(Py (A,z))] is Pell's_solution of (A ^2) -' 1 by Lm3;
A - 1 divides (Py (A,z)) - z by Th27, INT_1:def 4;
then Py (A,z),z are_congruent_mod 2 * y by INT_1:def 4, A32, INT_2:9;
hence ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) by A5, A21, A6, A35, A2, A1, Th29, A29, A33, A26, A22, A34; :: thesis: verum
end;
end;
end;
given x, x1, y1, A, x2, y2 being Nat such that A36: a > 1 and
A37: [x,y] is Pell's_solution of (a ^2) -' 1 and
A38: [x1,y1] is Pell's_solution of (a ^2) -' 1 and
A39: ( y1 >= y & A > y ) and
A40: y >= z and
A41: [x2,y2] is Pell's_solution of (A ^2) -' 1 and
A42: y2,y are_congruent_mod x1 and
A43: A,a are_congruent_mod x1 and
A44: y2,z are_congruent_mod 2 * y and
A45: A,1 are_congruent_mod 2 * y and
A46: y1, 0 are_congruent_mod y ^2 ; :: thesis: ( y = Py (a,z) & a > 1 )
A47: not a is trivial by NAT_2:28, A36;
per cases ( y = 0 or y > 0 ) ;
suppose A48: y = 0 ; :: thesis: ( y = Py (a,z) & a > 1 )
then z = 0 by A40;
hence ( y = Py (a,z) & a > 1 ) by A36, A47, Th6, A48; :: thesis: verum
end;
suppose A49: y > 0 ; :: thesis: ( y = Py (a,z) & a > 1 )
then y >= 1 by NAT_1:14;
then reconsider A = A as non trivial Nat by A39, NAT_2:28;
consider w being Nat such that
A50: ( x = Px (a,w) & y = Py (a,w) ) by A47, A37, Th7;
consider u being Nat such that
A51: ( x1 = Px (a,u) & y1 = Py (a,u) ) by A47, A38, Th7;
consider v being Nat such that
A52: ( x2 = Px (A,v) & y2 = Py (A,v) ) by A41, Th7;
A53: y2, Py (a,v) are_congruent_mod x1 by A47, A43, A52, Th29;
y,y2 are_congruent_mod x1 by A42, INT_1:14;
then A54: y, Py (a,v) are_congruent_mod Px (a,u) by A51, A53, INT_1:15;
A55: u <> 0 by Th6, A51, A49, A39, A47;
Py (A,v),v are_congruent_mod 2 * y then v,y2 are_congruent_mod 2 * y by A52, INT_1:14;
then A57: v,z are_congruent_mod 2 * y by A44, INT_1:15;
A58: y ^2 divides y1 - 0 by A46, INT_1:def 4;
A59: z,v are_congruent_mod 2 * y by A57, INT_1:14;
A60: Py (a,v), Py (a,w) are_congruent_mod Px (a,u) by A54, A50, INT_1:14;
consider r being Integer such that
A61: y * r = u by A58, A51, A50, Th40, INT_1:def 3, A47;
A62: y >= w by A47, A50, Th16;
A63: ( 0 - y <= z - w & z - w <= y - 0 ) by A40, A62, XREAL_1:13;
( y + 0 < y + y & (- y) - y < (- y) - 0 ) by A49, XREAL_1:6, XREAL_1:15;
then A64: ( (- 1) * (2 * y) < z - w & z - w < 1 * (2 * y) ) by A63, XXREAL_0:2;
A65: ( 0 + 0 <= z + w & z + w <= y + y ) by A40, A62, XREAL_1:7;
per cases ( v,w are_congruent_mod 2 * u or v, - w are_congruent_mod 2 * u ) by A60, A55, Th36, A47;
suppose v,w are_congruent_mod 2 * u ; :: thesis: ( y = Py (a,z) & a > 1 )
then consider t being Integer such that
A66: v - w = (2 * u) * t by INT_1:def 5;
v - w = (2 * y) * (t * r) by A66, A61;
then v,w are_congruent_mod 2 * y by INT_1:def 5;
then consider i being Integer such that
A67: z - w = (2 * y) * i by INT_1:def 5, A59, INT_1:15;
( - 1 < i & i < 0 + 1 ) by A67, A64, XREAL_1:64;
then ( (- 1) + 1 <= i & i <= 0 ) by INT_1:7;
then z - w = 0 by A67;
hence ( y = Py (a,z) & a > 1 ) by A36, A50; :: thesis: verum
end;
suppose v, - w are_congruent_mod 2 * u ; :: thesis: ( y = Py (a,z) & a > 1 )
then consider t being Integer such that
A68: v - (- w) = (2 * u) * t by INT_1:def 5;
v - (- w) = (2 * y) * (t * r) by A61, A68;
then v, - w are_congruent_mod 2 * y by INT_1:def 5;
then consider i being Integer such that
A69: z - (- w) = (2 * y) * i by INT_1:def 5, A59, INT_1:15;
( (2 * y) * 0 <= (2 * y) * i & (2 * y) * i <= (2 * y) * 1 ) by A69, A65;
then A70: ( 0 <= i & i <= 1 ) by A49, XREAL_1:68;
( i < 1 or i = 1 ) by A70, XXREAL_0:1;
then A71: ( i = 0 or i = 1 ) by A70, NAT_1:14;
per cases ( z + w = 0 or z + w = 2 * y ) by A71, A69;
suppose z + w = 0 ; :: thesis: ( y = Py (a,z) & a > 1 )
then ( z = 0 & 0 = w ) ;
hence ( y = Py (a,z) & a > 1 ) by A36, A50; :: thesis: verum
end;
suppose A72: z + w = 2 * y ; :: thesis: ( y = Py (a,z) & a > 1 )
A73: z = y
proof
assume z <> y ; :: thesis: contradiction
then z < y by A40, XXREAL_0:1;
then z + w < y + y by A47, A50, Th16, XREAL_1:8;
hence contradiction by A72; :: thesis: verum
end;
w = y
proof
assume w <> y ; :: thesis: contradiction
then w < y by A62, XXREAL_0:1;
then z + w < y + y by A40, XREAL_1:8;
hence contradiction by A72; :: thesis: verum
end;
hence ( y = Py (a,z) & a > 1 ) by A36, A73, A50; :: thesis: verum
end;
end;
end;
end;
end;
end;