:: The {M}atiyasevich Theorem -- Preliminaries
:: by Karol P\kak
::
:: Received November 29, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XXREAL_0, SUBSET_1, TARSKI, ARYTM_3, RELAT_1, ARYTM_1,
CARD_1, SQUARE_1, REAL_1, PYTHTRIP, FUNCT_1, XBOOLE_0, ZFMISC_1, MCART_1,
NAT_1, INT_1, COMPLEX1, FINSEQ_1, NEWTON, PELLS_EQ, HILB10_1, ABSVALUE,
ABIAN, INT_2, XCMPLX_0, VALUED_0, FINSEQ_2, ORDINAL4, CARD_3, POWER;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, XXREAL_0, SQUARE_1, INT_1, FUNCT_1, DOMAIN_1,
PYTHTRIP, VALUED_0, FINSEQ_2, RVSUM_1, ABSVALUE, POWER, NEWTON, NAT_D,
PELLS_EQ, ABIAN, INT_2, FINSEQ_1;
constructors RELSET_1, DOMAIN_1, PEPIN, NEWTON, NAT_D, PELLS_EQ, ABSVALUE,
ABIAN, WSIERP_1, POWER;
registrations NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, SQUARE_1,
RELAT_1, FUNCT_1, XTUPLE_0, NAT_1, MEMBERED, MCART_1, NEWTON03, INT_1,
NEWTON, PYTHTRIP, VALUED_0, PELLS_EQ, ABIAN, NEWTON02, ABSVALUE, NAT_6,
XBOOLE_0, FINSEQ_1, FINSEQ_2, VALUED_1, CARD_1, RVSUM_1, POWER, NEWTON04,
FOMODEL0, NAT_5;
requirements NUMERALS, SUBSET, ARITHM, REAL;
definitions TARSKI;
equalities SQUARE_1, FINSEQ_1;
expansions PELLS_EQ;
theorems TARSKI, FUNCT_1, CARD_1, NAT_1, ZFMISC_1, XREAL_1, XXREAL_0, NEWTON,
PYTHTRIP, INT_1, FINSEQ_3, FINSEQ_1, SQUARE_1, XCMPLX_1, ABSVALUE,
COMPLEX1, XREAL_0, NEWTON02, PEPIN, PELLS_EQ, NAT_2, RVSUM_1, ABIAN,
FINSEQ_5, VALUED_0, FINSEQ_2, VALUED_1, POWER, INT_4, EULER_1, INT_2,
NAT_D, RVSUM_2, ORDINAL1, WSIERP_1;
schemes NAT_1, FINSEQ_1;
begin :: Preliminaries
reserve i,j,n,n1,n2,m,k,u for Nat,
r,r1,r2 for Real,
x,y for Integer,
a,b for non trivial Nat;
Lm1: [\(2*n +1)/ 2 /] = n
proof
2*n < 2*n +1 by NAT_1:13;
then
A1:n < (2*n +1)/ 2 by XREAL_1:81;
2*n -1 < 2*n -0 by XREAL_1:15;
then (2*n +1-2)/ 2 <n by XREAL_1:83;
then (2*n +1)/ 2 - 2/2 <n;
hence thesis by A1,INT_1:def 6;
end;
Lm2:[/(2*n +1)/ 2 \] = n+1
proof
2*n+1 <= 2*n+1+1 by NAT_1:11;
then 2*n +1 <= 2*(n+1);
then
A1: (2*n +1)/ 2 <= n+1 by XREAL_1:79;
2*n < 2*n +1 by NAT_1:13;
then n+1 < (2*n +1)/ 2+1 by XREAL_1:6,81;
hence thesis by A1,INT_1:def 7;
end;
theorem Th1:
for F be FinSequence of NAT st
for k st 1 < k <= len F holds (F.k) mod n = 0
holds Sum F mod n = (F.1) mod n
proof
defpred P[Nat] means for F be FinSequence of NAT st
len F = $1 & for k st 1 < k <= len F holds (F.k) mod n = 0
holds Sum F mod n = (F.1) mod n;
A1:P[0]
proof
let F be FinSequence of NAT such that A2: len F = 0;
F = {} by A2;
hence thesis;
end;
A3:P[k] implies P[k+1]
proof
assume
A4: P[k];set k1=k+1;
let F be FinSequence of NAT such that
A5: len F = k+1 and
A6: for i be Nat st 1<i<=len F holds (F.i) mod n = 0;
per cases;
suppose k=0;
then F = <*F.1*> by A5,FINSEQ_1:40;
hence thesis;
end;
suppose
A7: k >0;
F is non empty by A5;
then len F in dom F by FINSEQ_5:6;
then (F|k) ^ <*F.k1*> = F| k1 by A5,FINSEQ_5:10
.=F by A5;
then
A8: Sum F = Sum (F|k) + F.k1 by RVSUM_1:74;
A9: k <= k1 by NAT_1:11;
A10: len (F|k) = k by A5,NAT_1:11,FINSEQ_1:59;
for i be Nat st 1 < i <= len (F|k) holds ((F|k).i) mod n = 0
proof
let i be Nat such that
A11: 1< i <= len (F|k);
(F|k).i = F.i & i <= len F by A10,A11,A5,A9,FINSEQ_3:112,XXREAL_0:2;
hence thesis by A11,A6;
end;
then
A12: Sum (F|k) mod n = ((F|k).1) mod n by A4,A10;
A13: F.1 mod n = Sum (F|k) mod n by A7,NAT_1:14,A12,FINSEQ_3:112;
per cases;
suppose n=0;
then Sum F mod n = 0 = (F.1) mod n;
hence thesis;
end;
suppose
A14: n >0;
A15: Sum(F|k) is Nat & Sum(F) is Nat by TARSKI:1;
0+1< k1 by A7,XREAL_1:8;
then 0= (Sum F - Sum (F|k))mod n by A5,A6,A8;
hence thesis by A13, A15,A14,INT_4:22;
end;
end;
end;
P[k] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th2:
for f be complex-valued FinSequence
ex e,o be complex-valued FinSequence st
len e = [\len f/2/] & len o = [/len f/2 \] &
Sum f = Sum e + Sum o &
for n holds e.n = f.(2*n) & o.n = f.(2*n-1)
proof
defpred P[Nat] means
for f be complex-valued FinSequence st len f=$1
ex e,o be complex-valued FinSequence st
len e = [\len f/2/] & len o = [/len f/2 \] &
Sum f = Sum e + Sum o &
for n holds e.n = f.(2*n) & o.n = f.(2*n-1);
A1:P[0]
proof
let f be complex-valued FinSequence such that
A2: len f=0;
take f,f;
thus len f = [\len f/2/] & len f = [/len f/2 \] by A2;
f=<*>REAL by A2;
hence Sum f=Sum f+Sum f by RVSUM_1:72;
let n;
f={} by A2;
then f.n = 0=f.(2*n) & f.n = 0 = f.(2*n-1);
hence thesis;
end;
A3: P[n] implies P[n+1]
proof
assume
A4: P[n];set n1=n+1;
let f be complex-valued FinSequence such that
A5: len f=n1;
set fn=f|n;
A6: f = fn^<*f.n1*> by A5,FINSEQ_3:55;
n < n1 by NAT_1:13;
then len fn = n by A5,FINSEQ_1:59;
then consider e,o be complex-valued FinSequence such that
A7: len e = [\n/2/] & len o = [/n/2 \] and
A8: Sum (fn) = Sum e + Sum o and
A9: for k holds e.k = fn.(2*k) & o.k = fn.(2*k-1) by A4;
per cases;
suppose n is even;
then consider k such that
A10: 2*k=n by ABIAN:def 2;
take e,oF=o^<*f.n1*>;
A11: len oF = len o+1 by FINSEQ_2:16;
A12: [\n/2/] = k = [\(n+1)/2/] & [/n/2 \] = k & [/(n+1)/2 \] =k+1
by A10,Lm1,Lm2;
hence len e = [\len f/2/] & len oF = [/len f/2 \]
by FINSEQ_2:16,A5,A7;
thus Sum f = Sum fn+f.n1 by A6,RVSUM_2:31
.= Sum e + (Sum o+f.n1) by A8
.= Sum e + Sum oF by RVSUM_2:31;
let i be Nat;
thus e.i = f.(2*i)
proof
per cases;
suppose 2*i <=n;
then fn.(2*i) = f.(2*i) by FINSEQ_3:112;
hence thesis by A9;
end;
suppose 2*i > n;
then
A13: i > k by A10,XREAL_1:64;
then i >= k+1 by NAT_1:13;
then 2*i >= 2*(k+1) & 2*(k+1) = len f+1 by A10,A5,XREAL_1:64;
then 2*i > len f by NAT_1:13;
then not 2*i in dom f & not i in dom e
by FINSEQ_3:25,A7,A12,A13;
then f.(2*i) = 0 = e.i by FUNCT_1:def 2;
hence thesis;
end;
end;
thus oF.i = f.(2*i-1)
proof
per cases;
suppose i=0;
then not i in dom oF & not (2*i-1) in dom f
by FINSEQ_3:25;
then oF.i = 0 = f.(2*i-1) by FUNCT_1:def 2;
hence thesis;
end;
suppose
A14: i<>0 & 2*i <=n;
then 1<= i <= k by A10,XREAL_1:68,NAT_1:14;
then i in dom o by A7,A12,FINSEQ_3:25;
then
A15: oF.i = o.i by FINSEQ_1:def 7
.= fn.(2*i-1) by A9;
2*i-1 <=n-0 by XREAL_1:13,A14;
hence thesis by A15,A14,FINSEQ_3:112;
end;
suppose 2*i > n;
then i > k by A10,XREAL_1:64;
then i >= k+1 by NAT_1:13;
then 2*i >= 2*(k+1) & 2*(k+1) = len f+1 by A10,A5,XREAL_1:64;
then
A16: 2*i-1 >= len f by XREAL_1:19;
per cases by A16,XXREAL_0:1;
suppose 2*i-1 = len f;
hence thesis by A5,A10,A7,A12;
end;
suppose
A17: 2*i -1 > len f;
then not (2*i-1) in dom f by FINSEQ_3:25;
then
A18: f.(2*i-1) = 0 by FUNCT_1:def 2;
2*i > len f+1 by A17,XREAL_1:20;
then 2*i > 2*(k+1) by A10,A5;
then i > k+1 by XREAL_1:64;
then not i in dom oF by A11,A12,A7,FINSEQ_3:25;
hence thesis by A18,FUNCT_1:def 2;
end;
end;
end;
end;
suppose n is odd;
then consider k such that
A19: n =2*k+1 by ABIAN:9;
take eF=e^<*f.n1*>,o;
A20: len eF = len e+1 by FINSEQ_2:16;
A21: [\n/2/] = k & [\(n+1)/2/]=k+1 & [/n/2 \] = k+1 &
[/(n+1)/2 \] =k+1 by A19,Lm1,Lm2;
hence len eF = [\len f/2/] & len o = [/len f/2 \] by FINSEQ_2:16,A5,A7;
thus Sum f = Sum fn+f.n1 by A6,RVSUM_2:31
.= (Sum e + f.n1) + Sum o by A8
.= Sum eF + Sum o by RVSUM_2:31;
let i be Nat;
thus eF.i = f.(2*i)
proof
per cases;
suppose i=0;
hence thesis;
end;
suppose i <>0 & i <= k;
then 1<=i<=k & 2*i <= 2*k by NAT_1:14,XREAL_1:64;
then i in dom e & 2*i < n by A19,NAT_1:13,FINSEQ_3:25,A7,A21;
then eF.i =e.i & fn.(2*i) = f.(2*i) by FINSEQ_1:def 7,FINSEQ_3:112;
hence thesis by A9;
end;
suppose i > k;
then
A22: i >= k+1 by NAT_1:13;
per cases by A22,XXREAL_0:1;
suppose i = k+1;
hence thesis by A19,A7,A21;
end;
suppose
A23: i > k+1;
then not i in dom eF by FINSEQ_3:25,A7,A20,A21;
then
A24: eF.i = 0 by FUNCT_1:def 2;
2*i > 2*(k+1) by A23,XREAL_1:68;
then not 2*i in dom f by A5,A19,FINSEQ_3:25;
hence thesis by A24,FUNCT_1:def 2;
end;
end;
end;
thus o.i = f.(2*i-1)
proof
per cases;
suppose i =0;
then not i in dom o & not (2*i-1) in dom f by FINSEQ_3:25;
then o.i= 0 = f.(2*i-1) by FUNCT_1:def 2;
hence thesis;
end;
suppose
A25: i<>0 & 2*i-1 <=n;
fn.(2*i-1) = f.(2*i-1) by A25,FINSEQ_3:112;
hence thesis by A9;
end;
suppose 2*i-1 > n;
then 2*i > n+1 by XREAL_1:20;
then 2*i > 2*(k+1) by A19;
then
A26: i > k+1 by XREAL_1:64;
then not i in dom o by FINSEQ_3:25,A7,A21;
then
A27: o.i = 0 by FUNCT_1:def 2;
i >= k+1+1 by A26,NAT_1:13;
then 2*i >= 2*(k+1+1) by XREAL_1:64;
then 2*i >= len f+1+1 by A19,A5;
then 2*i > len f+1 by NAT_1:13;
then not 2*i-1 in dom f by XREAL_1:20,FINSEQ_3:25;
hence thesis by A27,FUNCT_1:def 2;
end;
end;
end;
end;
P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
registration
let a;
cluster a^2 -' 1 -> non square;
coherence
proof
assume
A1: a^2 -' 1 is square;
a >=2 by NAT_2:29;
then
A2: a^2>=2*2 by XREAL_1:66;
A3: a^2-'1 = a^2-1 by XREAL_1:233,NAT_1:14;
then a^2-'1 is non zero by A2;
then a^2-'1+1 is non square by A1;
hence thesis by A3;
end;
end;
begin :: Solutions of Pell's Equation - Special Case
definition
let a,n be Nat;
assume A1:a is non trivial;
func Px(a,n) -> Nat means :Def1:
for b be non trivial Nat st b=a
ex y be Nat st
it + y*sqrt (b^2-'1) =
( (min_Pell's_solution_of (b^2-'1))`1 +
(min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n;
existence
proof
reconsider A=a as non trivial Nat by A1;
consider x,y be Nat such that
A2: x + y*sqrt (A^2-'1) =
( (min_Pell's_solution_of (A^2-'1))`1 +
(min_Pell's_solution_of (A^2-'1))`2 *sqrt ((A^2-'1)) ) |^ n
by PELLS_EQ:4;
take x;
thus thesis by A2;
end;
uniqueness
proof
reconsider A=a as non trivial Nat by A1;
let p1,p2 be Nat such that
A3: for b be non trivial Nat st b=a
ex y be Nat st p1 + y*sqrt (b^2-'1) =
( (min_Pell's_solution_of (b^2-'1))`1 +
(min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n and
A4: for b be non trivial Nat st b=a
ex y be Nat st p2 + y*sqrt (b^2-'1) =
( (min_Pell's_solution_of (b^2-'1))`1 +
(min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n;
set m=min_Pell's_solution_of (A^2-'1);
A5: ex y be Nat st p1 + y*sqrt (A^2-'1) =
( m`1 + m`2 *sqrt ((A^2-'1)) ) |^ n by A3;
ex y be Nat st
p2 + y*sqrt (A^2-'1) =( m`1 + m`2 *sqrt ((A^2-'1)) ) |^ n by A4;
hence thesis by A5,PELLS_EQ:3;
end;
end;
definition
let a,n be Nat;
assume A1:a is non trivial;
func Py(a,n) -> Nat means :Def2:
for b be non trivial Nat st b=a holds
Px(b,n) + it*sqrt (b^2-'1) =
( (min_Pell's_solution_of (b^2-'1))`1 +
(min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n;
existence
proof
reconsider A=a as non trivial Nat by A1;
consider y be Nat such that
A2: Px(A,n) + y*sqrt (A^2-'1) =
( (min_Pell's_solution_of (A^2-'1))`1 +
(min_Pell's_solution_of (A^2-'1))`2 *sqrt ((A^2-'1)) ) |^ n by Def1;
take y;
thus thesis by A2;
end;
uniqueness
proof
reconsider A=a as non trivial Nat by A1;
let p1,p2 be Nat such that
A3: for b be non trivial Nat st b=a holds
Px(b,n) + p1*sqrt (b^2-'1) =
( (min_Pell's_solution_of (b^2-'1))`1 +
(min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n and
A4: for b be non trivial Nat st b=a holds
Px(b,n) + p2*sqrt (b^2-'1) =
( (min_Pell's_solution_of (b^2-'1))`1 +
(min_Pell's_solution_of (b^2-'1))`2 *sqrt ((b^2-'1)) ) |^ n;
set m=min_Pell's_solution_of (A^2-'1);
Px(A,n) + p1*sqrt (A^2-'1) = ( m`1 + m`2 *sqrt ((A^2-'1)) ) |^ n
= Px(A,n) + p2*sqrt (A^2-'1) by A3,A4;
hence thesis by PELLS_EQ:3;
end;
end;
theorem Th6:
Px(a,0) = 1 & Py(a,0) = 0
proof
set A = a^2-'1,M=min_Pell's_solution_of A;
Px(a,0) + Py(a,0)*sqrt (a^2-'1) = ( M`1 + M`2 *sqrt A ) |^ 0 by Def2
.= 1+0*sqrt A by NEWTON:4;
hence thesis by PELLS_EQ:3;
end;
Lm3:for x,y be Integer, D be Nat holds
x^2 - D*y^2 = 1 iff [x,y] is Pell's_solution of D
proof
let x,y be Integer, D be Nat;
A1:[x,y]`1 = x & [x,y]`2 =y;
x in INT & y in INT by INT_1:def 2;
then [x,y] in [:INT,INT:] by ZFMISC_1:87;
hence x^2 - D*y^2 = 1 implies [x,y] is Pell's_solution of D
by A1,PELLS_EQ:def 1;
assume [x,y] is Pell's_solution of D;
hence thesis by PELLS_EQ:def 1,A1;
end;
theorem Th7:
[n1,n2] is Pell's_solution of (a^2-'1) implies
ex n st n1 = Px(a,n) & n2 = Py(a,n)
proof
set D=a^2-'1;
assume
A1: [n1,n2] is Pell's_solution of D;
then reconsider N=[n1,n2] as Pell's_solution of D;
A2: n1^2-(a^2-'1)*n2^2 = 1 by A1,Lm3;
per cases;
suppose
A3: n2=0;
then n1 <=1 & n1 >=1 by A2,SQUARE_1:51,NAT_1:14;
then n1=1 by XXREAL_0:1;
then n1=Px(a,0) & n2=Py(a,0) by A3,Th6;
hence thesis;
end;
suppose n2 >0;
then N is positive by A2;
then consider n be positive Nat such that
A4: n1 + n2 * sqrt D =( (min_Pell's_solution_of D)`1 +
(min_Pell's_solution_of D)`2 *sqrt D ) |^ n by PELLS_EQ:21;
consider y be Nat such that
A5: Px(a,n) + y*sqrt D =
( (min_Pell's_solution_of D)`1 +
(min_Pell's_solution_of D)`2 *sqrt (D) ) |^ n
by Def1;
A6: n1 = Px(a,n) by A5,A4,PELLS_EQ:3;
Px(a,n) + Py(a,n)*sqrt D = n1 + n2 * sqrt D by A4,Def2;
then n2 = Py(a,n) by PELLS_EQ:3;
hence thesis by A6;
end;
end;
theorem Th8:
[a,1] = min_Pell's_solution_of (a^2-'1)
proof
set A=a^2-'1,M=min_Pell's_solution_of A;
assume
A1: [a,1] <> M;
a^2-'1 = a^2-1 by XREAL_1:233,NAT_1:14;
then a^2 - (a^2-'1)*1^2 = 1;
then reconsider a1 = [a,1] as Pell's_solution of A by Lm3;
M`1 <> a or M`2 <> 1 by A1;
then
A2: M`1 + M`2 * sqrt A <> a + 1 *sqrt A by PELLS_EQ:3;
A3: sqrt A >=0 by SQUARE_1:def 2;
a1 is positive;
then
A4: M`1 <= a1`1 & M`2 <= a1`2 by PELLS_EQ:def 3;
then M`2 * sqrt A <= a1`2 *sqrt A by A3,XREAL_1:64;
then M`1 + M`2 * sqrt A <= a1`1 + a1`2 *sqrt A by A4,XREAL_1:7;
then
A5: M`1 + M`2 * sqrt A < a1`1 + a1`2 *sqrt A by A2,XXREAL_0:1;
1 < M`1 + M`2 * sqrt A by PELLS_EQ:18;
hence thesis by NAT_1:14,A5,PELLS_EQ:19;
end;
theorem Th9:
Px(a,n+1) = Px(a,n)*a + Py(a,n)*(a^2-'1) &
Py(a,n+1) = Px(a,n) + Py(a,n)*a
proof
set A=a^2-'1,M=min_Pell's_solution_of A;
set n1=n+1;
A1:(sqrt A)^2 =A by SQUARE_1:def 2;
A2: M = [a,1] by Th8;
Px(a,n1) + Py(a,n1) * sqrt A = ( M`1 + M`2 * sqrt A) |^n1 by Def2
.= (M`1 + M`2 * sqrt A) |^n * (M`1 + M`2 * sqrt A) by NEWTON:6
.= (Px(a,n) + Py(a,n) * sqrt A) * (M`1 + M`2 * sqrt A) by Def2
.= (Px(a,n) * a + Py(a,n)* A) + (Px(a,n) + Py(a,n) * a) * sqrt A by A2,A1;
hence thesis by PELLS_EQ:3;
end;
theorem Th10:
Px(a,n)^2 - (a^2-'1) *Py(a,n)^2 = 1
proof
set m=min_Pell's_solution_of (a^2-'1);
per cases;
suppose n=0;
then Px(a,n) = 1 & Py(a,n) = 0 by Th6;
hence thesis;
end;
suppose
A1: n >0;
Px(a,n) + Py(a,n)*sqrt (a^2-'1) = (m`1 + m`2 *sqrt ((a^2-'1)) ) |^ n
by Def2;
then reconsider PP=[Px(a,n),Py(a,n)] as
positive Pell's_solution of (a^2-'1) by A1,PELLS_EQ:20;
(PP`1)^2 - (a^2-'1)* (PP`2)^2 =1 by PELLS_EQ:def 1;
hence thesis;
end;
end;
theorem Th11:
Px(a,n) + Py(a,n) * sqrt (a^2-'1) = (a + sqrt (a^2-'1)) |^ n &
Px(a,n) + (- Py(a,n)) * sqrt (a^2-'1) = (a - sqrt (a^2-'1)) |^ n
proof
set A=a^2-'1,M=min_Pell's_solution_of A;
set n1=n+1;
A1: M = [a,1] by Th8;
A2:Px(a,n) + Py(a,n) * sqrt A = ( M`1 + M`2 * sqrt A) |^n by Def2
.= (a+ 1*sqrt A) |^n by A1;
then Px(a,n) - Py(a,n) * sqrt A = (a- 1*sqrt A) |^n by PELLS_EQ:6;
hence thesis by A2;
end;
theorem Th12:
ex Fy,Fx be FinSequence of NAT st
Sum Fy = Py(a,n) & len Fy = [\ (n+1)/2 /] &
(for i st 1 <= i <= (n+1)/2 holds
Fy.i = (n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a^2-'1) |^ (i-'1))&
a|^n + Sum Fx = Px(a,n) & len Fx = [\ n/2 /] &
for i st 1 <= i <= n/2 holds
Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * (a^2-'1) |^ i
proof
set A = a^2-'1;
defpred P[Nat] means
ex Fy,Fx be FinSequence of NAT st
Sum Fy = Py(a,$1) & len Fy = [\ ($1+1)/2 /] &
(for i be Nat st 1 <= i <= ($1+1)/2 holds
Fy.i = ($1 choose (2*i-'1)) * a |^ ($1+1-'2*i) * A |^ (i-'1))&
a|^$1 + Sum Fx = Px(a,$1) & len Fx = [\ $1/2 /] &
for i be Nat st 1 <= i <= $1/2 holds
Fx.i = ($1 choose (2*i)) * a |^ ($1-'2*i) * A |^ i;
A1:P[0]
proof
set F = <*>NAT;
A2: len F = 0;
A3: 0 = [\(0*2+1)/2/] by Lm1;
A4: for i be Nat st 1 <= i <= (0+1)/2 holds
F.i = (0 choose (2*i-'1)) * a |^ (0+1-'2*i) * A |^ (i-'1) by XXREAL_0:2;
A5: Sum F = Py(a,0) by Th6;
a|^0 = 1 by NEWTON:4;
then
A6: a|^0 + Sum F = Px(a,0) by Th6;
for i be Nat st 1 <= i <= 0/2 holds
F.i = (0 choose (2*i)) * a |^ (0-'2*i) * A |^ i;
hence thesis by A2,A3,A4,A5,A6;
end;
A7: for n be Nat st P[n] holds P[n+1]
proof
let n;
set n1=n+1;
assume P[n];
then consider Fy,Fx be FinSequence of NAT such that
A8: Sum Fy = Py(a,n) & len Fy = [\ n1/2 /] and
A9: for i be Nat st 1 <= i <= n1/2 holds
Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ (i-'1)and
A10: a|^n + Sum Fx = Px(a,n) & len Fx = [\ n/2 /] and
A11: for i be Nat st 1 <= i <= n/2 holds
Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * A |^ i;
set Fxa = <*a|^n*>^Fx;
set Fx0=Fx^<*0*>;
set Fy0=Fy^<*0*>;
A12: Px(a,n1) = (a|^n + Sum Fx)*a + (Sum Fy)*A by Th9,A8,A10
.= (a|^n *a) + (Sum Fx)*a + (Sum Fy)*A
.= a|^n1 + (Sum Fx)*a + (Sum Fy)*A by NEWTON:6
.= a|^n1 + Sum (a*Fx) + (Sum Fy)*A by RVSUM_1:87;
A13: (Sum Fy)*A = Sum (A*Fy) by RVSUM_1:87;
A14: Sum Fy0 = Sum Fy+0 by RVSUM_1:74;
A15: Sum Fx0 = Sum Fx+0 by RVSUM_1:74;
A16: Sum (a*Fx0) = a * Sum Fx0 by RVSUM_1:87;
A17: Py(a,n1) = Px(a,n) + Py(a,n) * a by Th9
.= Sum Fxa + (Sum Fy) *a by A8,A10,RVSUM_1:76;
per cases;
suppose
A18: n is odd;
then consider k such that
A19: n = 2*k+1 by ABIAN:9;
set k1=k+1;
A20: [\ n1/2 /] = k1 & [\ n/2 /] = k by A19,Lm1;
then
A21: len Fxa =k1 & len (a*Fy) = k1 by A10,FINSEQ_5:8,A8,RVSUM_1:117;
rng Fxa c= REAL & rng (a*Fy) c= REAL;
then Fxa is FinSequence of REAL & a*Fy is FinSequence of REAL
by FINSEQ_1:def 4;
then reconsider FxA=Fxa,aFy=a*Fy as Element of k1-tuples_on REAL
by A21,FINSEQ_2:92;
rng (Fxa + a*Fy) c= NAT by VALUED_0:def 6;
then reconsider FY = Fxa + a*Fy as FinSequence of NAT by FINSEQ_1:def 4;
A22: len (a*Fx0) = len Fx0 = k1 & len (A*Fy) = k1
by A20,A8,A10,FINSEQ_2:16,RVSUM_1:117;
reconsider AFx0=a*Fx0,AFy=A*Fy as Element of k1-tuples_on REAL
by A22,FINSEQ_2:92;
rng (a*Fx0 + A*Fy) c= NAT by VALUED_0:def 6;
then reconsider FX = a*Fx0 + A*Fy as FinSequence of NAT
by FINSEQ_1:def 4;
take FY,FX;
thus Sum FY = Sum (FxA) + Sum aFy by RVSUM_1:89
.= Py(a,n1) by A17,RVSUM_1:87;
A23: n1+1 = 2*k1+1 by A19;
len (FxA+aFy) = k1 by CARD_1:def 7;
hence len FY = [\(n1+1)/2/] by A23,Lm1;
thus for i be Nat st 1 <= i <= (n1+1)/2 holds
FY.i = (n1 choose (2*i-'1)) * a |^ ((n1+1)-'2*i) * A |^ (i-'1)
proof
let i be Nat such that
A24: 1 <= i <= (n1+1)/2;
set i1=i-'1;
A25: i1 +1 = i by A24,XREAL_1:235;
2*1 <=2*i by A24,XREAL_1:66;
then
A26: 2*i-'1 = 2*i-1 by XREAL_1:233,XXREAL_0:2;
A27: 2*i <= n1+1 by A24,XREAL_1:83;
then
A28: 2*i < n1+1 by A18,XXREAL_0:1;
then
A29: 2*i <= n1 by NAT_1:13;
A30: i <= n1/2 by A28,NAT_1:13,XREAL_1:77;
A31: n1-'2*i = n1-2*i by A29,XREAL_1:233;
A32: n1+1-'2*i = n1+1-2*i by XREAL_1:233,A27;
then
A33: n1+1-'2*i = 1+ (n1-'2*i) by A31;
Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A24,A9,A30;
then
A34: (a*Fy).i = a*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1)
by VALUED_1:6
.= (n choose (2*i-'1)) * (a * a |^ (n1-'2*i)) * A |^ i1
.= (n choose (2*i1+1)) * a |^ (n1+1-'2*i) * A |^ i1
by A26,A25,A33,NEWTON:6;
2*i <= n1+1 by A24,XREAL_1:83;
then 2*i1+1+1 <= n1+1 by A25;
then 2*i1+1 <= n1 by XREAL_1:8;
then
A35: 2*i1 < n1 by NAT_1:13;
then
A36: 2*i1 <=n by NAT_1:13;
then
A37: n-'2*i1 = n-2*i1 by XREAL_1:233;
A38: Fxa.i = (n choose (2*i1)) * a |^ (n-'2*i1) * A |^ i1
proof
per cases;
suppose
A39: i > 1;
then
A40: i1 >=1 by A25,NAT_1:13;
i1 <= n/2 by XREAL_1:77,A35,NAT_1:13;
then
A41: Fx.i1 = (n choose (2*i1)) * a |^ (n-'2*i1) * A |^ i1
by A11,A39,A25,NAT_1:13;
2*i1< 2*k+1 by A36,A19,XXREAL_0:1;
then i1 <= k by XREAL_1:68,NAT_1:13;
then i1 in dom Fx by A40,A20,A10,FINSEQ_3:25;
hence thesis by A41,A25,FINSEQ_3:103;
end;
suppose i <=1;
then
A42: i=1 by A24,XXREAL_0:1;
A43: n choose (2*i1) = 1 by A42,A25,NEWTON:19;
n-'2*i1 = n-0 by A42,A25,XREAL_1:233;
hence thesis by A43,NEWTON:4,A42,A25;
end;
end;
thus FY.i = (FxA.i) + (aFy.i) by RVSUM_1:11
.= ((n choose (2*i1))+(n choose (2*i1+1))) * a |^ (n1+1-'2*i) *
A |^ i1 by A38,A34,A37,A32,A25
.= (n1 choose (2*i-'1)) * a |^ (n1+1-'2*i) * A |^ i1
by A26,A25,NEWTON:22;
end;
Sum FX = Sum AFx0 + Sum AFy by RVSUM_1:89
.= Sum (a*Fx) + Sum (A*Fy) by RVSUM_1:87,A15,A16;
hence a|^n1 + Sum FX = Px(a,n1) by A12,A13;
len (AFx0 + AFy) = k1 by CARD_1:def 7;
hence len FX = [\ n1/2 /] by A19;
thus for i be Nat st 1 <= i <= n1/2 holds
FX.i = (n1 choose (2*i)) * a |^ (n1-'2*i) * A |^ i
proof
let i be Nat such that
A44: 1 <= i <= n1/2;
set i1=i-'1;
i1 +1 = i by A44,XREAL_1:235;
then
A45: A* A |^ i1 = A |^ i by NEWTON:6;
Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A9,A44;
then
A46: (A*Fy).i = A*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1)
by VALUED_1:6
.= (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i by A45;
2*i <= n1 by A44,XREAL_1:83;
then
A47: n1-'2*i=n1-2*i by XREAL_1:233;
A48: (a*Fx0).i = a * (Fx0.i) by VALUED_1:6;
A49: (a*Fx0).i = (n choose (2*i)) * a |^ (n1-'2*i) * A |^ i
proof
per cases;
suppose
A50: i <= k;
then
A51: 2*i < n by A19,NAT_1:13,XREAL_1:66;
then i <= n / 2 by XREAL_1:77;
then
A52: Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * A |^ i by A11,A44;
A53: i in dom Fx by A44,A50,A10,A20,FINSEQ_3:25;
A54: n-'2*i = n- 2*i by A51,XREAL_1:233;
n1-'2*i = 1+ (n-'2*i) by A54,A47;
then
A55: a |^ (n1-'2*i) = a * a |^ (n-'2*i) by NEWTON:6;
(a*Fx0).i = a*((n choose (2*i)) * a |^ (n-'2*i) * A |^ i)
by A48,A52,A53,FINSEQ_1:def 7
.= (n choose (2*i)) * a |^ (n1-'2*i) * A |^ i by A55;
hence thesis;
end;
suppose i > k;
then i >= k1 by NAT_1:13;
then
A56: 2*i >= 2*k1 by XREAL_1:66;
then
A57: 2*i >= n1 by A19;
2*i <= n1 by A44,XREAL_1:83;
then A58:2*i = 2*k1 by A56,A19,XXREAL_0:1;
2*i> n by A57,NAT_1:13;
then n choose (2*i)=0 by NEWTON:def 3;
hence thesis by A58,A10,A20,A48;
end;
end;
A59: 2*i-'1+1 =2*i by XREAL_1:235,NAT_1:14,A44;
thus FX.i = (AFx0).i + (AFy).i by RVSUM_1:11
.= ((n choose (2*i-'1))+(n choose (2*i)))* a |^ (n1-'2*i) * A |^ i
by A46,A49
.= (n1 choose (2*i))* a |^ (n1-'2*i) * A |^ i by A59,NEWTON:22;
end;
end;
suppose n is even;
then consider k such that
A60: n = 2*k by ABIAN:def 2;set k1=k+1;
A61: [\ n1/2 /] = k & [\ n/2 /] = k by A60,Lm1;
then
A62: len Fxa =k1 & len Fy0 = k1 & len (a*Fy0) = len Fy0
by FINSEQ_2:16,FINSEQ_5:8,A8,A10,RVSUM_1:117;
rng Fxa c= REAL & rng (a*Fy0) c= REAL;
then Fxa is FinSequence of REAL & a*Fy0 is FinSequence of REAL
by FINSEQ_1:def 4;
then reconsider FxA=Fxa,aFy0=a*Fy0 as Element of k1-tuples_on REAL
by A62,FINSEQ_2:92;
rng (Fxa + a*Fy0) c= NAT by VALUED_0:def 6;
then reconsider FY = Fxa + a*Fy0 as FinSequence of NAT by FINSEQ_1:def 4;
A63: len (a*Fx) = len Fx = k & len (A*Fy) = k by A61,A8,A10,RVSUM_1:117;
reconsider AFx=a*Fx,AFy=A*Fy as Element of k-tuples_on REAL
by A63,FINSEQ_2:92;
rng (a*Fx + A*Fy) c= NAT by VALUED_0:def 6;
then reconsider FX = a*Fx + A*Fy as FinSequence of NAT by FINSEQ_1:def 4;
take FY,FX;
thus Sum FY = Sum (FxA) + Sum aFy0 by RVSUM_1:89
.= Py(a,n1) by A17,A14,RVSUM_1:87;
len (FxA+aFy0) = k1 by CARD_1:def 7;
hence len FY = [\(n1+1)/2/] by A60;
thus for i be Nat st 1 <= i <= (n1+1)/2 holds
FY.i = (n1 choose (2*i-'1)) * a |^ ((n1+1)-'2*i) * A |^ (i-'1)
proof
let i be Nat such that
A64: 1 <= i <= (n1+1)/2;
set i1=i-'1;
A65: i1 +1 = i by A64,XREAL_1:235;
A66: 2*i <= n1+1 by A64,XREAL_1:83;
then
A67: 2*i1+2 <= n+2 by A65;
then
A68: 2*i1 <= n by XREAL_1:8;
A69: n-'2*i1 = n-2*i1 & n1+1-'2*i = n1+1-2*i by A67,A66,XREAL_1:8,233;
2*1 <=2*i by A64,XREAL_1:66;
then
A70: 2*i-'1 = 2*i-1 by XREAL_1:233,XXREAL_0:2;
A71: FxA.i = (n choose (2*i1)) * a |^ (n1+1-'2*i) * A |^ i1
proof
per cases;
suppose
A72: i > 1;
then
A73: i1 >=1 by A65,NAT_1:13;
i1 <= n/2 by A68,XREAL_1:77;
then
A74: Fx.i1 = (n choose (2*i1)) * a |^ (n-'2*i1) * A |^ i1
by A11,A72,A65,NAT_1:13;
i1 <= k by A68,A60,XREAL_1:68;
then i1 in dom Fx by A73,A61,A10,FINSEQ_3:25;
hence thesis by A69,A74,A65,FINSEQ_3:103;
end;
suppose i <=1;
then
A75: i=1 by A64,XXREAL_0:1;
A76: n choose (2*i1) = 1 by A75,A65,NEWTON:19;
n1+1-'2*i = n+2-2*1 by A75,NAT_1:11,XREAL_1:233;
hence thesis by A76,NEWTON:4,A75,A65;
end;
end;
A77: (a*Fy0).i = (n choose (2*i1+1)) * a |^ (n1+1-'2*i) * A |^ i1
proof
per cases;
suppose
A78: i <= k;
then
A79: 2*i <= n1 by NAT_1:13,A60,XREAL_1:66;
then
A80: 2*i <= n1+1 by NAT_1:13;
i <= n1 / 2 by A79, XREAL_1:77;
then
A81: Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A9,A64;
i in dom Fy by A64,A78,A8,A61,FINSEQ_3:25;
then
A82: Fy.i = Fy0.i by FINSEQ_1:def 7;
A83: n1-'2*i = n1- 2*i & n1+1-'2*i = n1+1-2*i by A79,A80,XREAL_1:233;
n1+1-'2*i = 1+ (n1-'2*i) by A83;
then
A84: a |^ (n1+1-'2*i) = a * a |^ (n1-'2*i) by NEWTON:6;
(a*Fy0).i = a*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1)
by A81,A82,VALUED_1:6
.= (n choose (2*i-'1)) * a |^ (n1+1-'2*i) * A |^ i1 by A84;
hence thesis by A70,A65;
end;
suppose
A85: i > k;
then i1 >=k by A65,NAT_1:13;
then
A86: 2*i1+1 > n by NAT_1:13,A60,XREAL_1:66;
i >= k1 by A85,NAT_1:13;
then 2*i >= 2*k1 by XREAL_1:66;
then 2*i = 2*k1 by A60,A66,XXREAL_0:1;
then Fy0.i = 0 by A8,A61;
then
A87: (a*Fy0).i=a*0 by VALUED_1:6;
n choose (2*i1+1)=0 by A86,NEWTON:def 3;
hence thesis by A87;
end;
end;
thus FY.i = (FxA.i) + (aFy0.i) by RVSUM_1:11
.= ((n choose (2*i1))+
(n choose (2*i1+1))) * a |^ (n1+1-'2*i) * A |^ i1 by A71,A77
.= (n1 choose (2*i-'1)) * a |^ (n1+1-'2*i) * A |^ i1
by A70,A65,NEWTON:22;
end;
Sum FX = Sum AFx + Sum AFy by RVSUM_1:89
.= Sum (a*Fx) + Sum (A*Fy);
hence a|^n1 + Sum FX = Px(a,n1) by A12,A13;
len (AFx + AFy) = k by CARD_1:def 7;
hence len FX = [\ n1/2 /] by A60,Lm1;
thus for i be Nat st 1 <= i <= n1/2 holds
FX.i = (n1 choose (2*i)) * a |^ (n1-'2*i) * A |^ i
proof
let i be Nat such that
A88: 1 <= i <= n1/2;
set i1=i-'1;
i1 +1 = i by A88,XREAL_1:235;
then
A89: A* A |^ i1 = A |^ i by NEWTON:6;
Fy.i = (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1 by A9,A88;
then
A90: (A*Fy).i = A*((n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i1)
by VALUED_1:6
.= (n choose (2*i-'1)) * a |^ (n1-'2*i) * A |^ i by A89;
A91: 2*i <= n1 by A88,XREAL_1:83;
then
A92: n1-'2*i=n1-2*i by XREAL_1:233;
A93: 2*i < n1 by A91,A60,XXREAL_0:1;
then
A94: 2*i <= n by NAT_1:13;
A95: i <= n/2 by A93,NAT_1:13, XREAL_1:77;
A96: n-'2*i = n- 2*i by A94,XREAL_1:233;
n1-'2*i = 1+ (n-'2*i) by A96,A92;
then
A97: a |^ (n1-'2*i) = a * a |^ (n-'2*i) by NEWTON:6;
A98: (a*Fx).i = a * (Fx.i) by VALUED_1:6
.= a*((n choose (2*i)) * a |^ (n-'2*i) * A |^ i) by A95,A11,A88
.= (n choose (2*i)) * a |^ (n1-'2*i) * A |^ i by A97;
A99: 2*i-'1+1 =2*i by XREAL_1:235,NAT_1:14,A88;
thus FX.i = (AFx).i + (AFy).i by RVSUM_1:11
.= ((n choose (2*i-'1))+(n choose (2*i)))* a |^ (n1-'2*i) * A |^ i
by A90,A98
.= (n1 choose (2*i))* a |^ (n1-'2*i) * A |^ i by A99,NEWTON:22;
end;
end;
end;
for n holds P[n] from NAT_1:sch 2(A1,A7);
hence thesis;
end;
begin :: Solutions of Pell's Equation - Inequalities
theorem Th13:
k <= n implies Px(a,k) <= Px(a,n)
proof
assume k <=n;
then reconsider nk=n-k as Nat by NAT_1:21;
defpred P[Nat] means Px(a,k) <= Px(a,k+$1);
A1: P[0];
A2: for i be Nat holds P[i] implies P[i+1]
proof
let i be Nat;
assume
A3: P[i];
A4: Px(a,k+i+1) = Px(a,k+i)*a+Py(a,k+i)*(a^2-'1) by Th9;
a >=2 by NAT_2:29;
then a >= 1 by XXREAL_0:2;
then Px(a,k+i)*a >= Px(a,k+i)*1 by XREAL_1:64;
then Px(a,k+i+1) >= Px(a,k+i)*1+0 by A4,XREAL_1:7;
hence thesis by A3,XXREAL_0:2;
end;
P[n1] from NAT_1:sch 2(A1,A2);
then P[nk];
hence thesis;
end;
registration
let a,k;
cluster Px(a,k)-> positive;
coherence
proof
Px(a,0) = 1 & Px(a,0) <= Px(a,k) by Th6,Th13;
hence thesis;
end;
end;
theorem Th14:
k < n implies Py(a,k) < Py(a,n)
proof
assume
A1: k <n;
then reconsider nk=n-k as Nat by NAT_1:21;
A2: nk <>0 by A1;
defpred P[Nat] means $1 > 0 implies Py(a,k) < Py(a,k+$1);
A3: P[0];
A4: for i be Nat holds P[i] implies P[i+1]
proof
let i be Nat;
assume
A5: P[i];
A6: Py(a,k+i+1) = Py(a,k+i)*a+Px(a,k+i) by Th9;
a >=2 by NAT_2:29;
then a >= 1 by XXREAL_0:2;
then Py(a,k+i)*a >= Py(a,k+i)*1 by XREAL_1:64;
then
A7: Py(a,k+i+1) > Py(a,k+i)*1+0 by A6,XREAL_1:8;
i = 0 or i >0;
hence thesis by A7,A5,XXREAL_0:2;
end;
P[n1] from NAT_1:sch 2(A3,A4);
then P[nk];
hence thesis by A2;
end;
theorem Th15:
Py(a,k) = Py(a,n) implies k = n
proof
assume Py(a,k) = Py(a,n);
then k >= n >= k by Th14;
hence thesis by XXREAL_0:1;
end;
theorem Th16:
Py(a,n) >= n
proof
defpred P[Nat] means Py(a,$1) >= $1;
A1:P[0];
A2:P[k] implies P[k+1]
proof
k+1 > k by NAT_1:13;
then
A3: Py(a,k)+1 <= Py(a,k+1) by Th14,NAT_1:13;
assume P[k];
then k+1 <= Py(a,k)+1 by XREAL_1:6;
hence thesis by A3,XXREAL_0:2;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm4:Py(a,k) = 0 implies k=0
proof
assume Py(a,k) = 0;
then Py(a,k) = Py(a,0) by Th6;
hence thesis by Th15;
end;
registration
let a;
let k be non zero Nat;
cluster Py(a,k) -> non zero;
coherence by Lm4;
end;
registration
let a be non trivial Nat;
let x be positive Nat;
cluster a*x -> non trivial;
coherence
proof
a >= 2 & x >= 1 by NAT_1:14,NAT_2:29;
then a*x >= 2*1 by XREAL_1:66;
then a*x <>1;
hence thesis by NAT_2:28;
end;
end;
theorem Th17:
a <> 2 & k <= n implies 2 * Py(a,k) < Px(a,n)
proof
set A=a^2-'1,S = sqrt A;
A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233;
assume
A2: a<>2 & k <=n;
Px(a,k)^2 - (a^2-'1) *Py(a,k)^2 =1 by Th10;then
A3: A*(Py(a,k))^2+1 = Px(a,k)^2;
a >=2+1 by A2,NAT_1:22,NAT_2:29;
then a^2 >= 3*3 by XREAL_1:66;
then A >= 9-1 by A1,XREAL_1:9;
then A >= 4 by XXREAL_0:2;
then 4*(Py(a,k))^2 <= A*(Py(a,k))^2 by XREAL_1:64;
then (2*Py(a,k))^2 < Px(a,k)^2 by A3,NAT_1:13;
then
A4: 2 * Py(a,k) < Px(a,k) by SQUARE_1:15;
Px(a,k)<=Px(a,n) by A2,Th13;
hence thesis by A4,XXREAL_0:2;
end;
theorem Th18:
a = 2 & k <= n implies (sqrt 3) * Py(a,k) < Px(a,n)
proof
set A=a^2-'1,S = sqrt A;
A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233;
assume
A2: a = 2 & k <=n;
Px(a,k)^2 - (a^2-'1) *Py(a,k)^2 =1 by Th10;then
A*(Py(a,k))^2+1 = Px(a,k)^2;
then
A3: 3*(Py(a,k))^2 < Px(a,k)^2 by A1,A2,NAT_1:13;
3* Py(a,k)^2 = (sqrt 3)^2 * Py(a,k)^2 by SQUARE_1:def 2
.= ((sqrt 3)* Py(a,k))^2;
then
A4: (sqrt 3)* Py(a,k) < Px(a,k) by A3,SQUARE_1:15;
Px(a,k)<=Px(a,n) by A2,Th13;
hence thesis by A4,XXREAL_0:2;
end;
theorem Th19:
a = 2 & k < n implies (3 + 2*sqrt 3) * Py(a,k) < Px(a,n)
proof
A1:(sqrt 3)^2 = 3 & sqrt 3 >= 0 by SQUARE_1:def 2;
set A=a^2-'1,S = sqrt A;
assume
A2: a = 2 & k <n;
then
A3: k+1 <= n by NAT_1:13;
Py(a,k+1) = Px(a,k) + Py(a,k) * a by Th9;
then
A4: (sqrt 3) *(Px(a,k) + Py(a,k) * 2) < Px(a,n) by A3,A2,Th18;
(sqrt 3) * Py(a,k) <= Px(a,k) by A2,Th18;
then
A5: (sqrt 3) * Py(a,k)*(sqrt 3) <= Px(a,k)* (sqrt 3) by A1,XREAL_1:64;
A6: (sqrt 3) * Py(a,k)*(sqrt 3) = (sqrt 3) *(sqrt 3) * Py(a,k)
.= 3*Py(a,k) by A1;
(sqrt 3) *(Px(a,k) + Py(a,k) * 2) = Py(a,k) * (2*sqrt 3) + Px(a,k)* (sqrt 3);
then (sqrt 3) *(Px(a,k) + Py(a,k) * 2) >= Py(a,k) * (2*sqrt 3) + 3*Py(a,k)
by A5,A6,XREAL_1:7;
hence thesis by A4,XXREAL_0:2;
end;
theorem Th20:
(2*a-1)|^n *(a-1) <= Px(a,n+1) <= a * (2*a) |^ n &
(2*a-1)|^n <= Py(a,n+1) <= (2*a) |^ n
proof
defpred P[Nat] means
(2*a-1)|^$1 <= Py(a,$1+1) <= (2*a) |^ $1 &
(2*a-1)|^$1 *(a-1) <= Px(a,$1+1) <= a * (2*a) |^ $1;
A1: a^2-'1 = a^2-1 by XREAL_1:233,NAT_1:14;
A2: (2*a-1)|^0 = 1 & (2*a) |^ 0 =1 by NEWTON:4;
A3: a-1 <= a-0 by XREAL_1:10;
Py(a,0) = 0 & Px(a,0)= 1 by Th6;
then Py(a,1+0) = 1+0*a & Px(a,1+0) = 1*a+ 0*(a^2-'1) by Th9;
then
A4: P[0] by A2,A3;
A5: P[k] implies P[k+1]
proof
set k1=k+1;
assume
A6: P[k];
A7: Py(a,k1+1) = Px(a,k1) + Py(a,k1)*a &
Px(a,k1+1) = Px(a,k1)*a + Py(a,k1)*(a^2-'1) by Th9;
A8: Py(a,k1)*a <= (2*a) |^ k*a by A6,XREAL_1:64;
A9: (2*a) |^ k*a + (2*a) |^ k*a = (2*a) |^ k*(2*a)
.= (2*a) |^ k1 by NEWTON:6;
A10: Py(a,k1)*a >= (2*a-1)|^k*a by A6,XREAL_1:64;
A11: (2*a-1)|^k *(a-1) + (2*a-1)|^k*a = (2*a-1)|^k *(2*a-1)
.= (2*a-1)|^k1 by NEWTON:6;
Px(a,k1)*a <= a * (2*a) |^ k *a & Py(a,k1)*(a^2-'1)
<= (2*a) |^ k * (a^2-'1) by A6,XREAL_1:64;
then
A12: Px(a,k1+1) <= a * (2*a) |^ k *a + (2*a) |^ k * (a^2-'1) by A7,XREAL_1:7;
a^2 +a^2-1 <= a^2+a^2-0 by XREAL_1:10;
then
A13: (2*a) |^ k * (a^2 +a^2-1) <= (2*a) |^ k * (a^2 +a^2) by XREAL_1:64;
(2*a-1)|^k * (a^2-'1) <= Py(a,k1)*(a^2-'1) &
(2*a-1)|^k *(a-1)*a <= Px(a,k1)*a by A6,XREAL_1:64;
then
A14: (2*a-1)|^k * (a^2-'1) + (2*a-1)|^k *(a-1)*a <= Px(a,k1+1)
by A7,XREAL_1:7;
2*1 <= 2*a by XREAL_1:64,NAT_1:14;
then 1--1 <= 2*a;
then 2*a^2-a+(1-2*a) <= 2*a^2-a+-1 by XREAL_1:6,12;
then (2*a-1)|^k * ((2*a-1)*(a-1)) <= (2*a-1)|^k * (a^2-1 + (a-1)*a)
by XREAL_1:64;
hence thesis by A8,A7,A6,XREAL_1:7,A9,A10,A11,A1,A13,A12,XXREAL_0:2,A14;
end;
P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
theorem Th21:
for x be positive Nat holds
x|^n * (1-1/(2*a*x)) |^ n
<= Py(a*x,n+1)/Py(a,n+1)
<= (x|^n) * (1 / (1-1/(2*a))|^n)
proof
let x be positive Nat; set z=n;
1-1/(2*a*x) = (2*a*x)/(2*a*x)-1/(2*a*x) by XCMPLX_1:60
.= (2*a*x-1)/(2*a*x) by XCMPLX_1:120;
then x *(1-1/(2*a*x)) = (2*a*x-1)/(2*a) by XCMPLX_1:92;
then
A1: x|^z * (1-1/(2*a*x)) |^ z = ((2*a*x-1)/(2*a)) to_power z by NEWTON:7
.= ((2*a*x-1) to_power z) / ((2*a) to_power z) by POWER:31;
A2: (2*a-1)|^z <= Py(a,z+1) <= (2*a) |^ z by Th20;
A3: (2*(a*x)-1)|^z <= Py(a*x,z+1) <= (2*(a*x)) |^ z by Th20;
((2*a*x-1)|^z)*Py(a,z+1) <=Py(a*x,z+1)*((2*a) |^ z) by A2,A3,XREAL_1:66;
hence x|^z * (1-1/(2*a*x)) |^ z <= Py(a*x,z+1)/Py(a,z+1) by A1,XREAL_1:102;
a>=1 by NAT_1:14;
then a+a >= 1+1 by XREAL_1:7;
then 1*(2*a) > 1 by NAT_1:13;
then 1 > 1/(2*a) by XREAL_1:83;
then
A4: 1 - 1/(2*a) >1/(2*a)-1/(2*a) by XREAL_1:14;
A5: Py(a*x,z+1)*((2*a-1) |^ z)<= ((2*a*x) |^ z)*Py(a,z+1) by A2,A3,XREAL_1:66;
(2*a)/(2*a)=1 by XCMPLX_1:60;
then (2*a-1)/(2*a) = 1 - (1/(2*a)) by XCMPLX_1:120;
then (2*a)/(2*a-1) = 1 / (1 - (1/(2*a))) by XCMPLX_1:57;
then (2*a*x)/(2*a-1)= x* (1 / (1 - (1/(2*a)))) by XCMPLX_1:74;
then (2*a*x)/(2*a-1)= (x*1) / (1 - 1/(2*a)) by XCMPLX_1:74;
then ((2*a*x) to_power z) / ((2*a-1) to_power z) =
(x / (1 - 1/(2*a))) to_power z by POWER:31
.= (1*(x to_power z)) / ((1 - 1/(2*a)) to_power z) by A4,POWER:31
.= (x|^z) * (1 / (1-1/(2*a))|^z) by XCMPLX_1:74;
hence thesis by A5,XREAL_1:102;
end;
Lm5: 0 <= 1-r <= 1 implies (1-r) |^ n >= 1-n*r
proof
defpred P[Nat] means 1-$1*r >=0 implies (1-r) |^ $1 >= 1 - $1 * r;
assume
A1: 0 <= 1-r <=1;
1-0=1;
then
A2: r >=0 by A1,XREAL_1:10;
A3: P[0] by NEWTON:4;
A4: P[k] implies P[k+1]
proof
assume
A5: P[k];
A6: (1-r) |^ (k+1) = (1-r) * (1-r) |^ k by NEWTON:6;
assume 1-(k+1)*r >=0;
then 1-k*r-r+r >= 0+r by XREAL_1:6;
then 1-k*r >= 0;
then
A7: (1-r) |^ (k+1) >= (1-r)* (1-k*r) by A5,A6,A1,XREAL_1:66;
1-k*r -r +r*r*k >= 1-k*r -r+0 by A2,XREAL_1:7;
hence thesis by A7,XXREAL_0:2;
end;
A8: P[k] from NAT_1:sch 2(A3,A4);
1-n*r>=0 or 1-n*r<0;
hence thesis by A8,A1;
end;
theorem Th22:
for x be positive Nat st a > 2*n*(x|^n) holds
x|^n - 1/2 < Py(a*x,n+1)/Py(a,n+1) < x|^n + 1/2
proof
let x be positive Nat;
A1: x|^n * (1-1/(2*a*x)) |^ n
<= Py(a*x,n+1)/Py(a,n+1)<= (x|^n) * (1 / (1-1/(2*a))|^n) by Th21;
assume
A2: a > 2*n*(x|^n);
A3: 1- n*(1/(2*a)) = 1- ((n*1)/(2*a)) by XCMPLX_1:74;
2*(x|^n)*n >= 1*n by XREAL_1:64,NAT_1:14;
then a >= n by A2,XXREAL_0:2;
then a-n >=n-n by XREAL_1:9;
then
A4: a-n+a >= a+0 by XREAL_1:6;
then n / (2*a -n)<= n/a by XREAL_1:118;
then 1 + n/(2*a -n) <= 1+n/a by XREAL_1:6;
then
A5: (x |^ n) * (1 + n/(2*a -n)) <= (x|^n) * (1+n/a) by XREAL_1:64;
A6: 2*a - n >0 by A4;
A7: 1/1>=1/(2*a) by XREAL_1:118,NAT_1:14;
2*a >n by A6,XREAL_1:47;
then n/(2*a)<1 by XREAL_1:191;
then
A8: 1- (n/(2*a)) >1-1 by XREAL_1:10;
1-1<=1-1/(2*a)<=1-0 by A7,XREAL_1:10;
then (1-1/(2*a))|^n >= 1- (n/(2*a)) by Lm5,A3;
then 1/ ((1-1/(2*a))|^n) <= 1 / (1- (n/(2*a))) by A8,XREAL_1:118;
then
A9: x|^n * (1/((1-1/(2*a))|^n)) <= x|^n * (1/(1- (n/(2*a)))) by XREAL_1:64;
1- (n/(2*a)) = (2*a)/(2*a) - (n/(2*a)) by XCMPLX_1:60
.= (2*a -n)/(2*a) by XCMPLX_1:120; then
A10: 1/(1- (n/(2*a))) = (2*a-n+n) / (2*a -n) by XCMPLX_1:57
.= (2*a -n)/(2*a -n) + n/(2*a -n) by XCMPLX_1:62
.= 1 + n/(2*a -n) by XCMPLX_1:60,A4;
A11: x|^n * (1/((1-1/(2*a))|^n)) <= x|^n * (1+n/a) by A5,A9,A10,XXREAL_0:2;
2*n*(x|^n) = 2*(n*(x|^n));
then n*(x|^n) < a/2 by A2,XREAL_1:81;
then n*(x|^n) < 1/2*a;
then (n * (x|^n))/a < 1/2 by XREAL_1:83;
then (n/a) * (x|^n) < 1/2 by XCMPLX_1:74;
then (x|^n) + (x|^n) * (n/a) < x|^n + 1/2 by XREAL_1:6;
then
A12: x|^n * (1 / (1-1/(2*a))|^n) < x|^n + 1/2 by A11,XXREAL_0:2;
1 >= 1/(2*a*x) by XREAL_1:185,NAT_1:14;
then 1-1<= 1-1/(2*a*x) <=1-0 by XREAL_1:10;
then
A13: x|^n * (1-1/(2*a*x)) |^ n >= x|^n * (1 - n*(1/(2*a*x)))
by Lm5,XREAL_1:64;
(x|^n)*(n*(1/(2*a*x)))*2 = (x|^n)*((n*1)/(2*a*x))*2 by XCMPLX_1:74
.= ((x|^n)*2)*(n/(2*a*x))
.= (x|^n *2*n) /(2*a*x) by XCMPLX_1:74;
then
A14: (x|^n)*(n*(1/(2*a*x)))*2 < a / (2*a*x) by A2,XREAL_1:74;
2*x*a >= 1*a by XREAL_1:64,NAT_1:14;
then a / (2*a*x) <= 1 by XREAL_1:183;
then (x|^n)*(n*(1/(2*a*x)))*2 < 1 by A14,XXREAL_0:2;
then (x|^n)*(n*(1/(2*a*x))) < 1/2 by XREAL_1:81;
then x|^n - (x|^n)*(n*(1/(2*a*x))) > x|^n -1/2 by XREAL_1:15;
then x|^n * (1-1/(2*a*x)) |^ n > (x|^n -1/2) by A13,XXREAL_0:2;
hence thesis by A12,A1,XXREAL_0:2;
end;
begin :: Solutions of Pell's Equation - Equality
theorem Th23:
x >=0 implies sgn(x)*Py(a,|.x.|) = Py(a,|.x.|)
proof
assume x>=0;
then x=0 or x >0;
then sgn(x) =1 or (sgn(x)=0 & x=0) by ABSVALUE:def 2;
hence thesis by Th6;
end;
theorem Th24:
x <= 0 implies sgn(x)*Py(a,|.x.|) = -Py(a,|.x.|)
proof
A1: Py(a,|.0.|)=0 by Th6;
assume x<=0;
then x=0 or x <0;
then sgn(x) = -1 or (sgn(x)=0 & x=0 ) by ABSVALUE:def 2;
hence thesis by A1;
end;
theorem Th25:
Px(a,|.x+y.|) = Px(a,|.x.|)*Px(a,|.y.|) +
(a^2-'1) * sgn(x)*Py(a,|.x.|)*sgn(y)*Py(a,|.y.|) &
sgn(x+y)*Py(a,|.x+y.|) = Px(a,|.x.|)*sgn(y)*Py(a,|.y.|) +
sgn(x)*Py(a,|.x.|)*Px(a,|.y.|)
proof
set i=x,j=y,I=|.x.|,J=|.y.|,IJ = |.x+y.|;
set A=a^2-'1,S = sqrt A;
A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233;
A2: S^2= A by SQUARE_1:def 2;
A3: 1 = ((a + S)*(a - S)) |^I by A2,A1
.= ((a + S) |^I)*((a - S) |^I) by NEWTON:7;
A4: 1 = ((a + S)*(a - S)) |^J by A2,A1
.= ((a + S) |^J)*((a - S) |^J) by NEWTON:7;
deffunc PX(Integer) = Px(a,|.$1.|);
deffunc PY(Integer) = sgn($1)*Py(a,|.$1.|);
per cases;
suppose
A5: i>=0 & j >=0;
then
A6: i = I & j=J by ABSVALUE:def 1;
A7: PY(i) = Py(a,I) by Th23,A5;
A8: PY(j) = Py(a,J) by A5,Th23;
A9: IJ=i+j by A5,ABSVALUE:def 1;
PY(i+j) = Py(a,IJ) by Th23,A5;
then PX(i+j) + PY(i+j) * S = (a+ S) |^ IJ by Th11
.= ((a+ S) |^ I) * ((a+ S) |^ J) by A6,A9,NEWTON:8
.= (PX(i) + PY(i) * S) * ((a+ S) |^ J) by A7,Th11
.= (PX(i) + PY(i) * S) * (PX(j) + PY(j) * S) by A8,Th11
.= PX(i)*PX(j) + A * PY(i)*PY(j) +
S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2;
hence thesis by PELLS_EQ:3;
end;
suppose
A10: i <0 & j >=0;
then
A11: -i = I & j=J by ABSVALUE:def 1;
A12: PY(i) = -Py(a,I) by A10,Th24;
A13: PY(j) = Py(a,J) by A10,Th23;
per cases;
suppose
A14: i+j>=0;
then IJ=i+j by ABSVALUE:def 1;
then
A15: IJ+I = J by A11;
PY(i+j) = Py(a,IJ) by A14,Th23;
then PX(i+j) + PY(i+j) * S = ((a+ S) |^ IJ) *
(((a + S) |^I)*((a - S) |^I)) by Th11,A3
.= ((a+ S) |^ IJ) * ((a + S) |^I)* ((a - S) |^I)
.= ((a+ S) |^ J)* ((a - S) |^I) by A15,NEWTON:8
.= (PX(j) + PY(j) * S)* ((a - S) |^I) by A13,Th11
.= (PX(j) + PY(j) * S)* (PX(i) + PY(i)*S) by A12,Th11
.= PX(i)*PX(j) + A * PY(i)*PY(j) +
S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2;
hence thesis by PELLS_EQ:3;
end;
suppose
A16:i+j <0;
then IJ=-(i+j) by ABSVALUE:def 1;
then
A17: IJ+J = I by A11;
PY(i+j) = -Py(a,IJ) by A16,Th24;
then PX(i+j) + PY(i+j) * S
= ((a- S) |^ IJ) * (((a + S) |^J)*((a - S) |^J)) by Th11,A4
.= ((a- S) |^ IJ) * ((a - S) |^J)* ((a + S) |^J)
.= ((a- S) |^ I)* ((a + S) |^J) by A17,NEWTON:8
.= (PX(i) + PY(i) * S)* ((a + S) |^J) by A12,Th11
.= (PX(i) + PY(i) * S)* (PX(j) + PY(j)*S) by A13,Th11
.= PX(i)*PX(j) + A * PY(i)*PY(j) +
S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2;
hence thesis by PELLS_EQ:3;
end;
end;
suppose
A18: i >=0 & j <0;
then
A19: i = I & -j=J by ABSVALUE:def 1;
A20: PY(i) = Py(a,I) by Th23,A18;
A21: PY(j) = -Py(a,J) by A18,Th24;
per cases;
suppose
A22: i+j>=0;
then IJ=i+j by ABSVALUE:def 1;
then
A23: IJ+J = I by A19;
PY(i+j) = Py(a,IJ) by A22,Th23;
then PX(i+j) + PY(i+j) * S =
((a+ S) |^ IJ) * (((a + S) |^J)*((a - S) |^J)) by A4,Th11
.= ((a+ S) |^ IJ) * ((a + S) |^J)* ((a - S) |^J)
.= ((a+ S) |^ I)* ((a - S) |^J) by A23,NEWTON:8
.= (PX(i) + PY(i) * S)* ((a - S) |^J) by A20,Th11
.= (PX(i) + PY(i) * S)* (PX(j) + PY(j)*S) by A21,Th11
.= PX(i)*PX(j) + A * PY(i)*PY(j) +
S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2;
hence thesis by PELLS_EQ:3;
end;
suppose
A24:i+j <0;
then IJ=-(i+j) by ABSVALUE:def 1;
then
A25: IJ+I = J by A19;
PY(i+j) = -Py(a,IJ) by A24,Th24;
then PX(i+j) + PY(i+j) * S =
((a- S) |^ IJ) * (((a - S) |^I)*((a + S) |^I)) by Th11,A3
.= ((a- S) |^ IJ) * ((a - S) |^I)* ((a + S) |^I)
.= ((a- S) |^ J)* ((a + S) |^I) by A25,NEWTON:8
.= (PX(j) + PY(j) * S)* ((a + S) |^I) by A21,Th11
.= (PX(j) + PY(j) * S)* (PX(i) + PY(i)*S) by A20,Th11
.= PX(i)*PX(j) + A * PY(i)*PY(j) +
S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2;
hence thesis by PELLS_EQ:3;
end;
end;
suppose
A26: i<0 & j <0;
then
A27: -i = I & -j=J by ABSVALUE:def 1;
A28: PY(i) = -Py(a,I) by A26,Th24;
A29: PY(j) = -Py(a,J) by A26,Th24;
A30: IJ=-(i+j) by A26,ABSVALUE:def 1;
A31: IJ = I+J by A27,A30;
PX(i+j) + PY(i+j) * S = PX(i+j) + (-Py(a,IJ)) * S by A26,Th24
.= (a- S) |^ IJ by Th11
.= ((a- S) |^ I) * ((a- S) |^ J) by A31,NEWTON:8
.= (PX(i) + PY(i) * S) * ((a- S) |^ J) by A28,Th11
.= (PX(i) + PY(i) * S) * (PX(j) + PY(j) * S) by A29,Th11
.= PX(i)*PX(j) + A * PY(i)*PY(j) +
S* (PX(i)*PY(j) + PY(i)*PX(j)) by A2;
hence thesis by PELLS_EQ:3;
end;
end;
begin :: Solutions of Pell's Equation - Congruences
theorem Th26:
Px(a,n),Py(a,n) are_coprime
proof
defpred P[Nat] means Px(a,$1) gcd Py(a,$1)=1;
Px(a,0) =1 & Py(a,0)=0 by Th6;
then
A1: P[0];
A2: for n st P[n] holds P[n+1]
proof
set A=a^2-'1;
A3: A = a^2 -1 by NAT_1:14,XREAL_1:233;
let n such that
A4: P[n];
A5: Px(a,n+1) = Px(a,n)*a + Py(a,n)*A&
Py(a,n+1) = Px(a,n) + Py(a,n) * a by Th9;
thus 1 = (Px(a,n) + Py(a,n) * a) gcd Py(a,n) by A4,EULER_1:8
.= Py(a,n+1) gcd -Py(a,n) by A5, NEWTON02:1
.= (-Py(a,n) + a* Py(a,n+1)) gcd Py(a,n+1) by NEWTON02:5
.= Px(a,n+1) gcd Py(a,n+1) by A3,A5;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
then Px(a,n) gcd Py(a,n)=1;
hence thesis by INT_2:def 3;
end;
theorem Th27:
Py(a,n),n are_congruent_mod (a-1)
proof
set A=a-1;
A1: a^2 -'1 = a^2 -1 by NAT_1:14,XREAL_1:233;
consider Fy,Fx be FinSequence of NAT such that
A2:Sum Fy = Py(a,n) & len Fy = [\ (n+1)/2 /] and
A3:for i be Nat st 1 <= i <= (n+1)/2 holds
Fy.i = (n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a^2-'1) |^ (i-'1) and
a|^n + Sum Fx = Px(a,n) & len Fx = [\ n/2 /] &
for i be Nat st 1 <= i <= n/2 holds
Fx.i = (n choose (2*i)) * a |^ (n-'2*i) * (a^2-'1) |^ i by Th12;
per cases;
suppose
A4: n=0;
then Py(a,n) = 0 by Th6;
hence thesis by A4,INT_1:11;
end;
suppose
A5: n <> 0;
for i be Nat st 1 < i <= len Fy holds (Fy.i) mod A = 0
proof
let i be Nat such that
A6: 1 < i <= len Fy;
i -'1 = i-1 by A6,XREAL_1:233;
then i-'1 <> 0 by A6;
then reconsider ii= i-'1-1 as Element of NAT by NAT_1:20;
i-'1 = ii+1;
then
A7: (a^2-'1) |^ (i-'1) = A* (a+1) * ((a^2-'1) |^ ii) by A1,NEWTON:6;
[\ (n+1)/2 /]<=(n+1)/2 by INT_1:def 6;then
i <= (n+1)/2 by A2,A6,XXREAL_0:2;
then Fy.i = (n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a^2-'1) |^ (i-'1)
by A6,A3
.=(n choose (2*i-'1)) * a |^ (n+1-'2*i) * (a+1) * ((a^2-'1) |^ ii) *A
by A7;
then A divides Fy.i by INT_1:def 3;
hence thesis by INT_1:62;
end;
then Py(a,n) mod A = Fy.1 mod A by Th1,A2;
then (Py(a,n) - Fy.1) mod A =0 by INT_4:22;
then A divides Py(a,n)-Fy.1 by INT_1:62;
then
A8: Py(a,n),Fy.1 are_congruent_mod A by INT_1:def 4;
n >=1 by A5,NAT_1:14;
then n+1 >= 1+1 & 1+1=2*1 by XREAL_1:7;
then
A9: (n+1)/2>=1 by XREAL_1:77;
1-'1=1-1 by XREAL_1:233;
then
A10: (a^2-'1) |^ (1-'1) = 1 by NEWTON:4;
2*1-'1 = 2-1 by XREAL_1:233;
then
A11: n choose (2*1-'1) = n by A5,NAT_1:14,NEWTON:23;
A12: Fy.1 = n * (a |^ (n+1-'2*1)) *1 by A9,A10,A11,A3;
A13: A >= 2-1 by NAT_2:29,XREAL_1:9;
per cases by A13,XXREAL_0:1;
suppose A=1;
then A * (Py(a,n)- n) = Py(a,n)- n;
hence thesis by INT_1:def 5;
end;
suppose
A14: A >1;
a = A*1+1;
then a mod A =1 mod A by PEPIN:10
.= 1 by A14,PEPIN:5;
then a |^ (n+1-'2*1) mod A = 1 by A14,PEPIN:35;
then a |^ (n+1-'2*1),1 are_congruent_mod A by A14,PEPIN:39;
then Fy.1,1*n are_congruent_mod A by A12,INT_4:11;
hence thesis by A8,INT_1:15;
end;
end;
end;
theorem Th28:
Px(a,n),Px(b,n) are_congruent_mod (a-b) &
Py(a,n),Py(b,n) are_congruent_mod (a-b)
proof
defpred P[Nat] means Px(a,$1),Px(b,$1) are_congruent_mod (a-b) &
Py(a,$1),Py(b,$1) are_congruent_mod (a-b);
Px(a,0) = 1 = Px(b,0) &
Py(a,0) = 0 = Py(b,0) by Th6;
then
A1: P[0] by INT_1:11;
A2: for n st P[n] holds P[n+1]
proof
set A=a^2-'1,B= b^2-'1;
A = a^2 -1 & B = b^2-1 by NAT_1:14,XREAL_1:233;
then A-B = (a-b)*(a+b);
then
A3: A,B are_congruent_mod (a-b) by INT_1:def 5;
a-b = 1*(a-b);
then
A4: a,b are_congruent_mod (a-b) by INT_1:def 5;
let n such that
A5: P[n];
A6: Px(a,n+1) = Px(a,n)*a + Py(a,n)*A &
Px(b,n+1) = Px(b,n)*b + Py(b,n)*B by Th9;
A7: Py(a,n)*A,Py(b,n)*B are_congruent_mod (a-b) by A5,A3,INT_1:18;
Px(a,n)*a,Px(b,n)*b are_congruent_mod (a-b) by A5,A4,INT_1:18;
hence Px(a,n+1),Px(b,n+1) are_congruent_mod (a-b) by A6,A7,INT_1:16;
A8: Py(a,n+1) = Px(a,n) + Py(a,n)*a& Py(b,n+1) = Px(b,n) + Py(b,n)*b by Th9;
Py(a,n)*a,Py(b,n)*b are_congruent_mod (a-b) by A4,A5,INT_1:18;
hence Py(a,n+1),Py(b,n+1) are_congruent_mod (a-b) by A8,A5,INT_1:16;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th29:
a,b are_congruent_mod k implies Py(a,n),Py(b,n) are_congruent_mod k
proof
assume a,b are_congruent_mod k;
then consider x be Integer such that
A1: k*x = a-b by INT_1:def 5;
consider p be Integer such that
A2: (a-b)*p = Py(a,n)-Py(b,n) by Th28,INT_1:def 5;
p*(a-b) = p*(x*k) by A1
.= p*x*k;
hence thesis by A2, INT_1:def 5;
end;
Lm6:sgn(x)*sgn(x)*Py(a,|.x.|)=Py(a,|.x.|)
proof
per cases;
suppose
A1: x >= 0;
thus sgn(x)*sgn(x)*Py(a,|.x.|)=sgn(x)*(sgn(x)*Py(a,|.x.|))
.= sgn(x)*Py(a,|.x.|) by A1,Th23
.= Py(a,|.x.|) by A1,Th23;
end;
suppose
A2: x <= 0;
thus sgn(x)*sgn(x)*Py(a,|.x.|)=sgn(x)*(sgn(x)*Py(a,|.x.|))
.= sgn(x)*(-Py(a,|.x.|)) by A2,Th24
.= -(sgn(x)*Py(a,|.x.|))
.= --Py(a,|.x.|) by A2,Th24
.= Py(a,|.x.|);
end;
end;
theorem Th30:
sgn(2*x+y)*Py(a,|.2*x+y.|),-sgn(y)*Py(a,|.y.|)
are_congruent_mod Px(a,|.x.|)
proof
set i=x,j=y,A=a^2-'1;
2*i+j = i+(i+j);
then sgn(2*i+j)*Py(a,|.2*i+j.|) = Px(a,|.i.|)*sgn(i+j)*Py(a,|.i+j.|) +
sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|) by Th25;
then sgn(2*i+j)*Py(a,|.2*i+j.|) - sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|) =
Px(a,|.i.|)*(sgn(i+j)*Py(a,|.i+j.|));
then
A1: sgn(2*i+j)*Py(a,|.2*i+j.|), sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|)
are_congruent_mod Px(a,|.i.|) by INT_1:def 5;
A2:sgn(i)*Py(a,|.i.|)*(A * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|)) =
(sgn(i)*sgn(i)*Py(a,|.i.|))*(a^2-'1)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|)
.= Py(a,|.i.|) * A*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) by Lm6;
A3: Px(a,|.i.|)^2 - (a^2-'1) *Py(a,|.i.|)^2 =1 by Th10;
Px(a,|.i+j.|) = Px(a,|.i.|)*Px(a,|.j.|) +
(a^2-'1) * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) by Th25;
then Px(a,|.i+j.|)- (a^2-'1) * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) =
Px(a,|.i.|)*Px(a,|.j.|);
then Px(a,|.i+j.|), (a^2-'1) * sgn(i)*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|)
are_congruent_mod Px(a,|.i.|) by INT_1:def 5;
then sgn(i)*Py(a,|.i.|)*Px(a,|.i+j.|),
Py(a,|.i.|)*A*Py(a,|.i.|)*sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|)
by A2,INT_4:11;
then
A4: sgn(2*i+j)*Py(a,|.2*i+j.|),
(Px(a,|.i.|)^2-1)*sgn(j)*Py(a,|.j.|) are_congruent_mod Px(a,|.i.|)
by A3,A1,INT_1:15;
(Px(a,|.i.|)^2-1)*sgn(j)*Py(a,|.j.|)-(- sgn(j)*Py(a,|.j.|)) =
Px(a,|.i.|) * (Px(a,|.i.|)*sgn(j)*Py(a,|.j.|));
then (Px(a,|.i.|)^2-1)*sgn(j)*Py(a,|.j.|),- sgn(j)*Py(a,|.j.|)
are_congruent_mod Px(a,|.i.|) by INT_1:def 5;
hence thesis by A4,INT_1:15;
end;
Lm7:
for i,j be Integer holds
sgn(4*i+j)*Py(a,|.4*i+j.|),sgn(j)*Py(a,|.j.|)
are_congruent_mod Px(a,|.i.|)
proof
let i,j be Integer;
4*i+j = 2*i+(2*i+j);
then
A1: sgn(4*i+j)*Py(a,|.4*i+j.|),-sgn(2*i+j)*Py(a,|.2*i+j.|)
are_congruent_mod Px(a,|.i.|) by Th30;
(-1)* (sgn(2*i+j)*Py(a,|.2*i+j.|)), (-1) * (-sgn(j)*Py(a,|.j.|))
are_congruent_mod Px(a,|.i.|) by Th30,INT_4:11;
hence thesis by A1,INT_1:15;
end;
theorem Th31:
sgn(4*x*n+y)*Py(a,|.4*x*n+y.|),sgn(y)*Py(a,|.y.|)
are_congruent_mod Px(a,|.x.|)
proof
defpred P[Nat] means
sgn(4*x*$1+y)*Py(a,|.4*x*$1+y.|),sgn(y)*Py(a,|.y.|)
are_congruent_mod Px(a,|.x.|);
A1: P[0] by INT_1:11;
A2: for n holds P[n] implies P[n+1]
proof let n;set n1=n+1;
assume
A3: P[n];
4*x*n1+y = 4*x + (4*x*n+y);
then sgn(4*x*n1+y)*Py(a,|.4*x*n1+y.|),sgn(4*x*n+y)*Py(a,|.4*x*n+y.|)
are_congruent_mod Px(a,|.x.|) by Lm7;
hence thesis by A3,INT_1:15;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th32:
sgn(x+y)*Py(a,|.x+y.|),sgn(x-y)*Py(a,|.x-y.|)
are_congruent_mod Px(a,|.x.|)
proof
x+y = 2*x+(-x+y);
then
A1: sgn(x+y)*Py(a,|.x+y.|),-sgn(-x+y)*Py(a,|.-x+y.|)
are_congruent_mod Px(a,|.x.|) by Th30;
A2: |. -x+y.|= |.-(-x+y).| by COMPLEX1:52;
-x+y= (-1)*(x-y);
then sgn(-x+y) = sgn(x-y)*sgn(-1) & sgn(-1)=-1 by ABSVALUE:18,def 2;
hence thesis by A2,A1;
end;
Lm8: |.r1.| < r2 implies -r2 < r1 < r2
proof
assume
A1: |.r1.| < r2;
then
A2: -|.r1.| > -r2 by XREAL_1:24;
-|.r1.| <= r1 <= |.r1.| by ABSVALUE:4;
hence thesis by A1,A2,XXREAL_0:2;
end;
theorem Th33:
n1 < n2 <= n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2)
& x,y are_congruent_mod Px(a,n)
implies x = y
proof
assume
A1: n1 < n2 <= n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2)
& x,y are_congruent_mod Px(a,n);
then consider i be Integer such that
A2: x - y = Px(a,n)*i by INT_1:def 5;
A3: n1 < n by A1,XXREAL_0:2;
-Px(a,n) < x-y < Px(a,n)
proof
per cases;
suppose
A4: a=2;
A5: (sqrt 3)^2 = 3 by SQUARE_1:def 2;
A6: sqrt 3 >0 by SQUARE_1:25;
(3 + 2*sqrt 3)*Py(a,n1) < Px(a,n) by A4,A3,Th19;
then Py(a,n1) < Px(a,n) / (3 + 2*sqrt 3) by A6,XREAL_1:81;
then
A7: - Px(a,n) / (3 + 2*sqrt 3) < x < Px(a,n) / (3 + 2*sqrt 3) by Lm8,A1;
(sqrt 3)*Py(a,n2) < Px(a,n) by A4,Th18,A1;
then Py(a,n2) < Px(a,n)/(sqrt 3) by XREAL_1:81,A6;
then -Px(a,n)/(sqrt 3) < y < Px(a,n)/(sqrt 3) by Lm8,A1;
then
A8: - Px(a,n) / (3 + 2*sqrt 3) - Px(a,n)/(sqrt 3)<
x-y < Px(a,n)/(3 + 2*sqrt 3) - - Px(a,n)/(sqrt 3) by A7,XREAL_1:14;
A9: Px(a,n) / (3 + 2*sqrt 3) + Px(a,n)/(sqrt 3) =
(Px(a,n) * (sqrt 3) + Px(a,n) *
(3 + 2*sqrt 3)) / ((3 + 2*sqrt 3)*(sqrt 3)) by XCMPLX_1:116,A6
.= (Px(a,n) * (3 + 3*sqrt 3))/ ((3 + 2*sqrt 3)*(sqrt 3))
.= Px(a,n) * ((3 + 3*sqrt 3)/ (3* (sqrt 3) + 6)) by A5,XCMPLX_1:74;
3 + 3*sqrt 3 <= 6+3* sqrt 3 by XREAL_1:7;
then (3 + 3*sqrt 3)/ (3* (sqrt 3) + 6) <=1 by A6,XREAL_1:183;
then
A10: Px(a,n) * ((3 + 3*sqrt 3)/ (3* (sqrt 3) + 6)) <= Px(a,n)*1
by XREAL_1:64;
then -(Px(a,n) / (3 + 2*sqrt 3) + Px(a,n)/(sqrt 3)) >= -Px(a,n)
by A9, XREAL_1:24;
hence thesis by A10,A8,A9,XXREAL_0:2;
end;
suppose
A11: a<>2;
2*Py(a,n1) < Px(a,n) by A11,A3,Th17;
then |.x.| < Px(a,n)/2 by A1,XREAL_1:81;
then
A12: - Px(a,n)/2 < x < Px(a,n)/2 by Lm8;
2*Py(a,n2) < Px(a,n) by A11,Th17,A1;
then |.y.| < Px(a,n)/2 by A1,XREAL_1:81;
then - Px(a,n)/2 < y < Px(a,n)/2 by Lm8;
then -Px(a,n)/2 -Px(a,n)/2 < x-y < Px(a,n)/2 - -Px(a,n)/2
by A12,XREAL_1:14;
hence thesis;
end;
end;
then (-1)*Px(a,n) < Px(a,n)*i < 1*Px(a,n) by A2;
then -1 < i < 1+0 by XREAL_1:64;
then 0<= i <=0 by INT_1:7,8;
then x - y = 0 by A2;
hence thesis;
end;
Lm9:
n1 < n2 <= 2*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n)
implies n1 = 2*n -n2
proof
assume
A1: n1 < n2 <= 2*n & |.x.| = Py(a,n1) &
|.y.| = Py(a,n2) & x,y are_congruent_mod Px(a,n) & n1 <> 2*n -n2;
per cases;
suppose n2 <= n;
then Py(a,n1) = Py(a,n2) by A1,Th33;
hence thesis by A1,Th15;
end;
suppose
A2: n2 >n;
then reconsider m=n2-n as Nat by NAT_1:21;
n+n-n2 >=n2-n2 by A1,XREAL_1:9;
then reconsider nm=n-m as Element of NAT by INT_1:3;
A3: sgn(n2)*Py(a,|.n2.|) = Py(a,n2) & sgn(nm)*Py(a,|.nm.|) =Py(a,nm) by Th23;
n2 = n+m;then
sgn(n2)*Py(a,|.n2.|),sgn(nm)*Py(a,|.nm.|)
are_congruent_mod Px(a,|.n.|) by Th32;
then sgn(y)*Py(a,n2),sgn(y)*Py(a,nm) are_congruent_mod Px(a,n)
by A3,INT_4:11;
then y,sgn(y)*Py(a,nm) are_congruent_mod Px(a,n) by A1,ABSVALUE:17;
then
A4: x,sgn(y)*Py(a,nm) are_congruent_mod Px(a,n) by A1,INT_1:15;
then
A5: sgn(y)*Py(a,nm),x are_congruent_mod Px(a,n) by INT_1:14;
nm = n+n-n2;
then
A6: nm < n+n-n by A2,XREAL_1:15;
A7: n1 < nm or nm < n1 by A1,XXREAL_0:1;
y <>0 by A1;
then y >0 or y <0;
then sgn y =1 or sgn y = -1 by ABSVALUE:def 2;
then sgn(y)*Py(a,nm) = Py(a,nm) or sgn(y)*Py(a,nm) = -Py(a,nm);
then
A8: |.sgn(y)*Py(a,nm).| = Py(a,nm);
per cases;
suppose n1 <= n;
then
A9: Py(a,n1) = Py(a,nm) or Py(a,n1) = - Py(a,nm)
by A1,A4,INT_1:14,A8,A6,A7,Th33;
Py(a,n1) <> - Py(a,nm)
proof
assume
A10: Py(a,n1) = - Py(a,nm);
n1=0 & nm=0 by A10;
hence thesis by A1;
end;
hence thesis by A9,A1,Th15;
end;
suppose
A11: n1 > n;
then reconsider k=n1-n as Nat by NAT_1:21;
n+n >= n1 by A1,XXREAL_0:2;
then n+n-n1 >=n1-n1 by XREAL_1:9;
then reconsider nk=n-k as Element of NAT by INT_1:3;
A12: sgn(n1)*Py(a,|.n1.|) = Py(a,n1)& sgn(nk)*Py(a,|.nk.|)=Py(a,nk) by Th23;
n1 = n+k;
then sgn(n1)*Py(a,|.n1.|),sgn(nk)*Py(a,|.nk.|)
are_congruent_mod Px(a,|.n.|) by Th32;
then sgn(x)*Py(a,n1),sgn(x)*Py(a,nk) are_congruent_mod Px(a,n)
by A12,INT_4:11;
then x,sgn(x)*Py(a,nk) are_congruent_mod Px(a,n) by A1,ABSVALUE:17;
then
A13: sgn(y)*Py(a,nm),sgn(x)*Py(a,nk) are_congruent_mod Px(a,n)
by A5,INT_1:15;
nk = n+n-n1;
then
A14: nk < n+n-n by A11,XREAL_1:15;
A15: nk<>nm by A1;
then
A16: nk < nm or nm < nk by XXREAL_0:1;
x <>0 by A1,A11;
then x >0 or x <0;
then sgn x =1 or sgn x = -1 by ABSVALUE:def 2;
then sgn(x)*Py(a,nk) = Py(a,nk) or sgn(x)*Py(a,nk) = -Py(a,nk);
then
A17: |.sgn(x)*Py(a,nk).|= Py(a,nk);
A18: Py(a,nk) = Py(a,nm) or Py(a,nk) = -Py(a,nm)
by Th33,A16,A14,A6,A13,INT_1:14,A8,A17;
Py(a,nk) <> - Py(a,nm)
proof
assume
A19: Py(a,nk) = - Py(a,nm);
nk=0 & nm=0 by A19;
hence thesis by A1;
end;
hence thesis by A18,A15,Th15;
end;
end;
end;
theorem Th34:
n1 <= 2*n & n2 <= 2*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n)
implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n
proof
assume that A1: n1 <= 2*n & n2 <= 2*n and
A2: |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n);
n1=n2 or n1>n2 or n1<n2 by XXREAL_0:1;
then n1=n2 or n1 = 2*n -n2 or n2 = 2*n -n1 by Lm9,A2,INT_1:14,A1;
then n1-n2 = 2*n*0 or n1 -- n2 = 2*n*1 or n1--n2 = 2*n*(-1);
hence thesis by INT_1:def 5;
end;
Lm10:
n1 <= 2*n & 2*n < n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n)
implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n
proof
assume that A1: n1 <= 2*n & 2*n < n2 <= 4*n and
A2: |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n);
reconsider m1=n2-2*n as Nat by A1,NAT_1:21;
A3: m1 <= 4*n -2*n by A1,XREAL_1:9;
m1 > 2*n-2*n & n2 >0 by XREAL_1:9,A1;
then
A4: sgn(m1) = 1 & sgn(n2) = 1 by ABSVALUE:def 2;
y <>0 by A2,A1;
then y >0 or y < 0;
then sgn y = 1 or sgn y = -1 by ABSVALUE:def 2;
then
A5: |.sgn(y)*(-Py(a,m1)).| = Py(a,m1);
2*n+m1 = n2;
then sgn(n2)*Py(a,|.n2.|),-sgn(m1)*Py(a,|.m1.|)
are_congruent_mod Px(a,|.n.|) by Th30;
then sgn(y)*Py(a,|.n2.|),sgn(y)*(-Py(a,m1))
are_congruent_mod Px(a,n) by A4,INT_4:11;
then y, sgn(y)*(-Py(a,m1))
are_congruent_mod Px(a,n) by ABSVALUE:17,A2;
then
A6: x, sgn(y)*(-Py(a,m1))
are_congruent_mod Px(a,n) by INT_1:15,A2;
per cases by XXREAL_0:1;
suppose
n1 < m1 or n1 >m1;
then n1 = 2*n -m1 or m1 = 2*n -n1 by A6,INT_1:14,A1,A2,A5,A3,Lm9;
then n1 -- n2 = 2*(2*n);
hence thesis by INT_1:def 5;
end;
suppose n1=m1;
then n1-n2 = (-1)*(2*n);
hence thesis by INT_1:def 5;
end;
end;
Lm11:
2*n < n1 <= 4*n & 2*n < n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n)
implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n
proof
assume that A1: 2*n < n1 <= 4*n & 2*n < n2 <= 4*n and
A2: |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n);
reconsider m2=n2-2*n as Nat by A1,NAT_1:21;
A3: m2 <= 4*n -2*n by A1,XREAL_1:9;
m2 > 2*n-2*n & n2 >0 by XREAL_1:9,A1;
then
A4: sgn(m2) = 1 & sgn(n2) = 1 by ABSVALUE:def 2;
y <>0 by A2,A1;
then y >0 or y < 0;
then sgn y = 1 or sgn y = -1 by ABSVALUE:def 2;
then
A5: |.sgn(y)*(-Py(a,m2)).| = Py(a,m2);
reconsider m1=n1-2*n as Nat by A1,NAT_1:21;
A6: m1 <= 4*n -2*n by A1,XREAL_1:9;
m1 > 2*n-2*n & n1 >0 by XREAL_1:9,A1;
then
A7: sgn(m1) = 1 & sgn(n1) = 1 by ABSVALUE:def 2;
x <>0 by A2,A1;
then x >0 or x < 0;
then sgn x = 1 or sgn x = -1 by ABSVALUE:def 2;
then
A8: |.sgn(x)*(-Py(a,m1)).| = Py(a,m1);
2*n+m1 = n1;
then sgn(n1)*Py(a,|.n1.|),-sgn(m1)*Py(a,|.m1.|)
are_congruent_mod Px(a,|.n.|) by Th30;
then sgn(x)*Py(a,|.n1.|),sgn(x)*(-Py(a,m1))
are_congruent_mod Px(a,n) by A7,INT_4:11;
then x, sgn(x)*(-Py(a,m1))
are_congruent_mod Px(a,n) by ABSVALUE:17,A2;
then sgn(x)*(-Py(a,m1)),x
are_congruent_mod Px(a,n) by INT_1:14;
then
A9: sgn(x)*(-Py(a,m1)),y
are_congruent_mod Px(a,n) by INT_1:15,A2;
2*n+m2 = n2;
then sgn(n2)*Py(a,|.n2.|),-sgn(m2)*Py(a,|.m2.|)
are_congruent_mod Px(a,|.n.|) by Th30;
then sgn(y)*Py(a,|.n2.|),sgn(y)*(-Py(a,m2))
are_congruent_mod Px(a,n) by A4,INT_4:11;
then y, sgn(y)*(-Py(a,m2))
are_congruent_mod Px(a,n) by ABSVALUE:17,A2;
then
A10: sgn(x)*(-Py(a,m1)),sgn(y)*(-Py(a,m2))
are_congruent_mod Px(a,n) by A9,INT_1:15;
per cases by XXREAL_0:1;
suppose
m1 < m2 or m1 >m2;
then m1 = 2*n -m2 or m2 = 2*n -m1 by A10,INT_1:14,A5,A3,A6,A8,Lm9;
then n1 -- n2 = 3*(2*n);
hence thesis by INT_1:def 5;
end;
suppose m1=m2;
then n1-n2 = 0*(2*n);
hence thesis by INT_1:def 5;
end;
end;
theorem Th35:
n1 <= 4*n & n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n)
implies n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n
proof
assume A1: n1 <= 4*n & n2 <= 4*n & |.x.| = Py(a,n1) & |.y.| = Py(a,n2) &
x,y are_congruent_mod Px(a,n);
then
A2: y,x are_congruent_mod Px(a,n) by INT_1:14;
per cases;
suppose n1 <= 2*n & n2 <= 2*n or n1 > 2*n & n2 > 2*n or n1 <= 2*n < n2;
hence thesis by A1,Th34,Lm10,Lm11;
end;
suppose n2 <=2*n <n1;
then n2,n1 are_congruent_mod 2*n or n2,-n1 are_congruent_mod 2*n
by A1,A2,Lm10;
then n1,n2 are_congruent_mod 2*n or (-1)*n2,(-1)*(-n1)
are_congruent_mod 2*n by INT_1:14,INT_4:11;
hence thesis by INT_1:14;
end;
end;
theorem Th36:
Py(a,n1),Py(a,n2) are_congruent_mod Px(a,n) & n >0
implies
n1,n2 are_congruent_mod 2*n or n1,-n2 are_congruent_mod 2*n
proof
assume that
A1: Py(a,n1),Py(a,n2) are_congruent_mod Px(a,n) and
A2: n>0;
reconsider m1 = n1 mod 4*n , d1= n1 div 4*n as Element of NAT;
A3: n1 - d1*(4*n) = m1 by A2,INT_1:def 10;
then sgn(4*d1*n+m1)*Py(a,|.4*d1*n+m1.|),sgn(m1)*Py(a,|.m1.|)
are_congruent_mod Px(a,|.n.|) by Th31;
then Py(a,n1),sgn(m1)*Py(a,|.m1.|) are_congruent_mod Px(a,|.n.|) by A3,Th23;
then Py(a,n1),Py(a,m1) are_congruent_mod Px(a,n) by Th23;
then
A4: Py(a,m1),Py(a,n1) are_congruent_mod Px(a,n) by INT_1:14;
reconsider m2 = n2 mod 4*n , d2= n2 div 4*n as Element of NAT;
A5: m1 <= 4*n & m2 <=4*n by A2,INT_1:58;
A6: |.Py(a,m1).| = Py(a,m1) & |.Py(a,m2).| = Py(a,m2);
A7: n2 - d2*(4*n) = m2 by A2,INT_1:def 10;
then sgn(4*d2*n+m2)*Py(a,|.4*d2*n+m2.|),sgn(m2)*Py(a,|.m2.|)
are_congruent_mod Px(a,|.n.|) by Th31;
then Py(a,n2),sgn(m2)*Py(a,|.m2.|) are_congruent_mod Px(a,|.n.|) by A7,Th23;
then Py(a,n2),Py(a,m2) are_congruent_mod Px(a,n) by Th23;
then Py(a,n1),Py(a,m2) are_congruent_mod Px(a,n) by A1,INT_1:15;
then Py(a,m1),Py(a,m2) are_congruent_mod Px(a,n) by A4,INT_1:15;
then
A8: m1,m2 are_congruent_mod 2*n or m1,-m2 are_congruent_mod 2*n
by A6,A5,Th35;
n1-m1 = (2*d1)*(2*n) by A3;
then n1,m1 are_congruent_mod 2*n by INT_1:def 5;
then
A9:n1,m2 are_congruent_mod 2*n or n1,-m2 are_congruent_mod 2*n
by A8,INT_1:15;
m2-n2 = (-2*d2)*(2*n) & -m2--n2 = (2*d2)*(2*n) by A7;
then m2,n2 are_congruent_mod 2*n & -m2,-n2 are_congruent_mod 2*n
by INT_1:def 5;
hence thesis by A9,INT_1:15;
end;
begin :: Solutions of Pell's Equation - Divisibility
theorem Th37:
Py(a,n) divides Py(a,n*k)
proof
defpred P[Nat] means Py(a,n) divides Py(a,n*$1);
Py(a,n) * 0 = Py(a,n*0) by Th6;
then
A1: P[0] by INT_1:def 3;
A2: for k holds P[k] implies P[k+1]
proof
let k;
assume
A3: P[k];
A4: Py(a,n*k+n) = sgn(n*k+n)*Py(a,|.n*k+n.|) & sgn(n)*Py(a,|.n.|) = Py(a,n)
& sgn(n*k)*Py(a,|.n*k.|)= Py(a,n*k) by Th23;
then
A5: Py(a,|.n*k+n.|) = Px(a,|.n*k.|)*sgn(n)*Py(a,|.n.|) +
sgn(n*k)*Py(a,|.n*k.|)*Px(a,|.n.|) by Th25
.= Px(a,n*k) * Py(a,n) + Py(a,n*k)*Px(a,n) by A4;
A6: Py(a,n) divides Py(a,n*k)*Px(a,n) by A3,INT_2:2;
Py(a,n) divides Px(a,n*k) * Py(a,n) by NAT_D:9;
hence thesis by A5,A6,NAT_D:8;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th38:
Py(a,n*k), k * (Px(a,n) |^ (k-'1)) *Py(a,n) are_congruent_mod Py(a,n)^2
proof
set m=min_Pell's_solution_of (a^2-'1);
set x = Px(a,n),y=Py(a,n),s = sqrt (a^2-'1),ys= y*s;
per cases;
suppose n=0 or k=0;
then (y=0 or k=0) & Py(a,n*k)=0 by Th6;
hence thesis by INT_1:11;
end;
suppose A1: n>0 & k >0;
set I=(x,ys) In_Power k;
A2: x+ys = (m`1 + m`2 *s) |^n by Def2;
A3: Px(a,n*k)+Py(a,n*k)*s = (m`1 + m`2 *s) |^(n*k) by Def2
.= (x+ys) |^ k by A2,NEWTON:9
.= Sum I by NEWTON:30;
consider e,o be complex-valued FinSequence such that
A4: len e = [\len I/2/] & len o = [/len I/2 \] and
A5: Sum I = Sum e + Sum o and
A6: for n holds e.n = I.(2*n) & o.n = I.(2*n-1) by Th2;
A7: len I = k+1 by NEWTON:def 4;
s|^(1+1) = s* s|^1 by NEWTON:6
.= s^2
.= (a^2-'1) by SQUARE_1:def 2;
then
A8: ys|^2 = (y |^ 2) * (a^2-'1) by NEWTON:7;
rng o c= NAT
proof
let w be object;assume w in rng o;
then consider z be object such that
A9: z in dom o & o.z=w by FUNCT_1:def 3;
reconsider z as Nat by A9;set Z=2*z-1;
A10: w = I.Z by A6,A9;
A11: 1<= z <= len o by A9,FINSEQ_3:25;
A12: 2*z >=2*1 by XREAL_1:64,A9,FINSEQ_3:25;
then
A13: Z >= 2-1 by XREAL_1:9;
reconsider zz=Z,m = Z-1 as Nat by A12;
A14: len I/2+1 = (len I+2)/2;
len o < len I/2 +1 by A4,INT_1:def 7;
then z < len I/2+1 by A11,XXREAL_0:2;
then 2*z < k+1+2 & k+1+2 = k+2+1 by A7,A14,XREAL_1:79;
then
A15: 2*z <= k+1+1 by NAT_1:13;
then
A16: Z <= k+1 by XREAL_1:20;
reconsider l = k+1-zz as Nat by NAT_1:21,XREAL_1:20,A15;
A17: Z in dom I by A16,A7,A13,FINSEQ_3:25;
l = k-m;
then
A18: I.Z = (k choose m) * x|^l *ys|^m by A17,NEWTON:def 4;
reconsider z1=z-1 as Nat by A11;
m = 2*z1;
then ys|^m = ((y |^ 2) * (a^2-'1)) |^z1 by A8,NEWTON:9;
hence thesis by A10,A18,ORDINAL1:def 12;
end;
then reconsider o as FinSequence of NAT by FINSEQ_1:def 4;
defpred E[object,object] means $2 in NAT & for n be Nat st n=$2
holds e.$1 = s * n &
for N be Nat st N=$1 holds N-1 is Nat & 2*N-1 is Nat & k+1-2*N is Nat
& for n1,m,l be Nat st n1=N-1 & m= 2*N-1 & l=k+1-2*N holds
$2 =(k choose m) * x|^l *(((y |^ 2) * (a^2-'1)) |^ n1 * y);
A19:for n st n in Seg len e ex x be object st E[n,x]
proof
let n such that
A20: n in Seg len e;
set N=2*n;
A21: 1<= n <= len e by A20,FINSEQ_1:1;
then N >=2*1 by XREAL_1:64;
then
A22: N >= 1 by XXREAL_0:2;
reconsider m = N-1,n1=n-1 as Nat by A21;
len e <= len I/2 by A4,INT_1:def 6;
then n <= len I/2 by A21,XXREAL_0:2;
then
A23: N <= k+1 by A7,XREAL_1:83;
then reconsider l = k+1-N as Nat by NAT_1:21;
take U= (k choose m) * x|^l *(((y |^ 2) * (a^2-'1)) |^ n1 * y);
thus U in NAT by ORDINAL1:def 12;
let u be Nat such that
A24: u=U;
A25: N in dom I by A23,A7,A22,FINSEQ_3:25;
l = k-m;
then
A26: I.N = (k choose m) * x|^l *ys|^m by A25,NEWTON:def 4;
m = 2*n1+1;
then ys|^m = (ys |^(2*n1)) * ys by NEWTON:6
.= ((y |^ 2) * (a^2-'1)) |^ n1 * ys by A8,NEWTON:9;
hence e.n = s * u by A6,A26,A24;
let nn be Nat such that
A27: n=nn;
nn-1 =n1 & 2*nn-1 = m & k+1-2*nn = l by A27;
hence thesis;
end;
consider p be FinSequence such that
A28: dom p = Seg len e & for n st n in Seg len e holds E[n,p.n]
from FINSEQ_1:sch 1(A19);
rng p c= NAT
proof
let w be object;assume w in rng p;
then ex n be object st n in dom p & p.n=w by FUNCT_1:def 3;
hence thesis by A28;
end;
then reconsider p as FinSequence of NAT by FINSEQ_1:def 4;
A29: dom (s*p) = dom p & dom p = dom e
by A28,VALUED_1:def 5,FINSEQ_1:def 3;
A30: len p=len e by A28,FINSEQ_1:def 3;
for n st n in dom p holds e.n = (s*p).n
proof
let n;
assume n in dom p;
hence e.n = s * (p.n) by A28
.= (s*p).n by VALUED_1:6;
end;
then e = s*p by A29,FINSEQ_1:13;
then Sum I = Sum o+s * Sum p by A5,RVSUM_1:87;
then
A31: Py(a,n*k) = Sum p by A3,PELLS_EQ:3;
A32: Sum p is Nat by TARSKI:1;
A33: y|^(1+1) = y* y|^1 by NEWTON:6
.= y*y;
for n st 1 < n <= len p holds (p.n) mod y^2 =0
proof
let n; assume
A34: 1 < n <= len p;
then
A35: n in Seg len e by A28,FINSEQ_3:25;
then E[n,p.n] by A28;
then reconsider n1=n-1, m=2*n-1, l= k+1-2*n as Nat;
A36: p.n = (k choose m) * x|^l *(((y |^ 2) * (a^2-'1)) |^ n1 * y)
by A35,A28;
A37: n-1 > 1-1 by A34,XREAL_1:9;
y^2 divides ((y |^ 2) * (a^2-'1)) |^ n1
by A37,NEWTON02:14,A33,INT_1:def 3;
then y^2 divides ((y |^ 2) * (a^2-'1)) |^ n1 * y by NAT_D:9;
then y^2 divides p.n by A36, NAT_D:9;
hence thesis by INT_1:62,A1;
end;
then Sum p mod y^2 = p.1 mod y^2 by Th1;
then ((Sum p) - (p.1)) mod (y^2) =0 by A32,INT_4:22,A1;
then y^2 divides Sum p - p.1 by INT_1:62,A1;
then
A38: Sum p, p.1 are_congruent_mod y^2 by INT_1:def 4;
len I >= 1+1 & 1+1= 2*1 by XREAL_1:6,A7,A1,NAT_1:14;
then len I/2 >= 1 by XREAL_1:77;
then len p >= 1 by INT_1:54,A30,A4;
then
A39: 1 in Seg len e by A28,FINSEQ_3:25;
then E[1,p.1] by A28;
then reconsider l= k+1-2*1 as Nat;
A40: k choose 1 = k by NEWTON:23,A1,NAT_1:14;
A41: ((y |^ 2) * (a^2-'1)) |^ 0 = 1 by NEWTON:4;
A42: l=k-1;
1-1=0 & 2*1-1=1;then
p.1 = k * x|^l *(1 * y) by A39,A28,A40,A41;
hence thesis by A42,A31,A38,XREAL_0:def 2;
end;
end;
theorem Th39:
k >0 & Py(a,k) divides Py(a,n) implies k divides n
proof
set Pk=Py(a,k),Pn=Py(a,n);
set r=n mod k,q = n div k;
assume
A1: k>0 & Pk divides Pn;
reconsider r,q as Element of NAT;
A2: r = n - q*k by A1,INT_1:def 10;
then n = r+q*k;
then sgn(n)*Py(a,|.n.|) = Px(a,|.r.|)*sgn(q*k)*Py(a,|.q*k.|) +
sgn(r)*Py(a,|.r.|)*Px(a,|.q*k.|) by Th25;
then
A3:Py(a,n) = Px(a,|.r.|)*(sgn(q*k)*Py(a,|.q*k.|)) +
sgn(r)*Py(a,|.r.|)*Px(a,|.q*k.|) by Th23
.= Px(a,|.r.|)*Py(a,q*k) +
sgn(r)*Py(a,|.r.|)*Px(a,|.q*k.|) by Th23
.= Px(a,r)*Py(a,q*k) + Py(a,r)*Px(a,q*k) by Th23;
A4: Pk divides Py(a,q*k) by Th37;
Pk divides Px(a,r)*Py(a,q*k) by Th37,INT_2:2;
then
A5: Pk divides Py(a,r)*Px(a,q*k) by INT_2:1,A1,A3;
A6: Pk,Px(a,k*q) are_coprime
proof
Pk gcd Px(a,k*q) divides Py(a,k) by INT_2:def 2;
then
A7: Py(a,k) gcd Px(a,k*q) divides Py(a,q*k) by A4, INT_2:9;
Pk gcd Px(a,k*q) divides Px(a,k*q) by INT_2:def 2;
then Pk gcd Px(a,k*q) divides Py(a,q*k) gcd Px(a,k*q) by A7,INT_2:22;
then Pk gcd Px(a,k*q) divides 1 by Th26,INT_2:def 3;
then Pk gcd Px(a,k*q) = 1 by INT_2:13;
hence thesis by INT_2:def 3;
end;
r=0
proof
assume r<>0;
then |.Pk.| <= |.Py(a,r).| by A6,INT_4:6,A5,INT_2:25;
hence thesis by Th14,INT_1:58,A1;
end;
hence thesis by A2,INT_1:def 3;
end;
theorem Th40:
Py(a,k)^2 divides Py(a,n) implies Py(a,k) divides n
proof
assume A1: Py(a,k)^2 divides Py(a,n);
per cases;
suppose k=0;
then Py(a,k)=0 by Th6;
then ex i be Integer st 0*i = Py(a,n) by A1,INT_1:def 3;
then Py(a,k)*0 = n;
hence thesis by INT_1:def 3;
end;
suppose A2:k>0;
Py(a,k) divides Py(a,k)^2 by INT_1:def 3;
then Py(a,k) divides Py(a,n) by A1,INT_2:9;
then consider w be Nat such that
A3: k*w = n by NAT_D:def 3,Th39,A2;
A4: w divides n by A3,NAT_D:def 3;
Py(a,k)^2 divides Py(a,n)-0 by A1;
then
A5: 0,Py(a,n) are_congruent_mod Py(a,k)^2 by INT_1:14,def 4;
Py(a,n), w * (Px(a,k) |^ (w-'1)) *Py(a,k) are_congruent_mod Py(a,k)^2
by Th38,A3;
then
A6: 0*(Px(a,k) |^ (w-'1)),(w* Py(a,k))*(Px(a,k) |^ (w-'1))
are_congruent_mod Py(a,k)^2 by A5,INT_1:15;
A8: Py(a,k)^2 = Py(a,k) * Py(a,k) |^1
.= Py(a,k) |^(1+1) by NEWTON:6;
Py(a,k),Px(a,k) are_coprime by Th26;
then Py(a,k) |^2,Px(a,k) are_coprime by WSIERP_1:10;
then 0,w* Py(a,k) are_congruent_mod Py(a,k)^2
by A6,A8,INT_4:9,WSIERP_1:10;
then Py(a,k)^2 divides w* Py(a,k)-0 by INT_1:def 4,14;
then Py(a,k) divides w or Py(a,k) = 0 by PYTHTRIP:7;
hence thesis by A4,A2,INT_2:9;
end;
end;
begin :: Special Case of Pell's Equation is Diophantin
theorem
for y,z,a be Nat holds
y = Py(a,z) & a > 1
iff ex x,x1,y1,A,x2,y2 be 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
proof
let y,z,a be Nat;
thus y = Py(a,z) & a > 1 implies ex x,x1,y1,A,x2,y2 be 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
proof
assume
A1: y=Py(a,z) & a >1;
then A2:a is non 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;
x^2 - (a^2-'1) *y^2 =1 by A1,Th10,A2;
then
A5: [x,y] is Pell's_solution of (a^2-'1) & a > 1
by A1,Lm3;
A6: y >= z by Th16,A1,A2;
per cases;
suppose
A7: y=0;
then
A8: z=0 by A1,A2;
then
A9: x=1 by Th6,A2;
set x1=x,y1=y,y2=y, A =1;
A^2-'1 = 1-1 by XREAL_1:233;
then
A10: 1^2-(A^2-'1)*y2^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,y2] is Pell's_solution of (A^2-'1) by A10,A11,A7,PELLS_EQ:def 1;
A13: y2,y are_congruent_mod x1 by INT_1:11;
A14: A,a are_congruent_mod x1 by INT_1:13,A9;
A15: A,1 are_congruent_mod 2*y by INT_1:11;
y1,0 are_congruent_mod y^2 by A7,INT_1:11;
hence thesis by A5,A12,A13,A14,A8,A7,A15;
end;
suppose
A16: y>0;
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=M`1,Y1=M`2;
A17: x1^2-B*Y1^2=1 by PELLS_EQ:def 1;
set y1=2*y^2*Y1;
A18: x1=[x1,y1]`1 & y1=[x1,y1]`2;
x1 in INT & y1 in INT by INT_1:def 2;
then
A19: [x1,y1] in [:INT,INT:] by ZFMISC_1:87;
A20: x1^2 - (a^2-'1)*y1^2=
1+B*Y1^2 - (a^2-'1)*y1^2 by PELLS_EQ:def 1
.=1;
then
A21: [x1,y1] is Pell's_solution of (a^2-'1) by A18,A19,PELLS_EQ:def 1;
2*Y1*y >=1*1 by A16,NAT_1:14;
then
A22: 2*Y1*y*y >= 1*y by XREAL_1:66;
A23: y1 >0 by A22;
then
A24: y1^2 >=1 & y1 >=1 by NAT_1:14;
y1= y^2*(2*Y1) & y1 = (2*y)*(y*Y1);
then
A25: y^2 divides y1-0 & 2*y divides y1 by INT_1:def 3;
then
A26: y1,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,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;
Y1^2 >= 1^2 by NAT_1:14;
then 1+B*Y1^2 > a by NAT_1:13,A28, XREAL_1:66;
then x1^2-a >=a-a by A17,XREAL_1:9;
then reconsider x1a=x1^2-a as Element of NAT by INT_1:3;
set A = a+x1^2*x1a;
A >=2+0 by A3,XREAL_1:7;
then A <>1 & A is non empty;
then reconsider A as non trivial Nat by NAT_2:28;
A-a = x1*(x1*x1a);
then
A29: A,a are_congruent_mod x1 by INT_1:def 4,def 3;
A = a+(1+(a^2-'1)*y1^2)*(1+(a^2-'1)*y1^2-a) by A20;
then
A30: A-1 = y1*(y1*( (a^2-'1) + (1+(a^2-'1)*y1^2)*(a^2-'1) -a * (a^2-'1)));
then
A31: y1 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)*(y1^2) >= a*1 by A27,A24,XREAL_1:66;
then 2+ (a^2-'1)*(y1^2) > a*1+0 by XREAL_1:8;
then 2+(a^2-'1)*y1^2-a >a-a by XREAL_1:9;
then y1* ((a^2-'1)*(2+(a^2-'1)*y1^2-a)) >= 1*1 by A2,A23,NAT_1:14;
then A-1 >=1*y1 & A-0 > A-1 by A30,XREAL_1:66,10;
then A > y1 by XXREAL_0:2;
then
A34: A > y by A22, XXREAL_0:2;
set x2 = Px(A,z),y2 = Py(A,z);
x2^2 - (A^2-'1) *y2^2 =1 by Th10;
then
A35: [x2,y2] is Pell's_solution of (A^2-'1) by Lm3;
A-1 divides y2-z by Th27,INT_1:def 4;
then y2,z are_congruent_mod 2*y by INT_1:def 4,A32,INT_2:9;
hence thesis by A5,A21,A6,A35,A2,A1,Th29,A29,A33,A26,A22,A34;
end;
end;
given x,x1,y1,A,x2,y2 be 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;
A47: a is non trivial by NAT_2:28,A36;
per cases;
suppose
A48: y=0;
then z=0 by A40;
hence thesis by A36,A47,Th6,A48;
end;
suppose
A49: y >0;
then y >=1 by NAT_1:14;
then reconsider A as non trivial Nat by A39,NAT_2:28;
consider w be Nat such that
A50: x = Px(a,w) & y = Py(a,w) by A47,A37,Th7;
consider u be Nat such that
A51: x1 = Px(a,u) & y1 = Py(a,u) by A47,A38,Th7;
consider v be 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
proof
A56: 2*y divides A-1 by A45,INT_1:def 4;
A-1 divides Py(A,v)-v by Th27,INT_1:def 4;
hence thesis by INT_1:def 4,A56,INT_2:9;
end;
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 be 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 <= 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 < 1*(2*y) by A63,XXREAL_0:2;
A65: 0+0 <= z+w <= y+y by A40,A62,XREAL_1:7;
per cases by A60,A55,Th36,A47;
suppose v,w are_congruent_mod 2*u;
then consider t be 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 be Integer such that
A67: z-w = (2*y)*i by INT_1:def 5,A59,INT_1:15;
-1 < 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;
end;
suppose v,-w are_congruent_mod 2*u;
then consider t be 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 be 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)*1 by A69,A65;
then
A70: 0 <= 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 by A71,A69;
suppose z+w=0;
then z=0=w;
hence thesis by A36,A50;
end;
suppose
A72: z+w = 2*y;
A73: z=y
proof
assume z<>y;
then z < y by A40,XXREAL_0:1;
then z+w <y+y by A47,A50,Th16,XREAL_1:8;
hence thesis by A72;
end;
w=y
proof
assume w<>y;
then w < y by A62,XXREAL_0:1;
then z+w <y+y by A40,XREAL_1:8;
hence thesis by A72;
end;
hence thesis by A36,A73,A50;
end;
end;
end;
end;
begin :: Exponential Function is Diophantin
theorem
for x,y,z be Nat holds
y = x|^z
iff
(y = 1 & z = 0) or
(x = 0 & y = 0 & z > 0) or
(x = 1 & y = 1 & z > 0) or
(x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2))
proof
let x,y,z be Nat;
thus y = x|^z implies
( y = 1 & z = 0) or
(x = 0 & y = 0 & z > 0) or
(x = 1 & y = 1 & z > 0) or
(x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2))
proof
assume
A1: y=x|^z;
per cases;
suppose z=0;
hence thesis by A1,NEWTON:4;
end;
suppose
A2: z>0;
per cases by NAT_1:53;
suppose x=0 or x=1;
hence thesis by A1,A2,NAT_1:14,NEWTON:11;
end;
suppose
A3: x>1;
then reconsider x1=x as non trivial Nat by NAT_2:28;
ex y1,y2,y3,K be Nat st
y1 = Py(x1,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x1,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2)
proof
set y1 = Py(x1,z+1),K=2*z*y1+1,y2=Py(K,z+1), y3 = Py(K*x1,z+1);
reconsider K as non trivial Nat by A2;
take y1,y2,y3,K;
x1+(x1-1) > x1+0 by XREAL_1:6;
then
A4: (x1+(x1-1)) to_power z > x1 to_power z by A2,POWER:37;
(2*x1-1)|^z <=y1 by Th20;
then y1 >= x1|^z by A4,XXREAL_0:2;
then K > 2*z*(x1|^z) by NAT_1:13,XREAL_1:64;
then
A5: y - 1/2 < y3/y2 < y + 1/2 by A1,Th22;
y-y3/y2 >=0 or -(y-y3/y2)>= -0;
hence thesis by NAT_1:13,XREAL_1:19,XREAL_1:11,A5;
end;
hence thesis by A3,A2;
end;
end;
end;
assume
A6: (y = 1 & z = 0) or
(x = 0 & y = 0 & z > 0) or
(x = 1 & y = 1 & z > 0) or
(x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2));
per cases by A6;
suppose y=1 & z=0;
hence thesis by NEWTON:4;
end;
suppose x = 0 & y = 0 & z > 0;
hence thesis by NAT_1:14,NEWTON:11;
end;
suppose x = 1 & y = 1 & z > 0;
hence thesis;
end;
suppose
A7: x > 1 & z > 0 & ex y1,y2,y3,K be Nat st
y1 = Py(x,z+1) & K > 2*z*y1 & y2 = Py(K,z+1) & y3 = Py(K*x,z+1) &
(0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2);
reconsider x1=x as non trivial Nat by A7,NAT_2:28;
consider y1,y2,y3,K be Nat such that
A8: y1 = Py(x1,z+1) and
A9: K > 2*z*y1 and
A10: y2 = Py(K,z+1) and
A11: y3 = Py(K*x1,z+1) and
A12: 0 <= y-y3/y2 <1/2 or 0 <= y3/y2 -y < 1/2 by A7;
2*z*y1 >=1 by NAT_1:14,A8,A7;
then reconsider K as non trivial Nat by NAT_2:28,A9;
x1+(x1-1) > x1+0 by XREAL_1:6;
then
A13: (x1+(x1-1)) to_power z > x1 to_power z by A7,POWER:37;
(2*x1-1)|^z <=y1 by A8,Th20;
then y1 >= x1|^z by A13,XXREAL_0:2;
then y1*(2*z) >= (x1|^z)*(2*z) by XREAL_1:64;
then K > 2*z*(x1|^z) by A9,XXREAL_0:2;
then
A14: x1|^z - 1/2 < y3/y2 < x1|^z + 1/2 by Th22,A10,A11;
per cases by A12;
suppose 0 <= y-y3/y2 <1/2;
then
A15: x1|^z - 1/2+0 < y-y3/y2+y3/y2< 1/2+(x1|^z + 1/2) by A14,XREAL_1:8;
then y < (x1|^z)+1;
then
A16: y <= x1|^z by INT_1:7;
x1|^z - 1 < x1|^z - 1/2 by XREAL_1:10;
then x1|^z -1 < y by A15,XXREAL_0:2;
then x1|^z-1+1 <=y by INT_1:7;
hence thesis by A16,XXREAL_0:1;
end;
suppose 0 <= y3/y2 -y < 1/2;
then
A17: x1|^z - 1/2 -1/2 < y3/y2 -(y3/y2 -y) < x1|^z + 1/2 -0
by A14,XREAL_1:14;
then
A18: x1|^z -1+1 <= y by INT_1:7;
x1|^z +1/2 < x1|^z +1 by XREAL_1:6;
then y < x1|^z +1 by A17,XXREAL_0:2;
then y <= x1|^z by INT_1:7;
hence thesis by A18,XXREAL_0:1;
end;
end;
end;