:: Prime Representing Polynomial
:: by Karol P\kak
::
:: Received November 30, 2021
:: Copyright (c) 2021-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, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, FUNCT_1,
XXREAL_0, NAT_1, INT_1, ARYTM_3, ZFMISC_1, CARD_1, ORDINAL1, ARYTM_1,
AFINSQ_1, COMPLEX1, SQUARE_1, NEWTON, HILB10_2, INT_2, REAL_1, CARD_3,
REALSET1, PELLS_EQ, PYTHTRIP, MCART_1, HILB10_1, ABSVALUE, POWER;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, XCMPLX_0, FINSEQ_1,
XXREAL_0, XREAL_0, INT_1, AFINSQ_1, SQUARE_1, NEWTON, POWER, HILB10_2,
RVSUM_1, CARD_1, NAT_D, PELLS_EQ, PYTHTRIP, ABSVALUE, HILB10_1, ZFMISC_1,
XTUPLE_0, INT_2;
constructors NAT_D, RECDEF_1, RELSET_1, NEWTON, HILB10_2, WSIERP_1, INT_6,
PELLS_EQ, DOMAIN_1, PEPIN, ABSVALUE, ABIAN, POWER, HILB10_1;
registrations RELAT_1, ORDINAL1, XREAL_0, NAT_1, VALUED_0, INT_1, AFINSQ_1,
HILB10_2, XXREAL_0, XCMPLX_0, NEWTON, NEWTON02, NAT_6, FINSEQ_1,
NEWTON04, INT_6, NEWTON03, PYTHTRIP, ABIAN, ABSVALUE, POWER, HILB10_1,
XTUPLE_0, FOMODEL0;
requirements NUMERALS, SUBSET, ARITHM, REAL;
equalities FINSEQ_1;
theorems NAT_1, ZFMISC_1, XREAL_1, XXREAL_0, NEWTON, INT_1, FINSEQ_3,
SQUARE_1, ABSVALUE, PEPIN, RVSUM_1, FINSEQ_5, INT_4, INT_2, NAT_D,
PREPOWER, HILB10_3, NEWTON03, HILB10_4, PELLS_EQ, HILB10_1, NAT_2,
XCMPLX_1, GAUSSINT, NAT_6, IRRAT_1, WSIERP_1, CATALAN2, PRE_FF, POWER,
PYTHTRIP, NAT_5;
schemes NAT_1, HILB10_3;
begin :: The Prime Number Set as a Diophantine Set
reserve n for Nat,
i,j,i1,i2,i3,i4,i5,i6 for Element of n,
p,q,r for n-element XFinSequence of NAT;
theorem Th1:
for i holds {p: p.i > 1} is diophantine Subset of n -xtuples_of NAT
proof
let i;
defpred Q[XFinSequence of NAT] means 1* $1 . i > 0*$1.i+1;
defpred R[XFinSequence of NAT] means $1 . i > 1;
A1:Q[q] iff R[q];
{q: Q[q]} = {r: R[r]} from HILB10_3:sch 2(A1);
hence thesis by HILB10_3:7;
end;
theorem Th2:
for i,j holds {p: p.i = (p.j-'1)! + 1}
is diophantine Subset of n -xtuples_of NAT
proof
A1:for n,i1,i2 holds
{p: p.i1 = p.i2-'1} is diophantine Subset of n -xtuples_of NAT
proof
let n,i1,i2;
defpred Q[XFinSequence of NAT] means 1* $1.i1 = 1* $1.i2-' 1;
defpred R[XFinSequence of NAT] means $1.i1 = $1.i2-' 1;
A2:Q[q] iff R[q];
{q: Q[q]} = {r: R[r]} from HILB10_3:sch 2(A2);
hence thesis by HILB10_3:20;
end;
A3:for n,i1,i2 holds
{p: p.i1 = (p.i2-' 1)!} is diophantine Subset of n -xtuples_of NAT
proof
defpred P[Nat,Nat,natural object,Nat,Nat,Nat] means $4 = ($3)!;
deffunc F(Nat,Nat,Nat) = $2-'1;
A4:for n,i1,i2,i3,i4,i5,i6 holds {p: P[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by HILB10_4:32;
A5:for n,i1,i2,i3,i4 holds {p: F(p.i1,p.i2,p.i3) = p.i4}
is diophantine Subset of n -xtuples_of NAT by A1;
for n,i1,i2,i3,i4,i5 holds
{p:P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A4,A5);
hence thesis;
end;
defpred P[Nat,Nat,natural object,Nat,Nat,Nat] means $4 = 1*$3+1;
deffunc F(Nat,Nat,Nat) = ($2 -' 1)!;
A6:for n,i1,i2,i3,i4,i5,i6 holds {p: P[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:15;
A7:for n,i1,i2,i3,i4 holds {p: F(p.i1,p.i2,p.i3) = p.i4}
is diophantine Subset of n -xtuples_of NAT by A3;
A8: for n,i1,i2,i3,i4,i5 holds
{p:P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A6,A7);
let i1,i2;
defpred Q[XFinSequence of NAT] means $1.i1 = 1*(($1.i2-'1)!)+1;
defpred R[XFinSequence of NAT] means $1.i1 = ($1.i2-'1)!+1;
A9:Q[q] iff R[q];
{q: Q[q]} = {r: R[r]} from HILB10_3:sch 2(A9);
hence thesis by A8;
end;
theorem Th3:
for i holds {p: (p.i-'1)! + 1 mod p.i = 0 & p.i > 1}
is diophantine Subset of n -xtuples_of NAT
proof
defpred P[Nat,Nat,natural object,Nat,Nat,Nat] means
1*$3,0*$4 are_congruent_mod 1*$4;
deffunc F(Nat,Nat,Nat) = ($2 -' 1)!+1;
A1:for n,i1,i2,i3,i4,i5,i6 holds {p: P[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:21;
A2:for n,i1,i2,i3,i4 holds {p: F(p.i1,p.i2,p.i3) = p.i4}
is diophantine Subset of n -xtuples_of NAT by Th2;
A3:for n,i1,i2,i3,i4,i5 holds
{p:P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A1,A2);
let i;
defpred Q1[XFinSequence of NAT] means
1*(($1.i-'1)!+1),0*$1.i are_congruent_mod 1*$1.i;
defpred Q2[XFinSequence of NAT] means $1.i > 1;
defpred Q12[XFinSequence of NAT] means Q1[$1] & Q2[$1];
A4:{q: Q1[q]} is diophantine Subset of n -xtuples_of NAT by A3;
A5:{q: Q2[q]} is diophantine Subset of n -xtuples_of NAT by Th1;
A6:{q: Q1[q] & Q2[q]} is diophantine Subset of n -xtuples_of NAT
from HILB10_3:sch 3(A4,A5);
defpred R[XFinSequence of NAT] means ($1.i-'1)! + 1 mod $1.i = 0 & $1.i > 1;
A7:Q12[q] iff R[q]
proof
hereby assume A8:Q12[q];
then ((q.i-'1)!+1) mod q.i = 0 mod q.i by NAT_D:64;
hence R[q] by A8;
end;
assume A9: R[q];
then ((q.i-'1)!+1) mod q.i = 0 mod q.i;
hence Q12[q] by A9,NAT_D:64;
end;
{q: Q12[q]} = {r: R[r]} from HILB10_3:sch 2(A7);
hence thesis by A6;
end;
theorem
for n being Nat,i being Element of n holds
{p where p is n-element XFinSequence of NAT: p.i is prime}
is diophantine Subset of n -xtuples_of NAT
proof let n,i;
defpred Q[XFinSequence of NAT] means $1.i is prime;
defpred R[XFinSequence of NAT] means ($1.i-'1)! + 1 mod $1.i = 0 & $1.i > 1;
A1:Q[q] iff R[q] by NAT_5:22;
{q: Q[q]} = {r: R[r]} from HILB10_3:sch 2(A1);
hence thesis by Th3;
end;
begin :: Special Case of Pell's Equation - Selected Properties
reserve i,j,n,n1,n2,m,k,l,u,e,p,t for Nat,
a,b for non trivial Nat,
x,y for Integer,
r,q for Real;
Lm1: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;
thus thesis by PELLS_EQ:def 1,A1;
end;
theorem Th5:
2 <= e & (ex i st e^2 *(e *(e+2))* (n+1)^2 +1 = i^2) implies
e - 1 + e |^ (e-'2) <= n
proof
set a=e+1, n1=n+1,A=a^2-'1;
A1:a^2=a*a by SQUARE_1:def 1;
assume
A2: 2 <= e;
then
A3: e-2=e-'2 by XREAL_1:233;
a*a>=0+1 by INT_1:7;
then
A4: A = a*a-1 by XREAL_1:233,A1
.= (a-1) *(a+1);
reconsider e2=e-2 as Nat by A2,NAT_1:21;
given i such that
A5: e^2 *(e *(e+2))*n1^2 +1 = i^2;
(e*n1)^2 = (e*n1)*(e*n1) & e^2=e*e & n1^2=n1*n1 by SQUARE_1:def 1;
then
A6:i^2 - A * (e*n1)^2 = 1 by A5,A4;
[i,e*n1] is Pell's_solution of A by A6,Lm1;
then consider j such that
A7: i = Px(a,j) & e*n1 = Py(a,j) by A2,HILB10_1:4;
A8: j<>0 by A7,A2,HILB10_1:3;
A9: Py(a,j),j are_congruent_mod (a-1) by A2,HILB10_1:24;
0*n1,e*n1 are_congruent_mod e by INT_4:11,INT_1:12;
then e divides 0-j by INT_1:def 4,A9,A7,INT_1:15;
then e divides --j by INT_2:10;
then e <=j by A8,INT_2:27;
then e<j or e=j by XXREAL_0:1;
then
A10: Py(a,e) < Py(a,j) or Py(a,e) = Py(a,j) by HILB10_1:11,A2;
A11: (2*a-1) |^(e2+1) <= Py(a,e2+1+1) by HILB10_1:17;
(a-2)*e + e|^(e2+1) < (2*a-1) |^(e2+1)
proof
per cases by A2,XXREAL_0:1;
suppose e=2;
hence thesis;
end;
suppose e>2;
then
A12: e2+1+1>1+1;
then
A13: e2+1 >=1+1 by NAT_1:13;
e2+1>1 by A12,XREAL_1:7;
then
A14: e2+1 is non trivial by NEWTON03:def 1;
A15: 2*a-1 = a+e;
a>=0+1 by NAT_1:13;
then
A16: a|^(e2+1) >= a|^ 2 & a|^2 = a*a by A13,PREPOWER:93,NEWTON:81;
A17: a-2 = e2+1;
a-0>= a-1 & a-0 >= a-2 by XREAL_1:13;
then a*a >= (a-1)*(a-2) by A17,XREAL_1:66;
then a|^(e2+1) >= (a-1)*(a-2) by A16,XXREAL_0:2;
then a|^(e2+1) + e|^(e2+1) >= (a-1)*(a-2) + e|^(e2+1) by XREAL_1:7;
hence thesis by A15,A14,A2,NEWTON03:103,XXREAL_0:2;
end;
end;
then (a-2)*e + e|^(e2+1) < Py(a,e2+1+1) by A11,XXREAL_0:2;
then
A18: (a-2)*e + e|^(e2+1) < e*n1 by A7,A10,XXREAL_0:2;
e|^(e2+1) = e* (e|^e2) by NEWTON:6;
then (a-2)*e + e|^(e2+1) = e* ( a-2 + (e|^e2));
then a-2 + (e|^e2) < n1 by A18,XREAL_1:64;
hence thesis by A3,INT_1:7;
end;
theorem Th6:
2 <= e & 0 <t implies
ex n,i st t divides n+1 & e^2 *(e *(e+2))*(n+1)^2 +1 = i^2
proof
set a=e+1, A=a^2-'1;
A1:a^2=a*a by SQUARE_1:def 1;
assume
A2: 2 <= e & 0 < t;
a*a>=0+1 by INT_1:7;
then
A3: A = a*a-1 by A1,XREAL_1:233
.= (a-1) *(a+1);
reconsider e2=e-2 as Nat by A2,NAT_1:21;
A4: (a-1)^2 =(a-1)*(a-1) & t^2=t*t by SQUARE_1:def 1;
then reconsider D=(a^2-'1) * (a-1)^2 *t^2 as non square Nat by A2;
consider x,y be Nat such that
A5: x^2 -D *y^2 =1 & y <>0 by PELLS_EQ:14;
A6: D*y^2 +1 = x^2 by A5;
reconsider n=t*y-1 as Nat by A2,A5;
take n,x;
y^2=y*y & e^2=e*e & (n+1)^2 = (n+1)*(n+1) by SQUARE_1:def 1;
hence thesis by A6,A3,INT_1:def 3,A4;
end;
theorem Th7:
n >=k implies n choose k >= (n+1-k) |^k /(k!)
proof
set n1=n+1;
defpred P[Nat] means $1 <= n implies n choose $1 >= (n1-$1) |^$1 /($1!);
n1 |^0 = 1 & n choose 0 = 1 & 0! =1 by NEWTON:4,12,19;
then
A1: P[0];
A2: P[i] implies P[i+1]
proof set i1=i+1;
assume
A3: P[i] & i+1 <=n;
then
A4: i <n by NAT_1:13;
A5: 0 < n-i by XREAL_1:50,A4;
n-i+1 > n-i by XREAL_1:29;
then (n1-i) |^i >= (n-i) |^i by A5,PREPOWER:9;
then (n1-i) |^i /(i!) >= (n-i) |^i/(i!) by XREAL_1:72;
then n choose i >= (n-i) |^i/(i!) by A3,NAT_1:13,XXREAL_0:2;
then
A6: ((n-i)/i1)*(n choose i) >= ((n-i)/i1)*((n-i) |^i/(i!))
by XREAL_1:64,A5;
((n-i)/i1)*((n-i) |^i/(i!)) = ((n-i)*((n-i) |^i))/(i1*(i!)) by XCMPLX_1:76
.= ((n-i) |^i1)/(i1*(i!)) by NEWTON:6
.= ((n-i) |^i1)/(i1!) by NEWTON:15;
hence thesis by A6,IRRAT_1:5;
end;
P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th8:
n >=k implies n choose k <= (n|^k) / (k!)
proof
defpred P[Nat] means $1 <= n implies n choose $1 <= (n|^$1) / ($1!);
n|^0 = 1 & n choose 0 = 1 & 0! =1 by NEWTON:4,12,19;
then
A1: P[0];
A2: P[i] implies P[i+1]
proof
set i1=i+1;
assume
A3: P[i] & i+1 <=n;
then
A4: i <n by NAT_1:13;
A5: 0 < n-i by XREAL_1:50,A4;
n-i <= n-0 by XREAL_1:10;
then (n-i)/i1 <= n /i1 by XREAL_1:72;
then
A6: ((n-i)/i1)*(n choose i) <= (n/i1)*((n|^i)/(i!))
by A5,NAT_1:13,A3,XREAL_1:66;
(n/i1)*((n|^i)/(i!)) = (n*(n|^i))/(i1*(i!)) by XCMPLX_1:76
.= (n|^i1)/(i1*(i!)) by NEWTON:6
.= (n|^i1)/(i1!) by NEWTON:15;
hence thesis by A6,IRRAT_1:5;
end;
P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th9:
i <= j & 2*j <= n+1 implies n choose i <= n choose j
proof
defpred P[Nat] means
i <= $1 & 2*$1 <= n+1 implies n choose i <= n choose $1;
A1: P[0];
A2: P[k] implies P[k+1]
proof
set k1=k+1;
assume
A3: P[k] & i <= k1 & 2*k1 <= n+1;
then per cases by XXREAL_0:1;
suppose i=k1;
hence thesis;
end;
suppose A4: i < k1;
k < k1 by NAT_1:13;
then
A5: 2*k <= 2*k1 by XREAL_1:66;
k1+k1 <= n+1 by A3;
then k1 <= n+1-k1 by XREAL_1:19;
then (n-k)/k1 >=1 by XREAL_1:181;
then ((n-k)/k1)*(n choose k) >= 1*(n choose k) by XREAL_1:66;
then n choose k1 >= n choose k by IRRAT_1:5;
hence thesis by A5,A4,NAT_1:13,A3,XXREAL_0:2;
end;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm2: n >0 implies k +n|^k <= (1+n) |^k
proof
assume
A1: n >0;
defpred P[Nat] means $1 +n|^$1 <= (1+n) |^$1;
n|^0 = 1 & (1+n) |^ 0 =1 by NEWTON:4;
then
A2: P[0];
A3: P[i] implies P[i+1]
proof
set i1=i+1;
A4: (1+n) |^i1 = (1+n) |^i * (1+n) & n|^i *n = n|^i1 by NEWTON:6;
assume P[i];
then
A5: (i+ n|^i) *(1+n) <= (1+n) |^i1 by A4,XREAL_1:66;
i*n + n|^i >= 0+1 by A1,NAT_1:14;
then i*n + n|^i + (i+ n|^i1) >= 1+(i+ n|^i1) by XREAL_1:7;
hence thesis by A4,A5,XXREAL_0:2;
end;
P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
Lm3: k < n implies 1 - (j*k)/n <= (1- k/n) |^j
proof
assume
A1: k <n;
defpred P[Nat] means 1 - $1*k/n <= (1- k/n) |^$1;
A2: P[0] by NEWTON:4;
A3: P[i] implies P[i+1]
proof
set i1=i+1;
n/n > k/n & n/n = 1 by A1,XCMPLX_1:60,XREAL_1:74;
then
A4: (1- k/n) >=0 by XREAL_1:50;
assume P[i];
then
A5: (1 - i*k/n)* (1- k/n) <= ((1- k/n) |^i)* (1- k/n) by A4,XREAL_1:64;
A6: 1 - i*k/n - k/n = 1 - (i*k/n + k/n)
.= 1 - ((i*k+k)/n) by XCMPLX_1:62
.= 1 - i1 *k/n;
(1 - i*k/n)*(1- k/n) = 1 - i*k/n - k/n + (i*k/n)*(k/n);
then (1 - i*k/n)*(1- k/n) >= 1 - i*k/n - k/n +0 by XREAL_1:7;
then 1 - i1*k/n <= ((1- k/n) |^i)* (1- k/n) by A6,A5,XXREAL_0:2;
hence thesis by NEWTON:6;
end;
P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
Lm4: k < n implies 1- k/n = (n-k)/n & 1/(1- k/n) = n / (n-k)
proof
assume k < n;
then 1 -k/n = (n/n) - k/n by XCMPLX_1:60
.= (n-k)/n by XCMPLX_1:120;
hence thesis by XCMPLX_1:57;
end;
Lm5: 0<2*k <= n implies 1 / (1-k/n) <= 1+(2*k)/n
proof
assume
A1: 0 < 2*k <= n;
then k+k > 0+k by XREAL_1:8;
then
A2: n >k by A1,XXREAL_0:2;
A3: n-k >0 by A2,XREAL_1:50;
n*k >= 2*k*k by A1,XREAL_1:64;
then 0 <= n*k - (2*k*k) by XREAL_1:48;
then n*n +0 <= n*n +(2*n*k - (k*n) - (2*k*k)) by XREAL_1:7;
then n*n<= (n+2*k)*(n-k);
then
A4: n/(n-k) <= (n+2*k)/n by A1,A3,XREAL_1:102;
(n+2*k)/n = n/n + (2*k)/n by XCMPLX_1:62
.= 1 +(2*k)/n by A1,XCMPLX_1:60;
hence thesis by A4,A2,Lm4;
end;
theorem Th10:
k <=n implies n! <= k! * n |^ (n-'k)
proof
assume
A1: k <=n;
then reconsider nk=n-k as Nat by NAT_1:21;
defpred P[Nat] means (k+$1)! <= k! * (k+$1) |^ $1;
(k+0) |^ 0 = 1 by NEWTON:4;
then
A2: P[0];
A3: P[i] implies P[i+1]
proof
set ki1=k+i+1;
assume
A4: P[i];
A5: (k+i) |^0 = 1 & ki1 |^0 = 1 by NEWTON:4;
A6: ki1 |^ i * ki1 = ki1 |^(i+1) by NEWTON:6;
k+i < ki1 & (i>=1 or i=0) by NAT_1:13,14;
then (k+i) |^ i <= ki1 |^i by A5,PREPOWER:10;
then k! * (k+i) |^ i <= k! *(ki1 |^i) by XREAL_1:66;
then
A7: (k+i)! <= k! *(ki1 |^i) by A4,XXREAL_0:2;
ki1! = (k+i)!* ki1 by NEWTON:15;
then ki1! <= (k! * ki1 |^ i) * ki1 by A7,XREAL_1:66;
hence thesis by A6;
end;
P[i] from NAT_1:sch 2(A2,A3);
then P[nk];
hence thesis by A1,XREAL_1:233;
end;
theorem Th11:
0 < k & (2*k) |^k <=n & n|^k < p implies
((p+1) |^n) mod (p|^(k+1)) >0 &
k! < ((n+1) |^ k * p|^k) / ( (p+1) |^n mod p|^(k+1)) < k!+1
proof
set k1=k+1, n1=n+1;
assume
A1: 0 <k & (2*k) |^k <=n & n|^k < p;
then
A2: 1<= k by NAT_1:14;
(2*k) |^k >= (2*k) |^1 by A1,NAT_6:1,NAT_1:14;
then
A3: 2*k <=n & k+0 < k+k by A1,XXREAL_0:2,XREAL_1:8;
then
A4: n<>0 & k < n by XXREAL_0:2;
then
A5: k <=n & 1 <=n & k1 <= n by NAT_1:13,14;
then
A6: k < n1 & k1 <= n1 by NAT_1:13;
n|^k >=1 by A4,NAT_1:14;
then 1<p by A1,XXREAL_0:2;
then
A7: 1+1 <=p by NAT_1:13;
reconsider K=k-1,nk=n-k as Nat by A3,XXREAL_0:2,A1,NAT_1:21;
set P = (1,p) In_Power n;
A8: len P = n+1 by NEWTON:def 4;
A9: Sum P = (1+p) |^n by NEWTON:30;
A10:Sum (P|k1), Sum P are_congruent_mod p|^k1
proof
defpred P[Nat] means k1 <= $1 <= len P implies
Sum (P|k1), Sum (P|$1) are_congruent_mod p|^k1;
A11: P[0];
A12: P[i] implies P[i+1]
proof
set i1=i+1;
assume that
A13: P[i] and
A14: k1 <= i1 <= len P;
per cases by A14,XXREAL_0:1;
suppose k1 = i1;
hence thesis by INT_1:11;
end;
suppose
A15: k1 <i1;
then
A16: k1 <= i <= len P by A14,NAT_1:13;
reconsider ni = n-i as Nat by A14,A8,NAT_1:21,XREAL_1:8;
A17: i1 in dom P by A14,FINSEQ_3:25,NAT_1:11;
then
A18: P|i1 = (P|i)^<*P.i1*> by FINSEQ_5:10;
i1-1=i & n-i = ni;
then
A19: P.i1 = (n choose i) * (1|^ni) * (p|^i) by A17,NEWTON:def 4;
p|^k1 divides P.i1-0 by A16,A19,INT_2:2,NEWTON:89;
then 0,P.i1 are_congruent_mod p|^k1 by INT_1:14,def 4;
then Sum (P|k1)+0, Sum (P|i)+P.i1 are_congruent_mod p|^k1
by A13,A15,A14,NAT_1:13,INT_1:16;
hence thesis by A18,RVSUM_1:74;
end;
end;
P[i] from NAT_1:sch 2(A11,A12);
then Sum (P|k1), Sum (P|len P) are_congruent_mod p|^k1 by A6,A8;
hence thesis;
end;
A20: Sum (P|k1)<>0
proof
assume Sum (P|k1)=0;
then p|^k1 divides 0 - Sum P by A10,INT_1:def 4;
then p|^k1 divides - ((1+p) |^n) by A9;
then
A21: p|^k1 divides (1+p) |^n by INT_2:10;
(1+p) |^n,p|^n are_coprime by PEPIN:1,WSIERP_1:11;
then
A22: ((1+p) |^n) gcd p|^n =1 by INT_2:def 3;
p|^k1 divides p |^n by A5,NEWTON:89;
then p|^k1 divides 1 by A21,A22,INT_2:def 2;
then p|^k1 =1 & p|^k1 > k1 by A7,NEWTON:86,INT_2:13;
hence thesis by NAT_1:14;
end;
A23: Sum (P|k1) < p|^k1
proof
defpred R[Nat] means $1 <= k1 implies Sum (P|$1) < p|^$1;
n|^k+1 <= p by A1,NAT_1:13;
then
A24: n|^k <= p-1 by XREAL_1:19;
reconsider p1=p-1 as Nat by A1;
A25: R[0];
A26: R[i] implies R[i+1]
proof
set i1=i+1;
assume
A27: R[i] & i1 <= k1;
then
A28: i < k1 by NAT_1:13;
A29: i1 <= n+1 by A6,A27,XXREAL_0:2;
then
A30: i <=n by XREAL_1:8;
reconsider ni = n-i as Nat by A29,XREAL_1:8,NAT_1:21;
1 <= i1 <= len P by A6,A8,A27,XXREAL_0:2,NAT_1:11;
then
A31: i1 in dom P by FINSEQ_3:25;
then
A32: P|i1 = (P|i)^<*P.i1*> by FINSEQ_5:10;
i1-1=i & n-i = ni;
then
A33: P.i1 = (n choose i) * (1|^ni) * (p|^i) by A31,NEWTON:def 4;
i<=k by A28,NAT_1:13;
then
A34: n|^i <= n|^k by A4,NAT_6:1;
n choose i <= n|^i by A30,HILB10_4:13;
then n choose i <= n|^k by A34,XXREAL_0:2;
then n choose i <= p-1 by A24,XXREAL_0:2;
then P.i1 <= p1 * (p|^i) by A33,XREAL_1:66;
then
A35: Sum (P|i) + P.i1 < (p|^i) + p1 * (p|^i) by NAT_1:13,A27,XREAL_1:8;
(p|^i) + p1 * (p|^i) = p * p|^i
.= p|^i1 by NEWTON:6;
hence thesis by A32,RVSUM_1:74,A35;
end;
R[i] from NAT_1:sch 2(A25,A26);
hence thesis;
end;
Sum (P|k1) mod p|^k1 = Sum P mod p|^k1 by A10,NAT_D:64;
then Sum P mod p|^k1 = Sum (P|k1) by A23,NAT_D:24;
then
A36: (1+p) |^n mod p|^k1 = Sum (P|k1) by NEWTON:30;
1 <= k1 <= len P by A5,NAT_1:13,A8,NAT_1:11;
then
A37: k1 in dom P by FINSEQ_3:25;
then P|k1 = (P|k)^<*P.k1*> by FINSEQ_5:10;
then
A38: Sum (P|k1) = Sum (P|k) + P.k1 by RVSUM_1:74;
k1-1=k & n-k = nk;
then
A39: P.k1 = (n choose k) * (1|^nk) * (p|^k) by A37,NEWTON:def 4;
n choose k <= (n|^k)/(k!) by A4,Th8;
then P.k1 <= (n|^k)/(k!) * (p|^k) by A39,XREAL_1:66;
then
A40: P.k1 <= ((p|^k)*(n|^k))/(k!) by XCMPLX_1:74;
A41: Sum (P|k) <= (n|^k) / (k!) *(p|^K)*k
proof
defpred R[Nat] means $1 <= k implies
Sum (P|$1) <= (n|^k) / (k!)*(p|^K)*$1;
A42: R[0];
A43: R[i] implies R[i+1]
proof
set i1=i+1;
assume
A44: R[i] & i1 <=k;
then
A45: i <k=K+1 by NAT_1:13;
then reconsider ni = n-i as Nat by NAT_1:21,A4,XXREAL_0:2;
A46: i1 <= n+1 by A44,A6,XXREAL_0:2;
1 <= i1 by NAT_1:11;
then
A47: i1 in dom P by A46,A8,FINSEQ_3:25;
then P|i1 = (P|i)^<*P.i1*> by FINSEQ_5:10;
then
A48: Sum (P|i1) = Sum (P|i) + P.i1 by RVSUM_1:74;
i1-1=i & n-i = ni;
then
A49: P.i1 = (n choose i) * (1|^ni) * (p|^i) by A47,NEWTON:def 4;
A50: i <= K by A45,NAT_1:13;
then
A51: p|^i <= p|^K by NAT_6:1,A1;
2*K <= 2*K+2 by NAT_1:11;
then 2*K <=n by A3,XXREAL_0:2;
then 2*K < n+1 by NAT_1:13;
then A52: n choose i <= n choose K by Th9,A50;
A53: (n|^K)*k <= (n|^K)*n = n|^(K+1) by A4,XREAL_1:66,NEWTON:6;
A54: K!*(K+1) = k! by NEWTON:15;
k/k=1 by A1,XCMPLX_1:60;
then (n|^K) / (K!) = ((n|^K) / (K!)) * (k/k)
.= ((n|^K)*k)/ (k!) by A54,XCMPLX_1:76;
then A55: (n|^K) / (K!) <= (n|^(K+1))/(k!) by A53,XREAL_1:72;
K+1=k <= n by A3,XXREAL_0:2;
then K < n by NAT_1:13;
then n choose K <= (n|^K) / (K!) by Th8;
then n choose i <= (n|^K) / (K!) by A52,XXREAL_0:2;
then n choose i <= (n|^k)/(k!) by A55,XXREAL_0:2;
then P.i1 <= (n|^k)/(k!) * (p|^K) by A49,A51,XREAL_1:66;
then Sum (P|i1) <= (n|^k) / (k!)*(p|^K)*i + (n|^k)/(k!) * (p|^K)
by A48,A44,NAT_1:13,XREAL_1:7;
hence thesis;
end;
R[i] from NAT_1:sch 2(A42,A43);
hence thesis;
end;
(p|^K) * p = p|^(K+1) by NEWTON:6;
then (p|^K)*k *p = k * (p|^k);
then
A56: (p|^K)*k * (n|^k) < k * (p|^k) by A1,XREAL_1:68;
(n|^k) / (k!) *(p|^K)*k = (n|^k) / (k!) *((p|^K)*k)
.= ((p|^K)*k * (n|^k))/ (k!) by XCMPLX_1:74;
then (n|^k) / (k!) *(p|^K)*k < k * (p|^k)/(k!) by A56,XREAL_1:74;
then Sum (P|k) < (k * (p|^k))/(k!) by A41,XXREAL_0:2;
then Sum (P|k) + P.k1 < (k * (p|^k))/(k!) + ((p|^k)*(n|^k))/(k!)
by A40,XREAL_1:8;
then Sum (P|k1) < (k * (p|^k) + (p|^k)*(n|^k))/(k!) by A38,XCMPLX_1:62;
then k!* Sum (P|k1) < k!*((k * (p|^k) + (p|^k)*(n|^k))/(k!)) by XREAL_1:68;
then
A57: k!* Sum (P|k1) < (k +n|^k)* (p|^k) by XCMPLX_1:87;
k +n|^k <= (1+n) |^k by A4,Lm2;
then (k +n|^k)* (p|^k) <= (1+n) |^k*(p|^k) by XREAL_1:66;
then k!* Sum (P|k1) < (1+n) |^k*(p|^k) by A57,XXREAL_0:2;
hence ((p+1) |^n) mod (p|^k1) >0 &
k! < ((n+1) |^ k * p|^k) / ( (p+1) |^n mod p|^k1) by A36,A20,XREAL_1:81;
A58: n1-k >0 by A6,XREAL_1:50;
n choose k >= (n1-k) |^k /(k!) by Th7,A4;
then
A59: (n1 |^k) / (n choose k) <= (n1 |^k)/ ((n1-k) |^k /(k!))
by A58,XREAL_1:118;
A60: (n1 |^k) / (((n1-k) |^k) /(k!)) = (k!) * ((n1 |^k) /((n1-k) |^k))
by XCMPLX_1:81;
A61: n1/n1 > k/n1 & n1/n1 = 1 by A6,XCMPLX_1:60,XREAL_1:74;
(n+1-k)/(n+1) = n1/n1 - k/n1 by XCMPLX_1:120
.= 1 - (k / n1) by XCMPLX_1:60;
then ((n1-k) |^k) / (n1 |^k) = (1 - (k / n1)) |^k by PREPOWER:8;
then
A62: ((n1 |^k) /((n1-k) |^k)) = 1 / ( (1 - (k / n1)) |^k) by XCMPLX_1:57;
A63:k*k <= n & 2*k*k <= n1
proof
A64: 4*(k*k) >= 1*(k*k) & 4*(k*k) >= 2*(k*k) by XREAL_1:64;
per cases by A2,XXREAL_0:1;
suppose k=1;
hence thesis by A5,NAT_1:13;
end;
suppose k >1;
then k>=1+1 by NAT_1:13;
then (2*k) |^k >= (2*k) |^2 = (2*k)*(2*k) by NAT_6:1,NEWTON:81;
then
A65: n >= (2*k)*(2*k) by A1,XXREAL_0:2;
then n1 >= 4*(k*k) by NAT_1:13;
hence thesis by A64,A65,XXREAL_0:2;
end;
end;
then k*k < n1 by NAT_1:13;
then 1 > (k*k) / n1 by A61,XREAL_1:74;
then
A66: 0 < 1 - (k*k)/n1 by XREAL_1:50;
1 - (k*k)/n1 <= (1 - (k / n1)) |^k by Lm3,A6;
then ((n1 |^k) /((n1-k) |^k)) <= 1 / (1 - (k*k)/n1 ) by A62,A66,XREAL_1:118;
then k!*((n1 |^k) /((n1-k) |^k)) <= k!* (1 / (1 - (k*k)/n1 )) by XREAL_1:64;
then
A67: (n1 |^k) / (n choose k) <= k!* (1 / (1 - (k*k)/n1 ))
by A59,A60,XXREAL_0:2;
n1 > (2*k) |^k & 2*k*k >0 & ((2*k) |^k) >0 by A1,NAT_1:13;
then (2*k*k)/n1 < (2*k*k)/((2*k) |^k) by XREAL_1:76;
then
A68: 1+(2*k*k)/n1 < 1+(2*k*k)/((2*k) |^k) by XREAL_1:8;
(1 / (1 - (k*k)/n1 )) <= 1+(2*(k*k))/n1 by Lm5,A1,A63;
then (1 / (1 - (k*k)/n1 )) < 1+(2*(k*k))/((2*k) |^k) by A68,XXREAL_0:2;
then k!* (1 / (1 - (k*k)/n1 )) < k!*(1+(2*(k*k))/((2*k) |^k)) by XREAL_1:68;
then
A69:(n1 |^k) / (n choose k) < k!*(1+(2*(k*k))/((2*k) |^k)) by A67,XXREAL_0:2;
A70: k! *(1+ 1/(k!)) = k! * 1+ k!*(1/(k!))
.= k!+ (k!)/(k!) by XCMPLX_1:74
.= k!+1 by XCMPLX_1:60;
A71: n choose k<>0 by CATALAN2:26,A4;
A72:k*k=k^2 by SQUARE_1:def 1;
1*(2*k) |^k >= 2*(k^2)*(k!)
proof
per cases by A2,XXREAL_0:1;
suppose k=1;
hence thesis by A72,NEWTON:13;
end;
suppose k >1;
then
A73: k>=1+1 by NAT_1:13;
then reconsider k2=k-2 as Nat by NAT_1:21;
k-'2 = k2 by A73,XREAL_1:233;
then k! <= 2!* k|^(k2) by A73,Th10;
then k!*k <= 2* k|^k2*k by XREAL_1:64,NEWTON:14;
then k!*k*k <= 2* k|^k2*k*k by XREAL_1:64;
then
A74: k!*k*k*2 <= 2* k|^k2*k*k*2 by XREAL_1:64;
A75: k|^(k2+1+1) = k* k|^(k2+1) by NEWTON:6
.= k* (k|^k2)*k by NEWTON:6;
2*2 = 2|^2 <= 2|^k by A73,NAT_6:1,NEWTON:81;
then (2*2)* (k|^k2*k*k) <= 2|^k * (k|^k) by A75,XREAL_1:64;
then k!*k*k*2 <= 2|^k * (k|^k)=(2*k) |^k by A74,XXREAL_0:2,NEWTON:7;
hence thesis by A72;
end;
end;
then 1/(k!) >= (2*(k^2)) / ((2*k) |^k) by A1,XREAL_1:102;
then 1+ 1/(k!) >= 1+ (2*(k^2)) / ((2*k) |^k) by XREAL_1:6;
then k! *(1+ 1/(k!)) >= k!* (1+ (2*(k^2)) / ((2*k) |^k)) by XREAL_1:66;
then
A76: (n1 |^k) / (n choose k) < k! +1 by A72,A70,A69,XXREAL_0:2;
Sum (P|k1) >= P.k1+0 by A38,XREAL_1:7;
then
A77: ((n1 |^k)* (p|^k)) / ((n choose k)* (p|^k)) >=
((n1 |^k)* (p|^k)) / Sum (P|k1) by A39,A71,A1,XREAL_1:118;
(n1 |^k) / (n choose k) = ((n1 |^k)* (p|^k)) / ((n choose k)* (p|^k))
by XCMPLX_1:91,A1;
hence thesis by A36,A76,A77,XXREAL_0:2;
end;
theorem Th12:
Px(a,n+2) = 2*a*Px(a,n+1) - Px(a,n) & Py(a,n+2) = 2*a*Py(a,n+1) - Py(a,n)
proof
set n1=n+1, d=a^2-'1;
a*a>=0+1 & a*a=a^2 by INT_1:7,SQUARE_1:def 1;
then
A1: a^2-'1 =a*a-1 by XREAL_1:233;
A2: Px(a,n1) = Px(a,n)*a + Py(a,n)*d & Py(a,n1) = Px(a,n) + Py(a,n)*a
by HILB10_1:6;
A3: Px(a,n1+1) = Px(a,n1)*a + Py(a,n1)*d &
Py(a,n1+1) = Px(a,n1) + Py(a,n1)*a by HILB10_1:6;
A4:a*Px(a,n1) - d*Py(a,n1) = Px(a,n) by A1,A2;
a*Py(a,n1) - Px(a,n1)= Py(a,n) by A1,A2;
hence thesis by A4,A3;
end;
theorem Th13:
Px(a,n), p|^n + Py(a,n)*(a-p) are_congruent_mod 2*a*p-p^2-1
proof
set D=a^2-'1;
set P=2*a*p-p^2-1;
defpred T[Nat] means
Px(a,$1) - Py(a,$1)*(a-p), p|^$1 are_congruent_mod P;
defpred P[Nat] means T[$1] & T[$1+1];
A1:P[0]
proof
A2: Px(a,0)= 1 & Py(a,0)= 0 & p|^0 =1 by HILB10_1:3,NEWTON:4;
Px(a,0+1) = Px(a,0)*a + Py(a,0)*D &
Py(a,0+1) = Px(a,0) + Py(a,0)*a by HILB10_1:6;
hence thesis by A2,INT_1:11;
end;
A3:P[k] implies P[k+1]
proof
set k1=k+1,k2=k1+1;
set X = Px(a,k), X1=Px(a,k1),X2=Px(a,k2);
set Y = Py(a,k), Y1=Py(a,k1),Y2=Py(a,k2);
assume
A4: P[k];
k2=k+2;
then
A5: X2 = 2*a*X1 - X & Y2 = 2*a*Y1 - Y by Th12;
A6: 2*a,2*a are_congruent_mod 2*a*p-p^2-1 by INT_1:11;
A7: 2*a*(X1 - Y1*(a-p)), 2*a*(p|^k1) are_congruent_mod P
by A4,A6,INT_1:18;
X2 - Y2*(a-p) = 2*a*(X1- Y1*(a-p)) - (X- Y*(a-p)) by A5;
then
A8: X2 - Y2*(a-p), 2*a*(p|^k1)-(p|^k) are_congruent_mod P
by A7,A4,INT_1:17;
A9: p|^k1= p*p|^k by NEWTON:6;
A10:(p^2)*(p|^k) = (p|^k)*(p|^2) by NEWTON:81
.= p|^ (k+2) by NEWTON:8;
A11: P = 2*a*p-1-p^2;
2*a*p -1, p^2 are_congruent_mod P &
(p|^k),(p|^k) are_congruent_mod P by A11,INT_1:def 4,11;
then (2*a*p -1)*(p|^k), p|^k2 are_congruent_mod P by A10,INT_1:18;
hence thesis by A4,A9,A8,INT_1:15;
end;
P[k] from NAT_1:sch 2(A1,A3);
then P divides Px(a,n)-Py(a,n)*(a-p) - p|^n by INT_1:def 4;
then P divides Px(a,n)- (p|^n + Py(a,n)*(a-p));
hence thesis by INT_1:def 4;
end;
theorem Th14:
0 < p|^n < a implies p|^n + Py(a,n)*(a-p) <= Px(a,n)
proof
assume
A1: 0 < p|^n < a;
A2: Px(a,0)= 1 & Py(a,0)= 0 & p|^0 =1 by HILB10_1:3,NEWTON:4;
A3: Py(a,0+1) = 1+0*a & Px(a,0+1) = 1*a +0 *(a^2-'1) by A2,HILB10_1:6;
A4: Py(a,1+1) = Px(a,1) + Py(a,1)*a by HILB10_1:6;
A5: a*a>=0+1 & a*a =a^2 by INT_1:7,SQUARE_1:def 1;
Px(a,n)^2 - (a^2-'1) *Py(a,n)^2 = 1 by HILB10_1:7;
then
A6: Px(a,n)^2 = (a^2-'1) *Py(a,n)^2 +1;
A7: ((a-1) *Py(a,n))^2=((a-1) *Py(a,n))* ((a-1) *Py(a,n)) &
Py(a,n)^2 = Py(a,n)* Py(a,n) by SQUARE_1:def 1;
- (2*a - 1) <= -1 by XREAL_1:24,NAT_1:14;
then
A8: a^2+-(2*a -1) <= a^2+-1 & (a-1)^2=(a-1)*(a-1)
by XREAL_1:6,SQUARE_1:def 1;
then (a-1)^2 *Py(a,n)^2 <= (a^2-1)*Py(a,n)^2 by A5,XREAL_1:64;
then ((a-1) *Py(a,n))^2 <= (a^2-'1)*Py(a,n)^2 by A8,A7,XREAL_1:233,A5;
then ((a-1) *Py(a,n))^2 < Px(a,n)^2 by A6,NAT_1:13;
then
A9: (a-1) *Py(a,n) < Px(a,n) by SQUARE_1:15;
per cases by NAT_1:23;
suppose n=0 or n=1;
hence thesis by A2,A3;
end;
suppose p=1;
hence thesis by A9,INT_1:7;
end;
suppose
A10: n >=1+1 & p <>1;
then n>=1 by NAT_1:13;
then p<>0 by A1,NEWTON:11;
then
A11: Py(a,n)*p >= Py(a,n)*2 by XREAL_1:64,A10,NAT_1:23;
n >2 or n=2 by A10,XXREAL_0:1;
then Py(a,n) > Py(a,2) or Py(a,n) = Py(a,2) by HILB10_1:11;
then Py(a,n)+Py(a,n) >= Py(a,n)+(a+a) by A3,A4,XREAL_1:6;
then
A12: Py(a,n)*p >= Py(a,n)+(a+a) by A11,XXREAL_0:2;
Py(a,n)+a+a >= Py(a,n)+a+1 by NAT_1:14, XREAL_1:6;
then Py(a,n)*p >= Py(a,n)+a+1 by A12,XXREAL_0:2;
then Py(a,n)*p > Py(a,n)+a by NAT_1:13;
then -(Py(a,n)*p -a) < - Py(a,n) by XREAL_1:20,24;
then Py(a,n)*a + -(Py(a,n)*p -a) < Py(a,n)*a + - Py(a,n) by XREAL_1:8;
then
A13: Py(a,n)*(a - p) +a < Px(a,n) by A9,XXREAL_0:2;
Py(a,n)*(a - p) +a > Py(a,n)*(a - p) + p|^n by A1, XREAL_1:8;
hence thesis by A13,XXREAL_0:2;
end;
end;
theorem Th15:
a <= b implies Px(a,n) <= Px(b,n) & Py(a,n) <= Py(b,n)
proof
assume
A1: a <=b;
defpred P[Nat] means Px(a,$1) <= Px(b,$1) & Py(a,$1) <= Py(b,$1);
Px(a,0) = 1 & Py(a,0) = 0 &
Px(b,0) = 1 & Py(b,0) = 0 by HILB10_1:3;
then
A2: P[0];
A3: P[k] implies P[k+1]
proof
assume
A4: P[k];
set k1=k+1;
A5: a*a =a^2 & b*b=b^2 by SQUARE_1:def 1;
then a^2>=1+0 & b^2>=1+0 by NAT_1:13;
then
A6: a^2-'1 = a^2-1 & b^2-'1 = b^2-1 by XREAL_1:233;
a^2 <= b^2 by A5,A1,XREAL_1:66;
then
A7: a^2-'1 <= b^2-'1 by A6,XREAL_1:9;
Px(a,k)*a <= Px(b,k)*b & Py(a,k)*(a^2-'1) <= Py(b,k)*(b^2-'1)
by A1,A7,A4,XREAL_1:66;
then Px(a,k1)= Px(a,k)*a + Py(a,k)*(a^2-'1) <=
Px(b,k)*b + Py(b,k)*(b^2-'1) by XREAL_1:7,HILB10_1:6;
hence Px(a,k1)<=Px(b,k1) by HILB10_1:6;
Py(a,k)*a <= Py(b,k)*b by A1,A4,XREAL_1:66;
then Py(a,k1)=Px(a,k) + Py(a,k)*a <= Px(b,k) + Py(b,k)*b
by A4,XREAL_1:7,HILB10_1:6;
hence thesis by HILB10_1:6;
end;
P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th16:
a,b are_congruent_mod k implies Px(a,n),Px(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 = Px(a,n)-Px(b,n) by HILB10_1:25,INT_1:def 5;
p*(a-b) = p*(x*k) by A1
.= p*x*k;
hence thesis by A2, INT_1:def 5;
end;
theorem Th17:
Px(a,|.2*x+y.|),- Px(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 Px(a,|.2*i+j.|) = Px(a,|.i.|)*Px(a,|.i+j.|) +
A * sgn(i)*Py(a,|.i.|)*sgn(i+j)*Py(a,|.i+j.|) by HILB10_1:22;
then Px(a,|.i.|)*Px(a,|.i+j.|) =
Px(a,|.2*i+j.|) - A * sgn(i)*Py(a,|.i.|)*sgn(i+j)*Py(a,|.i+j.|);
then
A1: Px(a,|.2*i+j.|) , A * sgn(i)*Py(a,|.i.|)*sgn(i+j)*Py(a,|.i+j.|)
are_congruent_mod Px(a,|.i.|) by INT_1:def 5;
sgn(i+j)*Py(a,|.i+j.|) = Px(a,|.i.|)*sgn(j)*Py(a,|.j.|) +
sgn(i)*Py(a,|.i.|)*Px(a,|.j.|) by HILB10_1:22;
then Px(a,|.i.|)*(sgn(j)*Py(a,|.j.|)) =
sgn(i+j)*Py(a,|.i+j.|) - sgn(i)*Py(a,|.i.|)*Px(a,|.j.|);
then sgn(i+j)*Py(a,|.i+j.|) , sgn(i)*Py(a,|.i.|)*Px(a,|.j.|)
are_congruent_mod Px(a,|.i.|) by INT_1:def 5;
then
A2: (A * sgn(i)*Py(a,|.i.|))*(sgn(i+j)*Py(a,|.i+j.|)),
(A * sgn(i)*Py(a,|.i.|))* (sgn(i)*Py(a,|.i.|)*Px(a,|.j.|))
are_congruent_mod Px(a,|.i.|) by INT_4:11;
A3: (A * sgn(i)*Py(a,|.i.|))* (sgn(i)*Py(a,|.i.|)*Px(a,|.j.|)) =
A* (Py(a,|.i.|)*Py(a,|.i.|))*Px(a,|.j.|)
proof
per cases;
suppose i=0;
then sgn(i)=0 & Py(a,|.i.|) = 0 by ABSVALUE:def 2,HILB10_1:3;
hence thesis;
end;
suppose i<>0;
then
A4: sgn(i)*sgn(i) = sgn (i*i) &i*i >0 by ABSVALUE:18;
(A * sgn(i)*Py(a,|.i.|))* (sgn(i)*Py(a,|.i.|)*Px(a,|.j.|)) =
(A * (sgn(i)*sgn(i)))*Py(a,|.i.|)* Py(a,|.i.|)*Px(a,|.j.|)
.= (A * 1)*Py(a,|.i.|)* Py(a,|.i.|)*Px(a,|.j.|) by A4,ABSVALUE:def 2
.= (A * 1)*(Py(a,|.i.|)* Py(a,|.i.|))*Px(a,|.j.|);
hence thesis;
end;
end;
A5: Py(a,|.i.|)^2 =Py(a,|.i.|)*Py(a,|.i.|) by SQUARE_1:def 1;
A6: Px(a,|.i.|)^2 =Px(a,|.i.|)*Px(a,|.i.|) by SQUARE_1:def 1;
Px(a,|.i.|)^2 - A *Py(a,|.i.|)^2 = 1 by HILB10_1:7;
then
A7: Px(a,|.2*i+j.|), (Px(a,|.i.|)^2-1)*Px(a,|.j.|)
are_congruent_mod Px(a,|.i.|) by A5,A3,A2,A1,INT_1:15;
Px(a,|.i.|)*(Px(a,|.i.|)*Px(a,|.j.|))
=(Px(a,|.i.|)^2-1)*Px(a,|.j.|) -- (Px(a,|.j.|)) by A6;
then (Px(a,|.i.|)^2-1)*Px(a,|.j.|),- (Px(a,|.j.|))
are_congruent_mod Px(a,|.i.|) by INT_1:def 5;
hence thesis by A7,INT_1:15;
end;
theorem Th18:
Px(a,|.4*x+y.|), Px(a,|.y.|) are_congruent_mod Px(a,|.x.|)
proof
A1: Px(a,|.2*x+y.|) * (-1),(- Px(a,|.y.|))*(-1)
are_congruent_mod Px(a,|.x.|) by Th17,INT_4:11;
Px(a,|.2*x+(2*x+y).|),- Px(a,|.2*x+y.|)
are_congruent_mod Px(a,|.x.|) by Th17;
hence thesis by A1,INT_1:15;
end;
Lm6: i <=j <n & i,j are_congruent_mod n implies i=j
proof
assume
A1: i <=j < n & i,j are_congruent_mod n;
then consider x such that
A2: n*x = i-j by INT_1:def 5;
i -j <= i-0 & i < n by XREAL_1:10,A1,XXREAL_0:2;
then n*x < n*1 by A2,XXREAL_0:2;
then
A3: x < 0+1 by XREAL_1:64;
i-j >= 0-j & -j > -n by XREAL_1:9,24,A1;
then n*x > n*(-1) by A2,XXREAL_0:2;
then x > -1 by XREAL_1:64;
then x >= -1+1 by INT_1:7;
then x=0 by A3,INT_1:7;
hence thesis by A2;
end;
Lm7: i <n & j <n & i,j are_congruent_mod n implies i=j
proof
assume
A1: i <n & j <n & i,j are_congruent_mod n;
i <=j or j < i;
hence thesis by A1,INT_1:14,Lm6;
end;
theorem Th19:
k < n implies Px(a,k) < Px(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 Px(a,k) < Px(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: Px(a,k+i+1) = Px(a,k+i)*a+Py(a,k+i)*(a^2-'1) by HILB10_1:6;
Px(a,k+i) >= Px(a,0) by HILB10_1:10;
then Px(a,k+i) >= 1 by HILB10_1:3;
then
A7: Px(a,k+i)+Px(a,k+i) >= Px(a,k+i)+1 by XREAL_1:7;
Px(a,k+i)*a >= Px(a,k+i)*2 by NAT_2:29,XREAL_1:64;
then Px(a,k+i+1) >= Px(a,k+i)*2+0 by A6,XREAL_1:7;
then
A8: Px(a,k+i+1) >= Px(a,k+i)+1 by A7,XXREAL_0:2;
then
A9: Px(a,k+i+1) > Px(a,k+i) by NAT_1:13;
per cases;
suppose i=0;
hence thesis by A8,NAT_1:13;
end;
suppose i >0;
hence thesis by A5,A9,XXREAL_0:2;
end;
end;
P[n1] from NAT_1:sch 2(A3,A4);
then Px(a,k) < Px(a,k+nk) by A2;
hence thesis;
end;
theorem Th20:
Px(a,k) = Px(a,n) implies k = n
proof
k < n or n <k or k=n by XXREAL_0:1;
hence thesis by Th19;
end;
Lm8: Px(a,i),Px(a,j) are_congruent_mod Px(a,n) & i <n & j < n
implies i=j
proof
assume
A1: Px(a,i),Px(a,j) are_congruent_mod Px(a,n) & i < n & j < n;
then Px(a,i) < Px(a,n) & Px(a,j) < Px(a,n) by Th19;
then
A2: Px(a,i) = Px(a,j) by Lm7,A1;
i<j or i=j or j<i by XXREAL_0:1;
hence thesis by A2,Th19;
end;
Lm9: i < n & not (a=2 & n=1) implies Px(a,i) < Px(a,n)/2
proof
assume
A1: i <n & not (a=2 & n=1);
then reconsider n1=n-1 as Nat;
n=n1+1;
then
A2: Px(a,n) = Px(a,n1)*a+Py(a,n1)*(a^2-'1) by HILB10_1:6;
then
A3: Px(a,n) >= Px(a,n1)*a+0 by XREAL_1:7;
i <n1+1 by A1;
then i <= n1 by NAT_1:13;
then Px(a,i) <= Px(a,n1) by HILB10_1:10;
then
A4: Px(a,i)*a <= Px(a,n1)*a by XREAL_1:64;
a >1 by NEWTON03:def 1;
then
A5: a >= 1+1 by NAT_1:13;
per cases by A5,XXREAL_0:1;
suppose
A6: a=2;
then n > 1 or n < 1 by A1,XXREAL_0:1;
then n-1 >1-1 by XREAL_1:9,A1,NAT_1:14;
then Px(a,n) > Px(a,n1)*a+0 by A2,XREAL_1:8;
then Px(a,n) > Px(a,i)*2 by A6,A4,XXREAL_0:2;
hence thesis by XREAL_1:81;
end;
suppose a>2;
then
A7: Px(a,i)*a > Px(a,i)*2 by XREAL_1:68;
Px(a,i)*a <= Px(a,n) by A4,A3,XXREAL_0:2;
then Px(a,n) > Px(a,i)*2 by A7,XXREAL_0:2;
hence thesis by XREAL_1:81;
end;
end;
Lm10:
Px(a,i),Px(a,j) are_congruent_mod Px(a,n) & n < i <= 2*n & n < j <= 2*n
implies i=j
proof
set P = Px(a,n);
assume
A1: Px(a,i),Px(a,j) are_congruent_mod P & n < i <= 2*n & n < j <= 2*n;
then reconsider i2n= 2*n-i,j2n = 2*n-j as Nat by NAT_1:21;
A2: P, P are_congruent_mod P by INT_1:11;
2*n+-i2n = i & 2*n+-j2n = j;
then
A3: Px(a,|.i.|),- Px(a,|.-i2n.|) are_congruent_mod Px(a,|.n.|)&
Px(a,|.j.|),- Px(a,|.-j2n.|) are_congruent_mod Px(a,|.n.|) by Th17;
then - Px(a,i2n),Px(a,i) are_congruent_mod P&
Px(a,|.j.|),- Px(a,|.-j2n.|) are_congruent_mod P by INT_1:14;
then - Px(a,i2n),Px(a,j) are_congruent_mod P by A1,INT_1:15;
then - Px(a,i2n),-Px(a,j2n) are_congruent_mod P by A3,INT_1:15;
then
A4: - Px(a,i2n)+P,-Px(a,j2n)+P are_congruent_mod P by A2,INT_1:16;
2*n-i <= 2*n-n & 2*n-j <= 2*n-n by A1,XREAL_1:15;
then reconsider Pi=P- Px(a,i2n), Pj=P- Px(a,j2n) as Nat
by NAT_1:21,HILB10_1:10;
Pi < P-0 & Pj < P-0 by XREAL_1:15;
then Pi = Pj by Lm7,A4;
then i2n = j2n by Th20;
hence thesis;
end;
theorem Th21:
i <= j <= 2*n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n)
implies (i=0 & j = 2 & a=2 & n=1) or i=j
proof
set P=Px(a,n);
assume
A1: i <= j <= 2*n & Px(a,i),Px(a,j) are_congruent_mod P
& not (i=0 & j = 2 & a=2 & n=1) & i<>j;
reconsider j2n = 2*n-j as Nat by A1,NAT_1:21;
A2: 0,P are_congruent_mod P by INT_1:12;
A3: i <= 2*n by A1,XXREAL_0:2;
i<n or i=n or n <i by XXREAL_0:1;
then per cases by A1,XXREAL_0:1,2;
suppose i < n & j < n;
hence thesis by A1,Lm8;
end;
suppose
A4: i < n & j = n;
then P,Px(a,i) are_congruent_mod P by A1,INT_1:14;
then
A5: P-P,Px(a,i) are_congruent_mod P by INT_1:22;
Px(a,i) <P by A4,Th19;
then 0 = Px(a,i) by A5,Lm7;
hence thesis;
end;
suppose
A6: i < n & j > n;
2*n + -j2n = j;
then Px(a,|.j.|),- Px(a,|.-j2n.|) are_congruent_mod Px(a,|.n.|) by Th17;
then Px(a,|.i.|),-Px(a,j2n) are_congruent_mod P by A1,INT_1:15;
then
A7: Px(a,|.i.|)+0,-Px(a,j2n)+P are_congruent_mod P by A2,INT_1:16;
A8: 2*n-j < 2*n-n by A6,XREAL_1:15;
then reconsider Pj=P- Px(a,j2n) as Nat by NAT_1:21,HILB10_1:10;
A9: Px(a,i) < P by A6,Th19;
Pj < P-0 by XREAL_1:15;
then
A10: Px(a,i) = Pj by A9,A7,Lm7;
per cases;
suppose not (a=2 & n=1);
then Px(a,i) < P/2 & Px(a,j2n) < P/2 by A6,A8,Lm9;
then Px(a,i) +Px(a,j2n) < P/2 +P/2 = P by XREAL_1:8;
hence thesis by A10;
end;
suppose
A11: a=2 & n=1;
then i=0 & j >= 1+1 by A6,NAT_1:13,14;
hence thesis by A1,A11,XXREAL_0:1;
end;
end;
suppose
A12: i = n & j >n;
2*n + -j2n = j;
then Px(a,|.j.|),- Px(a,|.-j2n.|) are_congruent_mod Px(a,|.n.|) by Th17;
then P,-Px(a,j2n) are_congruent_mod P by A12,A1,INT_1:15;
then P+0,-Px(a,j2n)+P are_congruent_mod P by A2,INT_1:16;
then
A13: P-P,-Px(a,j2n)+P are_congruent_mod P by INT_1:22;
2*n-j <= 2*n-n by A12,XREAL_1:15;
then reconsider Pj=P- Px(a,j2n) as Nat by NAT_1:21,HILB10_1:10;
Pj < P-0 by XREAL_1:15;
then 0 = Pj by A13,Lm7;
then 2*n-j = n by Th20;
hence thesis by A12;
end;
suppose i > n & j >n;
hence thesis by A1,Lm10,A3;
end;
end;
theorem Th22:
0 < i <= n & 0 <= j < 4*n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n)
implies j = i or j + i = 4*n
proof
set P=Px(a,n);
assume
A1: 0 < i <= n & 0 <= j < 4*n & Px(a,i),Px(a,j) are_congruent_mod P;
then
A2: Px(a,j),Px(a,i) are_congruent_mod P by INT_1:14;
reconsider j4n = 4*n-j as Nat by A1,NAT_1:21;
Px(a,|.4*n+-j4n.|), Px(a,|.-j4n.|) are_congruent_mod Px(a,|.n.|) by Th18;
then
A3: Px(a,i),Px(a,j4n) are_congruent_mod P by A1,INT_1:15;
then
A4: Px(a,j4n),Px(a,i) are_congruent_mod P by INT_1:14;
n<= n+n by NAT_1:11;
then
A5: i<= n+n by A1,XXREAL_0:2;
per cases;
suppose
A6: j <= 2*n;
per cases;
suppose i <=j;
hence thesis by A6,Th21,A1;
end;
suppose j < i;
then (j=0 & i = 2 & a=2 & n=1) or j=i by A6,Th21,A5,A2;
hence thesis by A1;
end;
end;
suppose
A7: j > 2*n;
then
A8: j4n < 4*n-2*n by XREAL_1:10;
per cases;
suppose
i <=j4n;
then i=j4n by A3,A8,Th21,A1;
hence thesis;
end;
suppose j4n < i;
then (j4n=0 & i = 2 & a=2 & n=1) or j4n=i by A4,A7,Th21,A5;
hence thesis by A1;
end;
end;
end;
theorem Th23:
Px(a,|.4*x*n+y.|), Px(a,|.y.|) are_congruent_mod Px(a,|.x.|)
proof
defpred P[Nat] means Px(a,|.4*x*$1+y.|), Px(a,|.y.|)
are_congruent_mod Px(a,|.x.|);
A1: P[0] by INT_1:11;
A2: P[k] implies P[k+1]
proof
Px(a,|.4*x+(4*x*k+y).|), Px(a,|.4*x*k+y.|)
are_congruent_mod Px(a,|.x.|)by Th18;
hence thesis by INT_1:15;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th24:
0 < i <= n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n)
implies j,i are_congruent_mod 4*n or j,-i are_congruent_mod 4*n
proof
set m = j mod (4*n), d = j div (4*n);
assume
A1: 0 < i <= n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n);
then
A2: j= d*(4*n) + m by INT_1:59;
then
A3: Px(a,|.j.|),Px(a,|.m.|) are_congruent_mod Px(a,|.n.|) by Th23;
m < 4*n by A1,INT_1:58;
then per cases by A3,Th22,A1,INT_1:15;
suppose m=i;
then (4*n) divides (j-i) by A1,PEPIN:8;
hence thesis by INT_2:15;
end;
suppose m + i = 4*n;
then (4*n) divides (m--i);
then
A4: m,-i are_congruent_mod 4*n by INT_2:15;
j-m =d*(4*n) by A2;
then j,m are_congruent_mod 4*n by INT_1:def 5;
hence thesis by A4,INT_1:15;
end;
end;
theorem Th25:
Py(a,2*n) = 2* Py(a,n)*Px(a,n)
proof
A1:Py(a,0)=0 by HILB10_1:3;
per cases;
suppose n=0;
hence thesis by A1;
end;
suppose n>0;
then
A2: sgn(n)=1 & sgn(n+n) =1 by ABSVALUE:def 2;
sgn(n+n)*Py(a,|.n+n.|) = Px(a,|.n.|)*sgn(n)*Py(a,|.n.|) +
sgn(n)*Py(a,|.n.|)*Px(a,|.n.|) by HILB10_1:22;
hence thesis by A2;
end;
end;
begin :: Special Case of Pell's Equation - Diophantine Polynomial With 8 Variables
theorem Th26:
for a being non trivial Nat
for y,n,b,c,d,r,s,t,u,v,x being Nat st 1 <= n &
[x,y] is Pell's_solution of a^2-'1 &
[u,v] is Pell's_solution of a^2-'1 &
[s,t] is Pell's_solution of b^2-'1 &
v = 4*r*y^2 &
b = a +u^2*(u^2-a) &
s = x+c*u &
t = n+4*d*y &
n <= y
holds b is non trivial & u^2 > a & y = Py(a,n)
proof
let a being non trivial Nat;
let y,n,b,c,d,r,s,t,u,v,x being Nat such that
A1: 1 <= n and
A2: [x,y] is Pell's_solution of a^2-'1 and
A3: [u,v] is Pell's_solution of a^2-'1 and
A4: [s,t] is Pell's_solution of b^2-'1 and
A5: v= 4*r*y^2 and
A6: b = a +u^2*(u^2-a)and
A7: s= x+c*u and
A8: t=n+4*d*y and
A9: n <= y;
A10: s^2 - (b^2-'1) *t^2 =1 by Lm1,A4;
consider i be Nat such that
A11: x = Px(a,i) & y = Py(a,i) by A2,HILB10_1:4;
A12: Px(a,i)^2 - (a^2-'1) *Py(a,i)^2 = 1 by HILB10_1:7;
consider n1 be Nat such that
A13: u = Px(a,n1) & v = Py(a,n1) by A3,HILB10_1:4;
A14: Px(a,n1)^2 - (a^2-'1) *Py(a,n1)^2 = 1 by HILB10_1:7;
then Px(a,n1)^2 = (a^2-'1) *Py(a,n1)^2 +1;
then
A15: u^2 = (a^2-'1)*v^2+1 by A13;
A16:Px(a,0) = 1 & Py(a,0) = 0 by HILB10_1:3;
then
A17: Px(a,0+1) = 1*a + 0*(a^2-'1) &
Py(a,0+1) = 1 + 0*a by HILB10_1:6;
A18: Px(a,n1)^2=Px(a,n1)*Px(a,n1) & Py(a,n1)^2=Py(a,n1)*Py(a,n1)
by SQUARE_1:def 1;
A19: Px(a,i)^2=Px(a,i)*Px(a,i) & Py(a,i)^2=Py(a,i)*Py(a,i) by SQUARE_1:def 1;
A20: v<>0
proof
assume
A21: v=0;
then
A22: u=1 by A18,A13, A14,NAT_1:15;
A23: u^2=1*1 by A21,A18,A13,A14;
b^2=b*b by SQUARE_1:def 1;
then b^2-'1 = 0 by A23,A6,XREAL_1:232;
then s*s=1 by A10,SQUARE_1:def 1;
then 1 = x+c*1 by A22,A7, NAT_1:15;
then x = 1 by A11,GAUSSINT:1;
then y*y=0 by A19,A12,A11;
hence thesis by A9,A1;
end;
then n1<>0 by A13,HILB10_1:3;
then n1 >= 1+0 by NAT_1:13;
then
A24: a <= u by A13,A17,HILB10_1:10;
u > 1 by NEWTON03:def 1,A24,XXREAL_0:2;
then
A25: a*1 < u*u & u^2=u*u by A24,XREAL_1:97,SQUARE_1:def 1;
then
A26: u^2-a > 0 & u^2 >0 by XREAL_1:50;
then reconsider B=b as non trivial Nat by A6;
consider j be Nat such that
A27: s = Px(B,j) & t = Py(B,j) by A4,HILB10_1:4;
r>0 by A5,A20;
then
A28: r >= 0+1 by NAT_1:13;
y >=1 by A9,A1,XXREAL_0:2;
then y*y >= y*1 by XREAL_1:66;
then r*(y*y) >= y*1 by A28,XREAL_1:66;
then
A29: 4*(r*(y*y)) >= y*1 by XREAL_1:66;
u^2=u*u by SQUARE_1:def 1;
then b-a = u*(u*(u^2-a)) by A6;
then
A30: Px(B,j),Px(a,j) are_congruent_mod Px(a,n1) by Th16,A13,INT_1:def 5;
A31: i>0 by A9,A1,A16,A11;
x-s = u*(-c) by A7;
then Px(a,i),Px(B,j) are_congruent_mod Px(a,n1) by A11,A13,A27,INT_1:def 5;
then Px(a,i),Px(a,j) are_congruent_mod Px(a,n1) by A30,INT_1:15;
then
A32: j,i are_congruent_mod 4*n1 or j,-i are_congruent_mod 4*n1
by A31,A29,A5,HILB10_1:11,A13,Th24,A11,A19;
Py(a,i)^2 divides Py(a,n1) by A5,A11,A13,INT_1:def 3;
then consider divN be Nat such that
A33: Py(a,i)*divN = n1 by NAT_D:def 3,HILB10_1:37;
4*n1 = 4*Py(a,i)*divN by A33;
then
A34: j,i are_congruent_mod 4*Py(a,i) or j,-i are_congruent_mod 4*Py(a,i)
by A32,INT_1:20;
b-1 = (4*y)*((a^2-'1)*(4*r*y^2)*(r*y)*((a^2-'1)*(4*r*y^2)^2 + 2 -a))
by A6,A15,A5,A11,A13,A18,A19;
then
A35: Py(B,j),j are_congruent_mod 4*Py(a,i) by HILB10_1:24,A11,INT_1:20;
Py(B,j)-n = 4*Py(a,i)*d by A11,A27,A8;
then n,Py(B,j) are_congruent_mod 4*Py(a,i) by INT_1:14,def 5;
then n,j are_congruent_mod 4*Py(a,i) by A35,INT_1:15;
then
A36: n,i are_congruent_mod 4*Py(a,i) or n,-i are_congruent_mod 4*Py(a,i)
by A34,INT_1:15;
A37: 1*Py(a,i) < 4*Py(a,i) by A9,A1,A11,XREAL_1:97;
A38:n < 4*Py(a,i) by A11,A9,A37,XXREAL_0:2;
A39: i <= Py(a,i) by HILB10_1:13;
then reconsider Pi = 4*Py(a,i)-i as Nat by NAT_1:21,A37,XXREAL_0:2;
A40: i < 4*Py(a,i) by A39,A37,XXREAL_0:2;
A41: 4*Py(a,i)+-i < 4*Py(a,i)+0 by A31,XREAL_1:8;
n=i
proof
assume n<>i;
then -i,n are_congruent_mod 4*Py(a,i) by INT_1:14,A36,A38,A40,Lm7;
then
A42: Pi =n by A41,A38,Lm7,INT_1:21;
A43: 4*Py(a,i)-i >= 4*Py(a,i)-Py(a,i) by HILB10_1:13,XREAL_1:10;
Py(a,i)+Py(a,i)+Py(a,i) > Py(a,i) + 0 by A9,A1,XREAL_1:8,A11;
hence thesis by A42,A11,A9,A43,XXREAL_0:2;
end;
hence thesis by A26,A6,A25,A11;
end;
theorem Th27:
for a be non trivial Nat for y,n be Nat st 1 <=n holds
y = Py(a,n) implies
ex b,c,d,r,s,t,u,v,x be Nat st
[x,y] is Pell's_solution of a^2-'1 &
[u,v] is Pell's_solution of a^2-'1 &
[s,t] is Pell's_solution of b^2-'1 &
v = 4*r*y^2 &
b =a +u^2*(u^2-a) &
s = x+c*u &
t = n+4*d*y &
n <= y
proof
let a be non trivial Nat;
let y,n be Nat such that
A1: n>=1 and
A2: y= Py(a,n);
set x = Px(a,n), m = 4*n*y,u = Px(a,m),v=Py(a,m);
A3: x^2 - (a^2-'1) *y^2 = 1 by A2,HILB10_1:7;
A4: u^2 - (a^2-'1) *(v^2) = 1 by HILB10_1:7;
A5: Py(a,n*y), y * (x |^ (y-'1)) *y are_congruent_mod y^2 by A2,HILB10_1:35;
y^2=y*y by SQUARE_1:def 1;
then y * (x |^ (y-'1)) *y= y^2*(x |^ (y-'1));
then y * (x |^ (y-'1)) *y,0 are_congruent_mod y^2 by INT_1:60;
then y^2 divides Py(a,n*y)-0 by A5,INT_1:15,INT_1:def 4;
then consider R be Nat such that
A6: y^2*R = Py(a,n*y) by NAT_D:def 3;
set r= R * Px(a,n*y) * Px(a,n*y*2);
A7: Py(a,n*y*2) = 2*Py(a,n*y)*Px(a,n*y) by Th25;
A8: Py(a,n*y*2*2) = 2*Py(a,n*y*2)*Px(a,n*y*2) by Th25;
Px(a,0) = 1 & Py(a,0) = 0 by HILB10_1:3;
then
A9: Px(a,0+1) = 1*a + 0*(a^2-'1) & Py(a,0+1) = 1 + 0*a by HILB10_1:6;
A10: m>=1+0 by A1,A2,NAT_1:13;
then
A11: a <= u by A9,HILB10_1:10;
then u > 1 by NEWTON03:def 1,XXREAL_0:2;
then
A12: a*1 < u*u & u^2=u*u by A11,XREAL_1:97,SQUARE_1:def 1;
then
A13: u^2-a > 0 by XREAL_1:50;
then reconsider b=a +u^2*(u^2-a) as non trivial Nat by A12;
set s = Px(b,n),t=Py(b,n);
A14: s^2 - (b^2-'1) *(t^2) = 1 by HILB10_1:7;
b-a = u*(u*(u^2-a)) by A12;
then s,x are_congruent_mod u by Th16,INT_1:def 5;
then consider c be Integer such that
A15: u*c = s-x by INT_1:def 5;
b > a+0 by A13,A12,XREAL_1:8;
then c >=0 by Th15,A15,XREAL_1:48;
then reconsider c as Element of NAT by INT_1:3;
consider D be Integer such that
A16: (b-1)*D = t-n by INT_1:def 5,HILB10_1:24;
D>=0 by A16,XREAL_1:48,HILB10_1:13;
then reconsider D as Element of NAT by INT_1:3;
set Z=(a^2-'1) *(v^2);
set d = (r*y *(a^2-'1) *v)*(Z+2-a)*D;
A17: y^2=y*y by SQUARE_1:def 1;
A18: v^2=v*v by SQUARE_1:def 1;
A19: a*a=a^2 by SQUARE_1:def 1;
then a^2>=1+0 by NAT_1:13;
then
A20: a^2-'1 = a^2-1 by XREAL_1:233;
v >= m by HILB10_1:13;
then v >=1 & v^2=v*v by A10,XXREAL_0:2,SQUARE_1:def 1;
then
A21: v^2 >=1*1 by XREAL_1:66;
a*a > a*1 by XREAL_1:97,NEWTON03:def 1;
then a^2 >= a+1 by A19,NAT_1:13;
then a^2-'1 >= a by A20,XREAL_1:19;
then Z >= a*1 by A21,XREAL_1:66;
then Z-a >=0 by XREAL_1:48;
then Z-a+2 >= 0+0;
then reconsider d as Element of NAT by INT_1:3;
take b,c,d,r,s,t,u,v,x;
A22: b = a+ ((a^2-'1) *(v^2)+1) * ((a^2-'1) *(v^2)+1-a) by A4
.= Z*Z + Z*(2-a) +1;
t = n+(b-1)*D by A16;
hence thesis by A17,A18,A3,A4,A14,Lm1,A8,A6,A7,A15,A2,HILB10_1:13,A22;
end;
theorem Th28:
for a for y,n be Nat st 1 <=n holds
y= Py(a,n) iff ex c,d,r,u,x be Nat st
[x,y] is Pell's_solution of a^2-'1 &
u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 &
(x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 &
n <= y
proof
let a;
let y,n be Nat such that
A1: 1 <=n;
thus y= Py(a,n) implies ex c,d,r,u,x be Nat st
[x,y] is Pell's_solution of a^2-'1 &
u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 &
(x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 &
n <= y
proof
assume y= Py(a,n);
then consider b,c,d,r,s,t,u,v,x be Nat such that
A2: [x,y] is Pell's_solution of a^2-'1 and
A3: [u,v] is Pell's_solution of a^2-'1 and
A4: [s,t] is Pell's_solution of b^2-'1 and
A5: v= 4*r*y^2 and
A6: b =a +u^2*(u^2-a)and
A7: s=x+c*u and
A8: t=n+4*d*y and
A9: n <= y by Th27,A1;
A10: b is non trivial & u^2 > a by Th26,A1,A2,A3,A4,A5,A6,A7,A8,A9;
A11: a^2=a*a & b^2=b*b & r^2=r*r & v^2=v*v by SQUARE_1:def 1;
then a^2>=1+0 & b^2>=1+0 by A10,NAT_1:13;
then
A12: a^2-'1 = a^2-1 & b^2-'1 = b^2-1 by XREAL_1:233;
take c,d,r,u,x;
thus [x,y] is Pell's_solution of a^2-'1 by A2;
u^2 - (a^2-'1)*v^2 =1 by A3,Lm1;
then u^2 = (a^2-'1)*v^2 +1;
hence u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 by A11,A12,A5;
s^2 - (b^2- 1)*t^2 =1 by A12,A4,Lm1;
then s^2 = (b^2- 1)*t^2 + 1;
hence thesis by A9,A6,A7,A8;
end;
given c,d,r,u,x be Nat such that
A13: [x,y] is Pell's_solution of a^2-'1 and
A14: u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 and
A15: (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 and
A16: n<=y;
consider k such that
A17: x=Px(a,k) & y = Py(a,k) by A13,HILB10_1:4;
A18: Px(a,0) = 1 & Py(a,0) = 0 by HILB10_1:3;
then
A19: Px(a,0+1) = 1*a + 0*(a^2-'1) by HILB10_1:6;
A20: y >=1 by A16,A1,XXREAL_0:2;
k>0 by A18,A17,A16,A1;
then k>=1+0 by NAT_1:13;
then x >= a & a >1 by A17,A19,HILB10_1:10,NEWTON03:def 1;
then
A21: x > 1 by XXREAL_0:2;
set v= 4*r*y^2,b =a +u^2*(u^2-a),s=x+c*u,t=n+4*d*y;
a^2=a*a by SQUARE_1:def 1;
then a^2>=1+0 by NAT_1:13;
then
A22: a^2-'1 = a^2-1 by XREAL_1:233;
A23: u^2=u*u & v^2=v*v & r^2=r*r & y^2=y*y by SQUARE_1:def 1;
r<>0
proof
assume r=0;
then
A24: u=1 by A14,NAT_1:15,A23;
then (x+c*u)*(x+c*u)=1 by A15,A23,SQUARE_1:def 1;
then x+c = 1+0 by A24,NAT_1:15;
hence thesis by A21,XREAL_1:8;
end;
then
A25: r^2 >=1+0 by A23,NAT_1:13;
A26: y^2 >=1*1 by A23,A20,XREAL_1:66;
a*a > a*1 by XREAL_1:97,NEWTON03:def 1;
then a*a >= a+1 by NAT_1:13;
then a*a-1 >= a &a^2=a*a by XREAL_1:19,SQUARE_1:def 1;
then 16*(a^2-1) >= 1*a by XREAL_1:66;
then 16*(a^2-1)*r^2 >= a*1 by A25,XREAL_1:66;
then 16*(a^2-1)*r^2*y^2 >= a*1 by A26,XREAL_1:66;
then 16*(a^2-1)*r^2*y^2*y^2+1 > a*1 by NAT_1:13,A26,XREAL_1:66;
then u^2-a >0 by A14,XREAL_1:50;
then b >= a+0 by XREAL_1:7;
then b >1 & b in NAT by NEWTON03:def 1,XXREAL_0:2,INT_1:3;
then reconsider b as non trivial Element of NAT by NEWTON03:def 1;
b^2=b*b by SQUARE_1:def 1;
then b^2>=1+0 by NAT_1:13;
then b^2-'1 = b^2-1 by XREAL_1:233;
then s^2 -(b^2-'1)*t^2 =1 by A15;
then
A27: [s,t] is Pell's_solution of b^2-'1 by Lm1;
u^2 = (a^2-1)*v^2+1 by A23,A14;
then u^2 - (a^2-'1)*v^2=1 by A22;
then [u,v] is Pell's_solution of a^2-'1 by Lm1;
hence thesis by A1,Th26,A27,A13,A16;
end;
theorem Th29:
for f,k be positive Nat holds f=k! iff
ex j,h,w be Nat, n,p,q,z be positive Nat st
q= w*z+h+j & z = f*(h+j) +h &
(2*k) |^3 *(2*k+2)*(n+1) |^2+1 is square &
p=(n+1) |^k & q=(p+1) |^n & z=p|^(k+1)
proof
let f,k be positive Nat;
set k2=2*k;
A1: k>=1 by NAT_1:14;
then
A2: k2 >= 1*2 & k2 >= 1*1 by XREAL_1:66;
thus f=k! implies ex j,h,w be Nat, n,p,q,z be positive Nat st
q= w*z+h+j & z = f*(h+j) +h &
(2*k) |^3*(k2+2)*(n+1) |^2+1 is square &
p=(n+1) |^k & q=(p+1) |^n & z=p|^(k+1)
proof
assume
A3: f=k!;
consider n,i such that
A4: 10 divides n+1 & k2^2 *(k2 *(k2+2))*(n+1)^2 +1 = i^2 by A2,Th6;
set p=(n+1) |^k,q=(p+1) |^n, z=p|^(k+1);
set w = q div z;
A5: k2 |^k <=n
proof
A6: k2-'2 = k2-2 by A2,XREAL_1:233;
A7: k2 -1 +k2 |^(k2-'2) <=n by A2,A4,Th5;
per cases by A1,XXREAL_0:1;
suppose k=1;
then k2 |^(k2-'2) = 1 & (k2) |^k = k2 by NEWTON:4,A6;
hence thesis by A7;
end;
suppose k>1;
then k>=1+1 by NAT_1:13;
then k+k >= k+2 by XREAL_1:6;
then k2 |^ (k2-'2) >= k2 |^ k by NAT_6:1,A6,XREAL_1:19;
then k2 |^ (k2-'2) +(k2 -1) >= k2 |^ k + 0 by XREAL_1:7;
hence thesis by A7,XXREAL_0:2;
end;
end;
n>0
proof
assume n<=0;
then n=0;
hence thesis by A4,INT_2:13;
end;
then reconsider n as positive Nat;
n < n+1 by NAT_1:13;
then
A8: n|^k < p by PREPOWER:10,NAT_1:14;
A9: (q mod z) >0 by A8,A5,Th11;
p * p|^k = z by NEWTON:6;
then k! < z / ( q mod z) < k!+1 by A8,A5,Th11;
then
A10: f * ( q mod z) < z < (f+1)*( q mod z) by A3,A9,XREAL_1:77,79;
then reconsider h = z- f*(q mod z) as Element of NAT by NAT_1:21;
reconsider h as positive Nat by A10,XREAL_1:50;
set j = (q mod z) -h;
0< (f+1)*( q mod z) - z by A10,XREAL_1:50;
then reconsider j as positive Nat;
A11: k2-1 +k2 |^(k2-'2) > k2-1 by XREAL_1:29;
w>0
proof
A12: p>=1 by NAT_1:14;
k2-1 +k2 |^(k2-'2) <= n by A2,A4,Th5;
then k2-1 <n by A11,XXREAL_0:2;
then k2-1+1 <=n by INT_1:7;
then 1+k <= k+k & k+k <=n by A1,XREAL_1:7;
then 1+k <=n & p < p+1 by XXREAL_0:2,NAT_1:13;
then p to_power (k+1) <= p to_power n &
p to_power n < (p+1) to_power n by A12,PRE_FF:8,POWER:37;
then
A13: z < q by XXREAL_0:2;
assume w<=0;
then q div z=0;
hence thesis by A13,NAT_2:12;
end;
then reconsider w as positive Nat;
take j,h,w,n,p,q,z;
(k2^2 *k2) *(k2+2)*((n+1) |^2) +1 is square by A4,NEWTON:81;
then (k2|^2 *k2) *(k2+2)*((n+1) |^2) +1 is square by NEWTON:81;
then
A14: (k2|^(2+1)) *(k2+2)*((n+1) |^2) +1 is square by NEWTON:6;
q= (q div z) * z +(q mod z) by NAT_D:2;
then q= w*z+h+j;
hence thesis by A14;
end;
given j,h,w be Nat,n,p,q,z be positive Nat such that
A15: q= w*z+h+j and
A16: z = f*(h+j) +h and
A17: (2*k) |^3*(k2+2)*(n+1) |^2+1 is square and
A18: p=(n+1) |^k and
A19: q=(p+1) |^n and
A20: z=p|^(k+1);
A21: k2 |^k <=n
proof
A22: k2-'2 = k2-2 by A2,XREAL_1:233;
(k2) |^(2+1)*(k2+2)*(n+1) |^2+1 =
(k2) |^2*k2*(k2+2)*(n+1) |^2+1 by NEWTON:6
.= (k2) ^2 *k2*(k2+2)*(n+1) |^2+1 by NEWTON:81
.= (k2) ^2 *k2*(k2+2)*(n+1) ^2+1 by NEWTON:81;
then ex i st (k2) ^2 *(k2*(k2+2))*(n+1) ^2+1 = i^2 by A17,PYTHTRIP:def 3;
then
A23: k2-1 + k2|^(k2-'2)<=n by A2,Th5;
per cases by A1,XXREAL_0:1;
suppose k=1;
then k2 |^(k2-'2) = 1 & (k2) |^k = k2 by NEWTON:4,A22;
hence thesis by A23;
end;
suppose k>1;
then k>=1+1 by NAT_1:13;
then k+k >= k+2 by XREAL_1:6;
then k2 |^ (k2-'2) >= k2 |^ k by A22,NAT_6:1,XREAL_1:19;
then k2 |^ (k2-'2) +(k2 -1) >= k2 |^ k + 0 by XREAL_1:7;
hence thesis by A23,XXREAL_0:2;
end;
end;
j <= h+j & 1*(h+j) <= f*(h+j) by XREAL_1:64,NAT_1:11,14;
then j <=f*(h+j) by XXREAL_0:2;
then
A24: h+j<=z by A16,XREAL_1:6;
n < n+1 by NAT_1:13;
then
A25:n|^k < p by PREPOWER:10,NAT_1:14,A18;
A26: p * p|^k = z by NEWTON:6,A20;
h+j<>z
proof
assume h+j=z;
then q =z*(w+1) by A15;
then q mod z=0;
hence thesis by A25,A21,Th11,A19,A20;
end;
then
A27: h+j <z by A24,XXREAL_0:1;
A28: w*z mod z=0;
q= w*z+(h+j) & z<>0 by A15;
then q mod z = h+j by A27,A28,NAT_D:16;
then
A29: k! < z / (h+j) < k!+ 1 by A26,A25,A21,Th11,A18,A19,A20;
z <= z+j by NAT_1:11;
then
A30: z <= (f+1)*(h+j) by A16;
h+j=0 or h+j>0;
then z / (h+j) <=f+1 by XREAL_1:79,A30;
then k! < f+1 by A29,XXREAL_0:2;
then
A31: k! <=f by NAT_1:13;
h+j<>0 by A16;
then f <= z/(h+j) by XREAL_1:77,A16,NAT_1:11;
then f <k!+1 by A29,XXREAL_0:2;
then f <=k! by NAT_1:13;
hence thesis by A31,XXREAL_0:1;
end;
theorem Th30:
for k be positive Nat holds k+1 is prime iff
ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st
q = w*z+h+j &
z = (g*k+g+k)*(h+j)+h &
(2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 &
e=p+q+z+2*n &
e |^3 *(e+2)*(a+1) |^2+1 =o^2 &
[x,y] is Pell's_solution of a^2-'1 &
u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 &
(x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 &
[m,l] is Pell's_solution of a^2-'1 &
l=k+i*(a-1) &
n+l+v=y &
m=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1) &
x= q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1) &
p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1)
proof
let k be positive Nat;
thus k+1 is prime implies
ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st
q = w*z+h+j &
z = (g*k+g+k)*(h+j)+h &
(2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 &
e=p+q+z+2*n &
e |^3 *(e+2)*(a+1) |^2+1 =o^2 &
[x,y] is Pell's_solution of a^2-'1 &
u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 &
(x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 &
[m,l] is Pell's_solution of a^2-'1 &
l=k+i*(a-1) &
n+l+v=y &
m=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1) &
x= q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1) &
p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1)
proof
A1: k+1-'1=k+1-1 by NAT_1:11,XREAL_1:233;
assume k+1 is prime;
then k!+1 mod (k+1)=0 by A1, NAT_5:22;
then k+1 divides k!+1 by INT_1:62;
then consider g1 be Nat such that
A2: k!+1 = (k+1)*g1 by NAT_D:def 3;
g1<>0 by A2;
then reconsider g=g1-1 as Nat;
k!+1 = (k+1)*(g+1) by A2;
then consider j,h,w be Nat,n,p,q,z be positive Nat such that
A3: q= w*z+h+j and
A4: z = (g*k+g+k)*(h+j) +h and
A5: (2*k) |^3 *(2*k+2)*(n+1) |^2+1 is square and
A6: p=(n+1) |^k & q=(p+1) |^n & z=p|^(k+1) by Th29;
consider f be Nat such that
A7: (2*k) |^3 *(2*k+2)*(n+1) |^2+1=f^2 by A5,PYTHTRIP:def 3;
set e=p+q+z+2*n;
p>=1 & q>=1 by NAT_1:14;
then p+q >=1+1 by XREAL_1:7;
then (p+q)+z >= 2+0 by XREAL_1:7;
then
A8: e>=2+0 by XREAL_1:7;
then consider a,o be Nat such that
A9: 10 divides a+1 & e^2 *(e *(e+2))*(a+1)^2 +1 = o^2 by Th6;
9+1=10<= a+1 by A9,INT_2:27;
then
A10: 9<=a by XREAL_1:6;
then
A11: a>=1+1 by XXREAL_0:2;
a>1 by A10,XXREAL_0:2;
then reconsider a as non trivial Nat by NEWTON03:def 1;
A12: e-1 +e |^(e-'2) > e-1 by XREAL_1:29;
e-1 +e |^(e-'2) <= a by A9,A8,Th5;
then e-1 <a by A12,XXREAL_0:2;
then
A13: e-1+1<=a by INT_1:7;
e^2 = e|^2 & (a+1) |^2 =(a+1) ^2 by NEWTON:81;
then
A14: e^2 *e = e|^(2+1) by NEWTON:6;
set y = Py(a,n);
1<=n by NAT_1:14;
then consider c,d,r,u,x be Nat such that
A15: [x,y] is Pell's_solution of a^2-'1 and
A16: u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 and
A17: (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 and
n <= y by Th28;
set m=Px(a,k),l=Py(a,k);
A18: m^2 - (a^2-'1)*l^2=1 by HILB10_1:7;
consider i be Integer such that
A19: (a-1)*i = Py(a,k)-k by INT_1:def 5,HILB10_1:24;
i>=0 by A19,NAT_1:21,HILB10_1:13;
then reconsider i as Element of NAT by INT_1:3;
reconsider n1=n-1 as Element of NAT by NAT_1:14,NAT_1:21;
A20: n-'1=n-1=n1 by NAT_1:14,XREAL_1:233;
A21: Px(a,n1)>=1 by NAT_1:14;
A22: Py(a,n1)+Py(a,n1) >= Py(a,n1)+n1 by HILB10_1:13,XREAL_1:6;
Py(a,n1)*a >= Py(a,n1)*2 by A11,XREAL_1:64;
then Py(a,n1)*a >= Py(a,n1)+n1 by A22,XXREAL_0:2;
then Px(a,n1)+Py(a,n1)*a>= 1+(Py(a,n1)+n1) by A21,XREAL_1:7;
then
A23: Py(a,n1+1) >= 1+(Py(a,n1)+n1) by HILB10_1:6;
A24: k>=1 by NAT_1:14;
A25: 2*k>=2*1 by NAT_1:14,XREAL_1:64;
(2*k)^2 = (2*k) |^2 & (n+1) |^2 =(n+1) ^2 by NEWTON:81;
then (2*k)^2 *(2*k) = (2*k) |^(2+1) by NEWTON:6;
then (2*k)^2 *((2*k) *((2*k)+2))*(n+1)^2+1 =f^2 by NEWTON:81,A7;
then A26: (2*k)-1 +(2*k) |^((2*k)-'2) <= n by A25,Th5;
(2*k)-1 +(2*k) |^((2*k)-'2) > (2*k)-1 by XREAL_1:29;
then 2*k-1 <n by A26,XXREAL_0:2;
then 2*k-1+1 <=n by INT_1:7;
then 1+k <= k+k & k+k <=n by A24,XREAL_1:7;
then 1+k <=n by XXREAL_0:2;
then k <= n-'1 by A20,XREAL_1:19;
then k = n-'1 or k < n-'1 by XXREAL_0:1;
then Py(a,k) = Py(a,n-'1) or Py(a,k) < Py(a,n-'1) by HILB10_1:11;
then Py(a,k)+n <= Py(a,n-'1)+n by XREAL_1:6;
then y-(n+l) is Element of NAT by NAT_1:21,A23,A20,XXREAL_0:2;
then consider v be Nat such that
A27: v=y-(n+l);
A28: 2*n=n+n >=n+1 >= 1+1 by XREAL_1:6,NAT_1:14;
then 2*n >=1+1 by XXREAL_0:2;
then 2*n > 1 by NAT_1:13;
then e>p+q+z+1 & p+q+(z+1) >z+1 & z+q+(p+1) >p+1 & p+z+(q+1)>q+1 & e> 2*n
by XREAL_1:29,6;
then e>z+1 & e >p+1 & e >q+1 & e>n+1 by A28,XXREAL_0:2;
then
A29: a>z+1 & a>p+1 & a>q+1 & a>n+1 by A13,XXREAL_0:2;
then
A30: a>z & a>p & a>q & a>n+1 by NAT_1:13;
A31: (n+1) |^k <a & (p+1) |^n<a & p |^(k+1) <a by A29,NAT_1:13,A6;
consider b be Integer such that
A32: (2*a*(n+1)-(n+1)^2-1)*b = Px(a,k) - (p +Py(a,k)*(a-(n+1)))
by INT_1:def 5,A6,Th13;
A33: a*(n+1)>(n+1)*(n+1)=(n+1)^2 by A29,XREAL_1:68,SQUARE_1:def 1;
a*(n+1)+a*(n+1) > (n+1)^2+1 by NAT_1:14,A33,XREAL_1:8;
then
A34: 2*a*(n+1)-((n+1)^2+1)>0 by XREAL_1:50;
p + Py(a,k)*(a-(n+1)) <= Px(a,k) by A31,Th14,A6;
then b>=0 by A32,A34,XREAL_1:48;
then reconsider b as Element of NAT by INT_1:3;
consider s be Integer such that
A35: (2*a*(p+1)-(p+1)^2-1)*s = Px(a,n) - (q +Py(a,n)*(a-(p+1)))
by INT_1:def 5,A6,Th13;
a*(p+1)>(p+1)*(p+1)=(p+1)^2 by SQUARE_1:def 1,A29,XREAL_1:68;
then a*(p+1)+a*(p+1) > (p+1)^2+1 by XREAL_1:8,NAT_1:14;
then
A36: 2*a*(p+1)-((p+1)^2+1)>0 by XREAL_1:50;
consider n2 be Nat such that
A37: x=Px(a,n2) & y = Py(a,n2) by A15,HILB10_1:4;
q + Py(a,n)*(a-(p+1)) <= Px(a,n) by Th14,A31,A6;
then s>=0 by A35,A36,XREAL_1:48;
then reconsider s as Element of NAT by INT_1:3;
consider t1 be Integer such that
A38: (2*a*p-p^2-1)*t1 = Px(a,k) - (p|^k +Py(a,k)*(a-p))
by Th13,INT_1:def 5;
a > p by A29,NAT_1:13;
then a*p > p*p=p^2 by SQUARE_1:def 1,XREAL_1:68;
then a*p+a*p > p^2+1 by XREAL_1:8,NAT_1:14;
then
A39: 2*a*p-(p^2+1)>0 by XREAL_1:50;
A40: z =p|^k *p & p >=1 by NAT_1:14,NEWTON:6,A6;
a > p|^k *p & p|^k *p >= p|^k*1 by A30,XREAL_1:64,NAT_1:14,NEWTON:6,A6;
then a > p|^k>0 by XXREAL_0:2;
then Px(a,k) >= (p|^k +Py(a,k)*(a-p)) by Th14;
then t1>=0 by A39,A38,XREAL_1:48;
then reconsider t1 as Element of NAT by INT_1:3;
set t=t1*p;
A41: (2*a*p-p^2-1)*t1*p = (Px(a,k) - (p|^k +Py(a,k)*(a-p)))*p by A38;
take a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z;
thus q = w*z+h+j & z = (g*k+g+k)*(h+j)+h &
(2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 by A3,A4,A7;
thus e=p+q+z+2*n & e |^3 *(e+2)*(a+1) |^2+1 =o^2 by A14,A9,NEWTON:81;
thus [x,y] is Pell's_solution of a^2-'1 &
u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 &
(x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 by A15,A16,A17;
thus [m,l] is Pell's_solution of a^2-'1 &
l=k+i*(a-1)& n+l+v=y by A27,A19,A18,Lm1;
thus thesis by A35,HILB10_1:12,A37,A41,A40,A32;
end;
given a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat such that
A42: q = w*z+h+j and
A43: z = (g*k+g+k)*(h+j)+h and
A44: (2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 and
A45: e=p+q+z+2*n and
A46: e |^3 *(e+2)*(a+1) |^2+1 =o^2 and
A47: [x,y] is Pell's_solution of a^2-'1 and
A48: u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 and
A49: (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 and
A50: [m,l] is Pell's_solution of a^2-'1 and
A51: l=k+i*(a-1) and
A52: n+l+v=y and
A53: m=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1) and
A54: x= q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1) and
A55: p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1);
A56: k>=1 by NAT_1:14;
A57: 2*k>=2*1 by NAT_1:14,XREAL_1:64;
(2*k)^2 = (2*k) |^2 & (n+1) |^2 =(n+1) ^2 by NEWTON:81;
then (2*k)^2 *(2*k) = (2*k) |^(2+1) by NEWTON:6;
then (2*k)^2 *((2*k) *((2*k)+2))*(n+1)^2+1 =f^2 by NEWTON:81,A44;
then
A58: (2*k)-1 +(2*k) |^((2*k)-'2) <= n by A57,Th5;
(2*k)-1 +(2*k) |^((2*k)-'2) > (2*k)-1 by XREAL_1:29;
then 2*k-1 <n by A58,XXREAL_0:2;
then 2*k-1+1 <=n by INT_1:7;
then 1+k <= k+k & k+k <=n by A56,XREAL_1:7;
then
A59: 1+k <=n by XXREAL_0:2;
then
A60: k <n by NAT_1:13;
A61: 1+1<=1+k by NAT_1:14,XREAL_1:6;
then
A62: 2<=n by A59,XXREAL_0:2;
then
A63: e>= 2*n=n+n >=2+0 & n+n >= n+2 by A45,XREAL_1:7,31;
then
A64: e>=2 & e >= n+1+1 by XXREAL_0:2;
then
A65: e >n+1 by NAT_1:13;
e^2 = e |^2 & (a+1) |^2 =(a+1) ^2 by NEWTON:81;
then e^2 *e = e |^(2+1) by NEWTON:6;
then
A66: e^2 *(e *(e+2))*(a+1)^2+1 =o^2 by NEWTON:81,A46;
then
A67: e-1 +e |^(e-'2) <= a by A64,Th5;
A68: e-1 +e |^(e-'2) > e-1 by A45,XREAL_1:29,A58;
e-1 +e |^(e-'2) <= a by A66,A64,Th5;
then e-1 <a by A68,XXREAL_0:2;
then
A69: e-1+1<=a by INT_1:7;
n>=1 & p+q+z+n >=n by NAT_1:14,A58,XREAL_1:31;
then p+q+z+n+n>=n+1 by XREAL_1:7;
then e>n by A45,NAT_1:13;
then
A70: n <a & 1<=n by A69,XXREAL_0:2,A62; then
A71: a>1 by XXREAL_0:2;
then reconsider a as non trivial Nat by NEWTON03:def 1;
reconsider a1=a-1 as Nat;
n <= n+(l+v) by XREAL_1:31;
then
A72: y =Py(a,n) by A52,A70,A47,A48,A49,Th28;
consider n2 be Nat such that
A73: x=Px(a,n2) & y = Py(a,n2) by A47,HILB10_1:4;
A74: n=n2 by A73,A72,HILB10_1:12;
consider k1 be Nat such that
A75: m=Px(a,k1) & l = Py(a,k1) by A50,HILB10_1:4;
n+v >=1+0 by A70,XREAL_1:7;
then l+1 <= l+(n+v) by XREAL_1:6;
then Py(a,k1) < Py(a,n) by A52,A72,A75,NAT_1:13;
then k1<>n & k1 <= n by HILB10_1:11;
then k1 <n by XXREAL_0:1;
then k1+1 <=n by NAT_1:13;
then k1+1 <a by A70,XXREAL_0:2;
then
A76: k1+1-1 <a-1 by XREAL_1:9;
k+1 <a by A70,XXREAL_0:2,A59;
then
A77: k+1-1 <a-1 by XREAL_1:9;
Py(a,k1)-k = i*(a-1) by A51,A75;
then
A78: k,Py(a,k1) are_congruent_mod (a-1) by INT_1:14,def 5;
Py(a,k1),k1 are_congruent_mod (a-1) by HILB10_1:24;
then 0+k mod a1 = 0+k1 mod a1 & 0 mod a1=0 by NAT_D:64,A78,INT_1:15;
then
A79: k = k mod a1 = k1 mod a1 =k1 by A76,A77,NAT_D:16;
2*n >=1+1 by A63;
then
A80: 2*n > 1 by NAT_1:13;
p+((q+z)+2*n)>=1+p by XREAL_1:6,A58,NAT_1:14;
then e>p by A45,NAT_1:13;
then
A81: a > p by A69,XXREAL_0:2;
e>=1+1 by A63,XXREAL_0:2;
then e>1 by NAT_1:13;
then e-1 >1-1 by XREAL_1:9;
then 0 + e |^(e-'2) < e-1 +e |^(e-'2) by XREAL_1:6;
then
A82: e to_power (e-'2) <a by A67,XXREAL_0:2;
A83: e-2 >= n+2-2 & e-2 > n+1-2 & e-'2 =e-2 & n-1 >= 2-1
by A62,A64,A65,XREAL_1:233,9;
then
A84: e-'2 > k & e-'2 >1 by A60,XXREAL_0:2;
A85: (n+1) |^k <a
proof
A86: n+1>0+1 by A58,XREAL_1:6;
(n+1) to_power k < (n+1) to_power (e-'2)&
(n+1) to_power (e-'2) < e to_power (e-'2) by A65,A84,A86,POWER:37,39;
then (n+1) to_power k < e to_power (e-'2) by XXREAL_0:2;
hence thesis by A82,XXREAL_0:2;
end;
A87: 2*1<= n* a by A71,A62,XREAL_1:66;
A88: n+1 <= a by A70,NAT_1:13;
then (n+1)*n <= a*n by XREAL_1:64;
then (n+1)*n +(n+1) <= a*n+a & (n+1)^2 = (n+1)*(n+1)
by A88,XREAL_1:7,SQUARE_1:def 1;
then (n+1) ^2 +2 <= a*n+a+n*a by A87,XREAL_1:7;
then (n+1)^2+1+1 <= 2*a*n+a;
then (n+1)^2+1 < 2*a*n+a by NAT_1:13;
then 0< 2*a*n+a - ((n+1)^2+1) by XREAL_1:50;
then 0+a< 2*a*n+a - (n+1)^2-1+a by XREAL_1:6;
then
A89: p < 2 * a*(n+1)-(n+1)^2-1 & (n+1) |^k < 2 * a*(n+1)-(n+1)^2-1
by A81,A85,XXREAL_0:2;
m-(p+l*(a-n-1))= b*(2*a*(n+1)-(n+1)^2-1) by A53;
then
A90: Px(a,k),p+Py(a,k)*(a-n-1) are_congruent_mod (2*a*(n+1)-(n+1)^2-1)
by INT_1:def 5,A79,A75;
A91: Py(a,k)*(a-(n+1)), Py(a,k)*(a-(n+1))
are_congruent_mod 2*a*(n+1)-(n+1)^2-1 by INT_1:11;
(n+1) |^k + Py(a,k)*(a-(n+1)),Px(a,k)
are_congruent_mod 2*a*(n+1)-(n+1)^2-1 by Th13,INT_1:14;
then (n+1) |^k + Py(a,k)*(a-(n+1)), p+Py(a,k)*(a-n-1)
are_congruent_mod 2*a*(n+1)-(n+1)^2-1 by A90,INT_1:15;
then (n+1) |^k + Py(a,k)*(a-(n+1))-Py(a,k)*(a-(n+1)),
p+Py(a,k)*(a-n-1)-Py(a,k)*(a-(n+1))
are_congruent_mod 2*a*(n+1)-(n+1)^2-1 by A91,INT_1:17;
then (0+(n+1) |^k) mod (2*a*(n+1)-(n+1)^2-1) =
0+ p mod (2*a*(n+1)-(n+1)^2-1) &
0 mod (2*a*(n+1)-(n+1)^2-1)=0 by NAT_D:64;
then
A92: (n+1) |^k = ((n+1) |^k) mod (2*a*(n+1)-(n+1)^2-1) =
p mod (2*a*(n+1)-(n+1)^2-1) = p by A89,NAT_D:16;
n+1 >=1+1 by A70,XREAL_1:6;
then p >= k+1 by A92,NEWTON:85;
then p > k by NAT_1:13;
then
A93: p > 1 by A56,XXREAL_0:2;
q+((p+z)+2*n)>=1+q by XREAL_1:6,A58,NAT_1:14;
then e>q by A45,NAT_1:13;
then
A94: a > q by A69,XXREAL_0:2;
n>=2 & p>=1 by A92,NAT_1:14,A61,A59,XXREAL_0:2;
then n+p >= 2+1 & n+(q+z) >= n+0 by XREAL_1:7;
then (n+q+z)+(n+p)>=n+(2+1) by XREAL_1:7;
then e-2 >=n+2+1-2 by A45,XREAL_1:9;
then
A95: e-'2 > n by A83,NAT_1:13;
A96: (p+1) |^n <a
proof
A97: p+1>0+1 by A92,XREAL_1:6;
p+1< p+ 2*n by A80,XREAL_1:6;
then
A98: p+1+0 < p+2*n+(q+z) by XREAL_1:8;
(p+1) to_power n < (p+1) to_power (e-'2)&
(p+1) to_power (e-'2) < e to_power (e-'2)
by A45,A98,A95,A97,POWER:37,39;
then (p+1) to_power n < e to_power (e-'2) by XXREAL_0:2;
hence thesis by A82,XXREAL_0:2;
end;
a>=1+1 & p >=1 by A71,A92,NAT_1:13,14;
then
A99: 2*1<= p * a by XREAL_1:66;
A100: p+1 <= a by A81,NAT_1:13;
then (p+1)*p <= a*p by XREAL_1:64;
then (p+1)*p +(p+1) <= a*p+a & (p+1)^2 = (p+1)*(p+1)
by SQUARE_1:def 1,A100,XREAL_1:7;
then (p+1) ^2 +2 <= a*p+a+p*a by A99,XREAL_1:7;
then (p+1)^2+1+1 <= 2*a*p+a;
then (p+1)^2+1 < 2*a*p+a by NAT_1:13;
then 0< 2*a*p+a - ((p+1)^2+1) by XREAL_1:50;
then 0+a< 2*a*p+a - (p+1)^2-1+a by XREAL_1:6;
then
A101: (p+1) |^n <2 * a*(p+1)-(p+1)^2-1 &
q < 2 * a*(p+1)-(p+1)^2-1 by A94,A96,XXREAL_0:2;
Px(a,n)-( q+Py(a,n)*(a-p-1))=
s*(2*a*(p+1)-(p+1)^2-1) by A54,A74,A73;
then
A102: Px(a,n),q+Py(a,n)*(a-p-1) are_congruent_mod (2*a*(p+1)-(p+1)^2-1)
by INT_1:def 5;
A103: Py(a,n)*(a-p-1),Py(a,n)*(a-p-1)
are_congruent_mod (2*a*(p+1)-(p+1)^2-1) by INT_1:11;
(p+1) |^n + Py(a,n)*(a-(p+1)),Px(a,n)
are_congruent_mod 2*a*(p+1)-(p+1)^2-1 by Th13,INT_1:14;
then (p+1) |^n + Py(a,n)*(a-(p+1)),q+Py(a,n)*(a-p-1)
are_congruent_mod (2*a*(p+1)-(p+1)^2-1) by A102,INT_1:15;
then (p+1) |^n + Py(a,n)*(a-(p+1))-Py(a,n)*(a-p-1)
,q+Py(a,n)*(a-p-1)-Py(a,n)*(a-p-1)
are_congruent_mod (2*a*(p+1)-(p+1)^2-1) by A103,INT_1:17;
then (0+(p+1) |^n) mod (2*a*(p+1)-(p+1)^2-1) =
(0+q) mod (2*a*(p+1)-(p+1)^2-1) &
0 mod (2*a*(p+1)-(p+1)^2-1)=0 by NAT_D:64;
then
A104: (p+1) |^n = (p+1) |^n mod (2*a*(p+1)-(p+1)^2-1) =
q mod (2*a*(p+1)-(p+1)^2-1)=q by A101,NAT_D:16;
(p+q)+2*n >=0+1 by A58,NAT_1:13;
then z+((p+q)+2*n)>=1+z by XREAL_1:6;
then e>z by A45,NAT_1:13;
then
A105: a > z by A69,XXREAL_0:2;
A106: p |^(k+1) <a
proof
A107: e-'2 > k+1 by A59,A95,XXREAL_0:2;
p+1< p+ 2*n by A80,XREAL_1:6;
then p+1+0 < p+2*n+(q+z) by XREAL_1:8;
then
A108: p < e by A45,NAT_1:13;
p to_power (k+1) < p to_power (e-'2)&
p to_power (e-'2) < e to_power (e-'2) by A93,A108,A107,POWER:37,39;
then p to_power (k+1) < e to_power (e-'2) by XXREAL_0:2;
hence thesis by A82,XXREAL_0:2;
end;
p+1 <= a by A81,NAT_1:13;
then
A109: (p+1)*p <= a*p by XREAL_1:64;
A110: a*1 <=a*p by A92,NAT_1:14,XREAL_1:64;
p^2+1 <= p^2+p & p^2=p*p by A92,NAT_1:14, XREAL_1:6,SQUARE_1:def 1;
then p^2+1 <= a*p by A109,XXREAL_0:2;
then p^2+1+a <= a*p+a*p by A110,XREAL_1:7;
then a+(p^2+1)-(p^2+1) <= 2 * a*p -(p^2+1) by XREAL_1:9;
then A111:p |^(k+1) <2 * a*p-p^2-1 & z < 2 * a*p-p^2-1
by A105,A106,XXREAL_0:2;
p*m-(z+p*l*(a-p))= t*(2*a*p-p^2-1) by A55;
then
A112: p*Px(a,k),z+p*Py(a,k)*(a-p) are_congruent_mod (2*a*p-p^2-1)
by INT_1:def 5,A79,A75;
A113: p*Py(a,k)*(a-p),p*Py(a,k)*(a-p) are_congruent_mod (2*a*p-p^2-1)
by INT_1:11;
A114: p,p are_congruent_mod (2*a*p-p^2-1) by INT_1:11;
p |^k + Py(a,k)*(a-p),Px(a,k) are_congruent_mod (2*a*p-p^2-1)
by Th13,INT_1:14;
then p*(p |^k + Py(a,k)*(a-p)),p*Px(a,k)
are_congruent_mod (2*a*p-p^2-1) by INT_1:18,A114;
then p*(p |^k + Py(a,k)*(a-p)),z+p*Py(a,k)*(a-p)
are_congruent_mod (2*a*p-p^2-1) by A112,INT_1:15;
then p*(p |^k) + p*Py(a,k)*(a-p)-p*Py(a,k)*(a-p),
z+p*Py(a,k)*(a-p)-p*Py(a,k)*(a-p)
are_congruent_mod (2*a*p-p^2-1) by A113,INT_1:17;
then p |^(k+1),z are_congruent_mod (2*a*p-p^2-1) by NEWTON:6;
then (0+ p |^(k+1)) mod (2*a*p-p^2-1) = (0+z) mod (2*a*p-p^2-1)
& 0 mod (2*a*p-p^2-1) = 0 by NAT_D:64;
then
A115: p|^ (k+1) = p |^(k+1) mod (2*a*p-p^2-1) = z mod (2*a*p-p^2-1) =z
by A111,NAT_D:16;
A116: k+1> 1 by NAT_1:13,NAT_1:14;
A117: k+1-'1=k+1-1 by XREAL_1:233,NAT_1:14;
g*k+g+k = k! by A44,Th29,A42,A43,A115,A104,A92,A58;
then k!+1 = (g+1)*(k+1);
then k+1 divides k!+1 by INT_1:def 3;
then k!+1 mod (k+1) =0 by INT_1:62;
hence thesis by A116,A117,NAT_5:22;
end;
begin :: Prime Representing Polynomial with 26 Variables
::$N Prime Representing Polynomial
theorem
for k be positive Nat holds k+1 is prime iff
ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st
0 = (w*z+h+j -q)^2 +
((g*k+g+k)*(h+j)+h-z)^2 +
((2*k) |^3 *(2*k+2)*(n+1) |^2+1 - f^2)^2 +
(p+q+z+2*n-e)^2 +
(e |^3 *(e+2)*(a+1) |^2+1 -o^2)^2 +
(x^2-(a^2-'1)*y^2-1)^2 +
(16*(a^2-1)*r^2*y^2*y^2+1 -u^2)^2+
(((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 -(x+c*u)^2)^2 +
(m^2-(a^2-'1)*l^2-1)^2 +
(k+i*(a-1)-l)^2 +
(n+l+v-y)^2 +
(p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1)-m)^2+
(q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1)-x)^2+
(z+p*l*(a-p)+t*(2*a*p-p^2-1)-p*m)^2
proof
let k be positive Nat;
thus k+1 is prime implies
ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st
0=(w*z+h+j -q)^2 + ((g*k+g+k)*(h+j)+h-z)^2 +
((2*k) |^3 *(2*k+2)*(n+1) |^2+1 - f^2)^2 + (p+q+z+2*n-e)^2 +
(e |^3 *(e+2)*(a+1) |^2+1 -o^2)^2 + (x^2-(a^2-'1)*y^2-1)^2 +
(16*(a^2-1)*r^2*y^2*y^2+1 -u^2)^2+
(((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 -(x+c*u)^2)^2+
(m^2-(a^2-'1)*l^2-1)^2 + (k+i*(a-1)-l)^2 +
(n+l+v-y)^2 +(p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1)-m)^2+
(q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1)-x)^2+
(z+p*l*(a-p)+t*(2*a*p-p^2-1)-p*m)^2
proof
assume k+1 is prime;
then consider a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat
such that
A1: q = w*z+h+j and
A2: z = (g*k+g+k)*(h+j)+h and
A3: (2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 and
A4: e = p+q+z+2*n and
A5: e |^3 *(e+2)*(a+1) |^2+1 =o^2 and
A6: [x,y] is Pell's_solution of a^2-'1 and
A7: u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 and
A8: (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 and
A9: [m,l] is Pell's_solution of a^2-'1 and
A10: l = k+i*(a-1) and
A11: n+l+v = y and
A12: m = p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1) and
A13: x = q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1) and
A14: p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1) by Th30;
reconsider x1=w*z+h+j -q,
x2=(g*k+g+k)*(h+j)+h-z,
x3=(2*k) |^3 *(2*k+2)*(n+1) |^2+1 - f^2,
x4=p+q+z+2*n-e,
x5=e |^3 *(e+2)*(a+1) |^2+1 -o^2 as Integer;
reconsider x6=x^2-(a^2-'1)*y^2-1,
x7=16*(a^2-1)*r^2*y^2*y^2+1 -u^2,
x8=((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 -(x+c*u)^2,
x9=m^2-(a^2-'1)*l^2-1,
x10=k+i*(a-1)-l as Integer;
reconsider x11= n+l+v-y,
x12=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1)-m,
x13=q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1)-x,
x14=z+p*l*(a-p)+t*(2*a*p-p^2-1)-p*m as Integer;
take a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z;
A15: x1^2=x1*x1 & x2^2=x2*x2 & x3^2=x3*x3 & x4^2=x4*x4 & x5^2=x5*x5 &
x6^2=x6*x6 & x7^2=x7*x7 & x8^2=x8*x8 & x9^2=x9*x9 & x10^2=x10*x10 &
x11^2=x11*x11 & x12^2=x12*x12 & x13^2=x13*x13 & x14^2=x14*x14
by SQUARE_1:def 1;
m^2-(a^2-'1)*l^2=1 by A9,Lm1;
hence thesis by A1,A2,A3,A4,A15,A5,A6,Lm1,A7,A8,A10,A11,A12,A13,A14;
end;
given a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat such that
A16: 0= (w*z+h+j -q)^2 + ((g*k+g+k)*(h+j)+h-z)^2 +
((2*k) |^3 *(2*k+2)*(n+1) |^2+1 - f^2)^2 +
(p+q+z+2*n-e)^2+ (e |^3 *(e+2)*(a+1) |^2+1 -o^2)^2 +
(x^2-(a^2-'1)*y^2-1)^2 +
(16*(a^2-1)*r^2*y^2*y^2+1 -u^2)^2+
(((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 -(x+c*u)^2)^2+
(m^2-(a^2-'1)*l^2-1)^2 + (k+i*(a-1)-l)^2 +
(n+l+v-y)^2 + (p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1)-m)^2+
(q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1)-x)^2+
(z+p*l*(a-p)+t*(2*a*p-p^2-1)-p*m)^2;
reconsider x1=w*z+h+j -q,
x2=(g*k+g+k)*(h+j)+h-z,
x3=(2*k) |^3 *(2*k+2)*(n+1) |^2+1 - f^2,
x4 = p+q+z+2*n-e,
x5=e |^3 *(e+2)*(a+1) |^2+1 -o^2 as Integer;
reconsider x6=x^2-(a^2-'1)*y^2-1,
x7=16*(a^2-1)*r^2*y^2*y^2+1 -u^2,
x8=((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 -(x+c*u)^2,
x9=m^2-(a^2-'1)*l^2-1,
x10=k+i*(a-1)-l as Integer;
reconsider x11= n+l+v-y,
x12=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1)-m,
x13=q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1)-x,
x14=z+p*l*(a-p)+t*(2*a*p-p^2-1)-p*m as Integer;
A17: x1^2=x1*x1 & x2^2=x2*x2 & x3^2=x3*x3 & x4^2=x4*x4 & x5^2=x5*x5 &
x6^2=x6*x6 & x7^2=x7*x7 & x8^2=x8*x8 & x9^2=x9*x9 & x10^2=x10*x10 &
x11^2=x11*x11 & x12^2=x12*x12 & x13^2=x13*x13 & x14^2=x14*x14
by SQUARE_1:def 1;
ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st
q = w*z+h+j &
z = (g*k+g+k)*(h+j)+h &
(2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 &
e=p+q+z+2*n &
e |^3 *(e+2)*(a+1) |^2+1 =o^2 &
[x,y] is Pell's_solution of a^2-'1 &
u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 &
(x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 &
[m,l] is Pell's_solution of a^2-'1 &
l=k+i*(a-1) &
n+l+v=y &
m=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1) &
x= q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1) &
p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1)
proof
take a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z;
x1=0 by A16,A17;
hence q = w*z+h+j;
x2=0 by A16,A17;
hence z = (g*k+g+k)*(h+j)+h;
x3=0 by A16,A17;
hence (2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2;
x4=0 by A16,A17;
hence e=p+q+z+2*n;
x5=0 by A16,A17;
hence e |^3 *(e+2)*(a+1) |^2+1 =o^2;
x6=0 by A16,A17;
hence [x,y] is Pell's_solution of a^2-'1 by Lm1;
x7=0 by A16,A17;
hence u^2 = 16*(a^2-1)*r^2*y^2*y^2+1;
x8=0 by A16,A17;
hence (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1;
x9=0 by A16,A17;
hence [m,l] is Pell's_solution of a^2-'1 by Lm1;
x10=0 by A16,A17;
hence l=k+i*(a-1);
x11=0 by A16,A17;
hence n+l+v=y;
x12=0 by A16,A17;
hence m=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1);
x13=0 by A16,A17;
hence x= q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1);
x14=0 by A16,A17;
hence p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1);
end;
hence thesis by Th30;
end;