:: Prime Representing Polynomial with 10 Unknowns -- Introduction. Part II
:: by Karol P\kak
::
:: Received December 27, 2022
:: Copyright (c) 2022-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, ARYTM_1, COMPLEX1,
SQUARE_1, NEWTON, INT_2, REAL_1, CARD_3, REALSET1, PELLS_EQ, PYTHTRIP,
MCART_1, HILB10_1, XBOOLE_0, TARSKI, HILB10_8;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, XCMPLX_0,
FINSEQ_1, XXREAL_0, XREAL_0, INT_1, SQUARE_1, NEWTON, RVSUM_1, NAT_D,
PELLS_EQ, PYTHTRIP, ABSVALUE, HILB10_1, ZFMISC_1, XTUPLE_0, INT_2, NAT_1,
PEPIN;
constructors NAT_D, RELSET_1, NEWTON, WSIERP_1, PELLS_EQ, DOMAIN_1, PEPIN,
ABIAN, HILB10_1;
registrations RELAT_1, ORDINAL1, XREAL_0, NAT_1, VALUED_0, INT_1, XXREAL_0,
XCMPLX_0, NEWTON, NEWTON02, NAT_6, FINSEQ_1, NEWTON04, NEWTON03,
PYTHTRIP, ABSVALUE, HILB10_1, XTUPLE_0, FOMODEL0, XBOOLE_0, SQUARE_1,
NUMBERS, CARD_1;
requirements NUMERALS, SUBSET, ARITHM, REAL;
definitions TARSKI;
equalities FINSEQ_1;
theorems NAT_1, ZFMISC_1, XREAL_1, XXREAL_0, NEWTON, INT_1, FINSEQ_3,
SQUARE_1, ABSVALUE, RVSUM_1, INT_2, PREPOWER, NEWTON03, PELLS_EQ,
HILB10_1, NAT_2, XCMPLX_1, IRRAT_1, WSIERP_1, PYTHTRIP, NAT_5, HILB10_6,
ORDINAL1, COMPLEX1, FINSEQ_1, RELAT_1, FUNCT_1, VALUED_1, FINSEQ_2,
RAMSEY_1, NEWTON02;
schemes NAT_1;
begin :: Theta Notation
reserve A for non trivial Nat,
B,C,n,m,k for Nat,
e for Nat;
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;
definition
let t be Real;
attr t is theta means :Def1:
-1 <= t <= 1;
end;
registration
cluster 0 -> theta;
coherence;
cluster theta for Real;
existence
proof
take 0;
thus thesis;
end;
end;
definition
mode _Theta is theta Real;
end;
registration
let t be _Theta;
cluster -t -> theta;
coherence
proof
-1 <= t <=1 by Def1;
then (-1)*(-1) >= (-1)*t >= (-1) * 1 by XREAL_1:65;
hence thesis;
end;
let u be _Theta;
cluster t*u -> theta;
coherence
proof
A1: -1 <= t <=1 & -1 <= u <=1 by Def1;
then
A2: (-1)*(-1) >= (-1)*u >= (-1) * 1 by XREAL_1:65;
per cases;
suppose 0<=u;
then (-1)*u <= t*u <=1*u by A1,XREAL_1:64;
hence thesis by A1,A2,XXREAL_0:2;
end;
suppose u <0;
then (-1)*u >= t*u >= 1*u by A1,XREAL_1:65;
hence thesis by A1,A2,XXREAL_0:2;
end;
end;
end;
theorem Th1:
for T be _Theta holds |.T.| <=1
proof
let T be _Theta;
-1<= T <= 1 by Def1;
hence thesis by ABSVALUE:5;
end;
theorem Th2:
for T be _Theta, lambda, epsilon1,epsilon2 be Real st
lambda = T * epsilon1 & |.epsilon1.| <= |.epsilon2.|
ex T1 be _Theta st lambda = T1 * epsilon2
proof
let T be _Theta, lambda, epsilon1,epsilon2 be Real such that
A1: lambda = T * epsilon1 & |.epsilon1.| <= |.epsilon2.|;
per cases;
suppose
A2: epsilon2=0;
take T1=0;
epsilon1=0 by A2,A1;
hence thesis by A1;
end;
suppose
A3: epsilon2 > 0;
then
A4: |.epsilon2.| = epsilon2 by ABSVALUE:def 1;
per cases;
suppose
A5: epsilon1 >= 0;
then |.epsilon1.| = epsilon1 by ABSVALUE:def 1;
then reconsider T1 = epsilon1 / epsilon2 as _Theta
by Def1,XREAL_1:183,A5,A1,A4;
take TT=T*T1;
thus TT * epsilon2 = T * (epsilon1 / epsilon2 * epsilon2)
.= lambda by A1,XCMPLX_1:87,A3;
end;
suppose
A6: epsilon1 < 0;
then
A7: -epsilon1 >0;
|.epsilon1.| = - epsilon1 by A6,ABSVALUE:def 1;
then
A8: (- epsilon1) / epsilon2 is theta by XREAL_1:183,A7,A1,A4;
-(- epsilon1) / epsilon2 = --((epsilon1) / epsilon2) by XCMPLX_1:187;
then reconsider T1 = (epsilon1) / epsilon2 as _Theta by A8;
take TT=T*T1;
thus TT * epsilon2 = T * ((epsilon1) / epsilon2 * epsilon2)
.= lambda by A1,XCMPLX_1:87,A3;
end;
end;
suppose
A9: epsilon2 < 0;
then
A10: |.epsilon2.| = - epsilon2 by ABSVALUE:def 1;
per cases;
suppose
A11: epsilon1 >= 0;
then |.epsilon1.| = epsilon1 by ABSVALUE:def 1;
then
A12: (epsilon1) / -epsilon2 is theta by XREAL_1:183,A11,A1,A10;
-(epsilon1) / (-epsilon2) = --((epsilon1) / epsilon2) by XCMPLX_1:188;
then reconsider T1 = (epsilon1) / epsilon2 as _Theta by A12;
take TT=T*T1;
thus TT * epsilon2 = T * (epsilon1 / epsilon2 * epsilon2)
.= lambda by A1,XCMPLX_1:87,A9;
end;
suppose
A13: epsilon1 < 0;
then
A14: -epsilon1 >0;
|.epsilon1.| = - epsilon1 by A13,ABSVALUE:def 1;
then (- epsilon1) / (- epsilon2) is theta by XREAL_1:183,A14,A1,A10;
then reconsider T1 = (epsilon1) / epsilon2 as _Theta by XCMPLX_1:191;
take TT=T*T1;
thus TT * epsilon2 = T * ((epsilon1) / epsilon2 * epsilon2)
.= lambda by XCMPLX_1:87,A9,A1;
end;
end;
end;
theorem Th3:
for T1,T2 be _Theta, lambda, epsilon1,epsilon2 be Real st
lambda = (1+ T1 * epsilon1) * (1+ T2 * epsilon2) & 0 <= epsilon1 <=1 &
0<= epsilon2
holds ex T be _Theta st lambda = 1+ T * (epsilon1 + 2*epsilon2)
proof
let T1,T2 be _Theta, lambda, epsilon1,epsilon2 be Real such that
A1: lambda = (1+ T1 * epsilon1) * (1+ T2 * epsilon2) &
0 <= epsilon1 <=1 & 0<= epsilon2;
reconsider epsilon1 as _Theta by A1,Def1;
set ep=epsilon1 + 2*epsilon2;
per cases;
suppose epsilon1 + 2*epsilon2=0;
then
A2: epsilon1=0 & 2*epsilon2=0 by A1;
take T =0;
thus thesis by A2,A1;
end;
suppose
A3: ep<>0;
-1<= T1<=1 & -1<= T2<=1 by Def1;
then (-1)*epsilon1 <= T1 * epsilon1 <= 1* epsilon1 &
(-1)*epsilon2 <= T2 * epsilon2 <= 1* epsilon2 by A1,XREAL_1:64;
then
A4: (-1)*epsilon1 + (-1)*epsilon2 <=
(T1 * epsilon1) + (T2 * epsilon2) <= epsilon1+epsilon2 by XREAL_1:7;
-1 <= T1*T2*epsilon1 <= 1 by Def1;
then (-1)*epsilon2 <= T1*T2*epsilon1*epsilon2 <= 1*epsilon2
by A1,XREAL_1:64;
then (-1)*epsilon1 + (-1)*epsilon2 + (-1)*epsilon2 <=
(T1 * epsilon1) + (T2 * epsilon2) + T1*T2*epsilon1*epsilon2
<= epsilon1 + epsilon2 +epsilon2 by A4,XREAL_1:7;
then (-1) * ep <= (T1 * epsilon1) + (T2 * epsilon2) +
T1*T2*epsilon1*epsilon2 <= 1* ep;
then -1 <= ((T1 * epsilon1) + (T2 * epsilon2) +
T1*T2*epsilon1*epsilon2)/ep <= 1 by A3,A1,XREAL_1:77,79;
then reconsider T =((T1 * epsilon1) + (T2 * epsilon2) +
T1*T2*epsilon1*epsilon2)/ep as _Theta by Def1;
take T;
T * ep = (T1 * epsilon1) + (T2 * epsilon2) +
T1*T2*epsilon1*epsilon2 by A3,XCMPLX_1:87;
hence thesis by A1;
end;
end;
theorem Th4:
for T1,T2 be _Theta,epsilon1,epsilon2 be Real st
T1*epsilon1 <= epsilon2 & epsilon2 <= T2 * epsilon1
holds ex T be _Theta st epsilon2 = T * epsilon1
proof
let T1,T2 be _Theta,epsilon1,epsilon2 be Real such that
A1: T1*epsilon1 <= epsilon2 & epsilon2 <= T2 * epsilon1;
per cases;
suppose
A2: epsilon1=0;
then epsilon2=0 & 0 = 0*0 by A1;
hence thesis by A2;
end;
suppose
A3: epsilon1>0; then
-1<= T1 <= epsilon2/epsilon1 <= T2 <=1 by A1,XREAL_1:77,79,Def1;
then -1 <= epsilon2/epsilon1 <=1 by XXREAL_0:2;
then reconsider T=epsilon2/epsilon1 as _Theta by Def1;
T*epsilon1 = epsilon2 by A3, XCMPLX_1:87;
hence thesis;
end;
suppose
A4: epsilon1<0;
1>=T1 >= epsilon2/epsilon1 >= T2 >=-1 by A1,A4,XREAL_1:78,80,Def1;
then -1 <= epsilon2/epsilon1 <=1 by XXREAL_0:2;
then reconsider T=epsilon2/epsilon1 as _Theta by Def1;
T*epsilon1 = epsilon2 by A4, XCMPLX_1:87;
hence thesis;
end;
end;
theorem Th5:
for T be _Theta, lambda, epsilon1,epsilon2 be Real st
lambda = T * epsilon1 & epsilon1 <= epsilon2 & 0 <= epsilon1
ex T1 be _Theta st lambda = T1 * epsilon2
proof
let T be _Theta, lambda, epsilon1,epsilon2 be Real such that
A1: lambda = T * epsilon1 & epsilon1 <= epsilon2 & 0 <= epsilon1;
|.epsilon1.| = epsilon1 & |.epsilon2.| = epsilon2 by A1,ABSVALUE:def 1;
hence thesis by Th2,A1;
end;
theorem Th6:
for T1,T2 be _Theta,epsilon1,epsilon2 be Real st
0 <= epsilon1 & 0 <= epsilon2
holds ex T be _Theta st T1*epsilon1 + T2*epsilon2 = T* (epsilon1+epsilon2)
proof
let T1,T2 be _Theta,epsilon1,epsilon2 be Real such that
A1: 0 <= epsilon1 & 0 <= epsilon2;
reconsider I=1 as _Theta by Def1;
-1<= T1 <= 1 & -1 <=T2<=1 by Def1;
then (-1)*epsilon1 <= T1*epsilon1 <= 1*epsilon1 &
(-1)*epsilon2 <= T2*epsilon2 <= 1*epsilon2 by A1,XREAL_1:64;
then (-1)*epsilon1 + (-1)*epsilon2 <= T1*epsilon1 + T2*epsilon2
<= 1*epsilon1 + 1*epsilon2 by XREAL_1:7;
then (-I)*(epsilon1 + epsilon2) <= T1*epsilon1 + T2*epsilon2
<= I*(epsilon1+epsilon2);
hence thesis by Th4;
end;
theorem Th7:
for T1 be _Theta, epsilon be Real st 0<= epsilon <= 1/2
ex T2 be _Theta st
1/ (1 + T1*epsilon) = 1 + T2*2* epsilon
proof
let T1 be _Theta, epsilon be Real such that
A1: 0<= epsilon <= 1/2;
A2: 1 - epsilon >=1- 1/2 by A1, XREAL_1:10;
-1<= T1 <= 1 by Def1;
then (-1) *epsilon <= T1*epsilon by A1,XREAL_1:64;
then
A3: 1 + (-1) *epsilon <= 1+ T1*epsilon by XREAL_1:6;
then 1/(1+ T1*epsilon) <= 1 / (1- epsilon) by A2,XREAL_1:118;
then 1/(1+ T1*epsilon)*epsilon <= 1 / (1- epsilon)*epsilon by A1,XREAL_1:64;
then 1/(1+ T1*epsilon)*epsilon <= (1*epsilon) / (1- epsilon) by XCMPLX_1:74;
then
A4: (1*epsilon) /(1+ T1*epsilon) <= (1*epsilon) / (1- epsilon) by XCMPLX_1:74;
reconsider I=1 as _Theta by Def1;
A5: |. 2*epsilon.| = 2*epsilon by A1,ABSVALUE:def 1;
A6: (epsilon / (1- epsilon)) <= epsilon/ (1/2)= 2*epsilon
by A1,XREAL_1:118,A2;
per cases;
suppose T1<0;
then
A7: |.(-T1)* (epsilon / (1+T1 *epsilon)) .| =
(-T1)*(epsilon / (1+T1 * epsilon)) by A1,A2,A3,ABSVALUE:def 1;
-T1 <= 1 by Def1;
then (-T1)*(epsilon /(1+ T1*epsilon))<= 1 *(epsilon /(1+ T1*epsilon))
by A1,A2,A3, XREAL_1:64;
then (-T1)*(epsilon /(1+ T1*epsilon))<= (epsilon) / (1- epsilon)
by A4,XXREAL_0:2;
then I* ((-T1)*(epsilon /(1+ T1*epsilon))) <= 2*epsilon by A6,XXREAL_0:2;
then consider T be _Theta such that
A8: (-T1)* (epsilon / (1+T1*epsilon)) = T * (2*epsilon) by Th2,A7,A5;
1 - (T1*epsilon) / (1+T1*epsilon) =
(1+ T1* epsilon)/(1+T1* epsilon) - (T1*epsilon) / (1+T1* epsilon)
by A2,A3,XCMPLX_1:60
.= (1+ T1* epsilon- T1*epsilon) / (1+T1* epsilon) by XCMPLX_1:120
.= 1 / (1+T1* epsilon);
then 1/ (1 + T1*epsilon) = 1 - T1*(epsilon / (1+T1*epsilon))
by XCMPLX_1:74;
then 1/ (1 + T1*epsilon) = 1 + T*2* epsilon by A8;
hence thesis;
end;
suppose T1>=0; then
A9: |.T1* (epsilon / (1+T1 *epsilon)) .| =
(T1*(epsilon / (1+T1 * epsilon))) by A1,ABSVALUE:def 1;
T1 <= 1 by Def1;
then T1*(epsilon /(1+ T1*epsilon))<= 1 *(epsilon /(1+ T1*epsilon))
by A1,A2,A3, XREAL_1:64;
then T1*(epsilon /(1+ T1*epsilon))<= (epsilon) / (1- epsilon)
by A4,XXREAL_0:2;
then I* (T1*(epsilon /(1+ T1*epsilon))) <= 2*epsilon by A6,XXREAL_0:2;
then consider T be _Theta such that
A10: T1* (epsilon / (1+T1*epsilon)) = T * (2*epsilon) by Th2,A9,A5;
1 - (T1*epsilon) / (1+T1*epsilon) =
(1+ T1* epsilon)/(1+T1* epsilon) - (T1*epsilon) / (1+T1* epsilon)
by A2,A3,XCMPLX_1:60
.= (1+ T1* epsilon- T1*epsilon) / (1+T1* epsilon) by XCMPLX_1:120
.= 1 / (1+T1* epsilon);
then 1/ (1 + T1*epsilon) = 1 - T * (2*epsilon) by A10,XCMPLX_1:74;
then 1/ (1 + T1*epsilon) = 1 + (-T)*2* epsilon;
hence thesis;
end;
end;
theorem Th8:
m^2 <= n implies ex T be _Theta st n choose m = n|^m / (m!) * (1+T*(m^2/n))
proof
defpred P[Nat] means $1^2 <= n implies
ex T be _Theta st n choose $1 = n|^$1 / ($1!) * (1+T*($1^2/n));
n choose 0 = (n|^0) / (0!)* (1+0*(0^2/n)) by NEWTON:12,19;
then
A1: P[0];
A2: for m st P[m] holds P[m+1]
proof
let m;
assume
A3: P[m]; set m1=m+1;
assume
A4: m1^2 <= n;
m <= m1 by NAT_1:11;
then
A5: m^2=m*m <= m1*m1=m1^2 by XREAL_1:66,SQUARE_1:def 1;
then consider T be _Theta such that
A6: n choose m = n|^m / (m!) * (1+T*(m^2/n)) by A3,A4,XXREAL_0:2;
A7: ((n-m)/m1)*1 = ((n-m)/m1)*(n/n) by A5,A4,XCMPLX_1:60
.= ((n-m)*n)/ (m1*n) by XCMPLX_1:76
.= ((n-m)/n) * (n/m1) by XCMPLX_1:76;
m^2 <= n by A5,A4,XXREAL_0:2;
then
A8: (m^2)/n <= n/n =1 by A5,A4,XREAL_1:72,XCMPLX_1:60;
reconsider I=1 as _Theta by Def1;
(n-m)/n = (n/n) - (m/n) by XCMPLX_1:120
.= 1 - 1*(m/n) by A5,A4,XCMPLX_1:60;
then (1+T*(m^2/n))*((n-m)/n) = (1 +T*(m^2/n))*(1 +(- I)*(m/n));
then consider t be _Theta such that
A9: (1+T*(m^2/n))*((n-m)/n) = 1+t*( (m^2/n) + 2*(m/n)) by A8,Th3;
m1^2 = m1*m1 = m*m +2*m +1 & m*m=m^2 by SQUARE_1:def 1;
then m^2 +2*m +0 <= m1^2 by XREAL_1:7;
then (m^2 +2*m)/n <= m1^2/n by XREAL_1:72;
then (m^2/n) + ((2*m)/n) <= m1^2/n by XCMPLX_1:62;
then |.(m^2/n) + 2*(m/n).| <= |.m1^2/n.| by XCMPLX_1:74;
then consider s be _Theta such that
A10: t*( (m^2/n) + 2*(m/n)) = s * (m1^2/n) by Th2;
m1*(m!)= m1! & n* (n|^m) = n|^m1 by NEWTON:6,15;
then
A11: (n/m1) * (n|^m / (m!)) = (n|^m1)/ (m1!) by XCMPLX_1:76;
n choose m1 = ((n-m)/m1) * (n choose m) by IRRAT_1:5
.= ((n|^m1)/ (m1!)) * (((n-m)/n)*(1+T*(m^2/n))) by A11,A6,A7
.= ((n|^m1)/ (m1!)) * (1+s * (m1^2/n)) by A10,A9;
hence thesis;
end;
for m holds P[m] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th9:
for T be _Theta, alpha, epsilon be Real st
alpha = (1+T*epsilon)|^n & 0<= epsilon <= 1 / (2*n) holds
ex T1 be _Theta st alpha = 1+T1*2*n*epsilon
proof
defpred P[Nat] means
for T be _Theta, alpha, epsilon be Real st
alpha = (1+T*epsilon)|^$1 & 0<= epsilon <= 1 / (2*$1) holds
ex T1 be _Theta st alpha = 1+T1*2*$1*epsilon;
A1:P[0]
proof
let T be _Theta, alpha, epsilon be Real such that
A2: alpha = (1+T*epsilon)|^0 & 0<= epsilon <= 1 / (2*0);
take T;
thus thesis by A2,NEWTON:4;
end;
A3:P[m] implies P[m+1]
proof
assume
A4: P[m];set m1=m+1;
let T be _Theta, alpha, epsilon be Real such that
A5: alpha = (1+T*epsilon)|^m1 & 0<= epsilon <= 1 / (2*m1);
per cases;
suppose
A6: m=0;
1<=m1 by NAT_1:11;
then 1 <= 2*1 <= 2*m1 by XREAL_1:66;
then 1<= 2*m1 by XXREAL_0:2;
then reconsider I=1/(2*m1) as _Theta by Def1,XREAL_1:183;
alpha = 1+T*(I*(2*m1))*epsilon by A5,A6;
then alpha = 1+(T*I)*2*m1*epsilon;
hence thesis;
end;
suppose
A7: m>0;
2*m*1 <= 2*m1*1 by XREAL_1:64,NAT_1:11;
then 1/(2*m1) <= 1/(2*m) by A7,XREAL_1:102;
then
A8: epsilon <= 1/(2*m) by A5,XXREAL_0:2;
then consider T1 be _Theta such that
A9: (1+T*epsilon)|^m = 1+T1*2*m*epsilon by A5,A4;
A10: (1+T*epsilon)|^m1 = (1+T1*(2*m*epsilon)) * (1+T*epsilon)
by A9,NEWTON:6;
epsilon*(2*m) <= 1/(2*m) *(2*m) by A8,XREAL_1:64;
then 0 <= 2*m*epsilon <=1 by A5,XCMPLX_1:87,A7;
then consider T2 be _Theta such that
A11: (1+T*epsilon)|^m1 =
1 + T2 * (2*m*epsilon +2 * epsilon ) by A5,A10,Th3;
take T2;
thus thesis by A5,A11;
end;
end;
P[m] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
begin :: More on Solutions to Pell's Equation
reserve a for non trivial Nat;
theorem Th10:
n <= a implies ex T be _Theta st
Py(a,n+1) = (2*a) |^n *(1+T*(n/a))
proof
assume
A1: n <=a;
per cases;
suppose
A2: n=0;
then Py(a,n+1) = Px(a,0) + Py(a,0)*a & Px(a,0) =1 & Py(a,0) =0
by HILB10_1:3,6;
then Py(a,n+1) = 1 = (2*a) |^n *(1+0*(n/a)) by A2;
hence thesis;
end;
suppose
A3: n >0;
A4: -1 is theta;
2*n <= 2*a by A1,XREAL_1:64;
then 1/ (2*a) <= 1/(2*n) by A3,XREAL_1:118;
then consider T be _Theta such that
A5: (1 + (-1) *(1/(2*a)))|^n = 1+T*2*n*(1/(2*a)) by A4,Th9;
A6: T*2*n*(1/(2*a)) = T * ((2*n)* (1/(2*a)))
.= T * ( (2*n*1) / (2*a)) by XCMPLX_1:74
.= T*(n/a) by XCMPLX_1:91;
2*a-1 = 2*a*1 - (2*a)*(1/(2*a)) by XCMPLX_1:87;
then (2*a-1)|^n = ( (2*a) *(1 - 1/(2*a)))|^n
.= (2*a)|^n * (1+T*(n/a)) by A6,A5,NEWTON:7;
then (2*a)|^n + (2*a)|^n * (T*(n/a)) <= Py(a,n+1)
<= (2*a) |^ n +0 by HILB10_1:17;
then (2*a)|^n * (T*(n/a)) <= Py(a,n+1) - (2*a)|^n <= (2*a)|^n * (0*(n/a))
by XREAL_1:19,20;
then T*(n/a) <= (Py(a,n+1) - (2*a)|^n) / ((2*a)|^n) <= 0*(n/a)
by XREAL_1:77;
then consider T1 be _Theta such that
A7: T1* (n/a) = (Py(a,n+1) - (2*a)|^n) / ((2*a)|^n) by Th4;
take T1;
T1* (n/a) * ((2*a)|^n) = Py(a,n+1) - (2*a)|^n by A7,XCMPLX_1:87;
hence thesis;
end;
end;
theorem Th11:
for a be non trivial Nat,y,n be Nat st
y>0 &
n>0 &
(a^2-1)*y^2 +1 is square &
y,n are_congruent_mod a-1 &
y <= Py(a,a-1) &
n<= a-1
holds y = Py(a,n)
proof
let a be non trivial Nat,y,n be Nat such that
A1: y>0 & n>0 and
A2:(a^2-1)*y^2+1 is square and
A3: y,n are_congruent_mod a-1 and
A4: y <= Py(a,a-1) and
A5: n<= a-1;
a*a=a^2 by SQUARE_1:def 1;
then a^2>=1+0 by NAT_1:13;
then
A6: a^2-'1 = a^2-1 by XREAL_1:233;
consider x be Nat such that
A7: (a^2-1)*y^2 +1 = x^2 by A2,PYTHTRIP:def 3;
x^2 - (a^2-'1)*y^2 = 1 by A7,A6;
then [x,y] is Pell's_solution of a^2-'1 by Lm1;
then consider n1 be Nat such that
A8: x = Px(a,n1) & y = Py(a,n1) by HILB10_1:4;
A9: n1 <= a-1 by A4,A8,HILB10_1:11;
n1,y are_congruent_mod (a-1) by INT_1:14,A8,HILB10_1:24;
then consider i be Integer such that
A10: (a-1)*i = n1-n by INT_1:def 5,A3,INT_1:15;
n1 <>0 by A8,A1,HILB10_1:3;
then 0 -(a-1) < n1-n < a-1 -0 by A1,A5,A9,XREAL_1:15,14;
then (-1)*(a-1) < i *(a-1) < 1*(a-1) by A10;
then -1 < i <1+0 by XREAL_1:64;
then -1+1 <=i <= 0 by INT_1:7;
then i=0;
hence thesis by A10,A8;
end;
theorem Th12:
for a be non trivial Nat,s,n be Nat holds
s^2*(s|^n)^2-(s^2-1)*Py(a,n+1)*(s|^n)-1,0 are_congruent_mod 2*a*s-s^2-1
proof
let a be non trivial Nat,s be Nat;set S=s^2;
defpred P[Nat] means
S*(s|^$1)^2-(S-1)*Py(a,$1+1)*(s|^$1)-1,0 are_congruent_mod
2*a*s-s^2-1;
A1:Py(a,0+1) = Px(a,0) + Py(a,0)*a & Py(a,0) = 0 by HILB10_1:3,6;
then
A2: Py(a,0+1) =1 + 0*a by HILB10_1:3;
s|^0 = 1 by NEWTON:4;
then
A3: S*(s|^0)^2-(S-1)*Py(a,0+1)*(s|^0)-1
= S * (1*1) - (S-1)*1*1-1 by A2,SQUARE_1:def 1
.=0;
A4: for k be Nat st for n st n < k holds P[n] holds P[k]
proof
let k be Nat such that
A5: for n st n < k holds P[n];
set as2 = 2*a*s-S-1;
per cases by NAT_1:23;
suppose k=0;
hence thesis by A3,INT_1:11;
end;
suppose
A6: k =1;
A7: Py(a,0+2) = 2*a*Py(a,0+1) - Py(a,0) by HILB10_6:12;
s|^1 = s & s*s =s^2 by SQUARE_1:def 1;
then s^2*(s|^1)^2-(s^2-1)*Py(a,1+1)*(s|^1)-1 =
as2*(-s*s+1) by A7,A1,A2;
then as2 divides s^2*(s|^1)^2-(s^2-1)*Py(a,1+1)*(s|^1)-1 -0
by INT_1:def 3;
hence thesis by A6,INT_1:def 4;
end;
suppose k>=2;
then reconsider n =k-2 as Nat by NAT_1:21;
set Sn = s|^n;
A8: Py(a,n+1+2) = 2*a*Py(a,n+1+1) - Py(a,n+1) by HILB10_6:12;
A9: - S*Sn^2 +1,- S*Sn^2 +1 are_congruent_mod as2 by INT_1:11;
A10: -S,-S are_congruent_mod as2 by INT_1:11;
A11: -S*(s|^(n+1))^2 +1,-S*(s|^(n+1))^2+1 are_congruent_mod as2 by INT_1:11;
A12: (2*a)*s,(2*a)*s are_congruent_mod as2 by INT_1:11;
A13: -Sn^2 * S*S +1,-Sn^2 * S*S +1 are_congruent_mod as2 by INT_1:11;
A14: s|^(n+1+1)= s|^(n+1) *s & s|^(n+1) = Sn * s & S=s*s
by NEWTON:6,SQUARE_1:def 1;
A15: n+1<n+1+1 by NAT_1:13;
then S*(s|^(n+1))^2-(S-1)*Py(a,n+1+1)*(s|^(n+1))-1,0
are_congruent_mod as2 by A5;
then (S*(s|^(n+1))^2-(S-1)*Py(a,k)*(s|^(n+1))-1) +
(- S*(s|^(n+1))^2 +1), 0+(- S*(s|^(n+1))^2 +1)
are_congruent_mod as2 by A11,INT_1:16;
then
A16: (-(S-1)*Py(a,k)*(s|^(n+1)))*((2*a)*s), (1-S*(s|^(n+1))^2)*(2*a*s)
are_congruent_mod as2 by A12,INT_1:18;
n<k by A15,NAT_1:13;
then s^2*(s|^n)^2-(s^2-1)*Py(a,n+1)*Sn-1,0 are_congruent_mod as2 by A5;
then s^2*Sn^2-(s^2-1)*Py(a,n+1)*Sn-1+
(- s^2*Sn^2 +1), 0+(- s^2*Sn^2 +1) are_congruent_mod as2
by A9,INT_1:16;
then
A17: (-(S-1)*Py(a,n+1)*Sn)*(-S), (1- s^2*Sn^2)*(-S)
are_congruent_mod as2 by A10,INT_1:18;
S*(s|^k)^2-1, S*(s|^k)^2-1 are_congruent_mod as2 by INT_1:11;
then S*(s|^k)^2-1+(s^2-1)*Py(a,n+1)*(s|^k),
S*(s|^k)^2-1 +(1- S*(s|^n)^2)*(-S)
are_congruent_mod as2 by A14,A17,INT_1:16;
then
A18: S*(s|^k)^2-1+(S-1)*Py(a,n+1)*(s|^k)+(-(S-1)*(2*a*Py(a,k))*(s|^k)),
S*(s|^k)^2-1 +(1- S*(s|^n)^2)*(-S) +(1-S*(s|^(n+1))^2)*(2*a*s)
are_congruent_mod as2 by A16,A14,INT_1:16;
s|^k = Sn*(s*s) by A14;
then
A19: (s|^k)^2 = Sn^2 * (s*s)^2 by SQUARE_1:9
.= Sn^2 * (S*S) by SQUARE_1:9;
A20: (s|^(n+1))^2 = Sn^2*S by A14,SQUARE_1:9;
as2,0 are_congruent_mod as2 by INT_1:12;
then (- Sn^2 * S*S +1)*as2,0*(- Sn^2 * S*S +1) are_congruent_mod as2
by A13,INT_1:18;
hence thesis by A8,A20,A19,A18,INT_1:15;
end;
end;
P[n] from NAT_1:sch 4(A4);
hence thesis;
end;
theorem Th13:
for a be non trivial Nat,s,n,r be Nat st
s > 0 & r > 0 &
s^2*r^2 - (s^2-1)*Py(a,n+1)*r -1,0 are_congruent_mod 2*a*s-s^2-1 &
s*((s|^n)^2*(s|^n))< a &
s*(r^2*r) < a
holds r = s|^n
proof
let a be non trivial Nat,s,n,r be Nat such that
A1: s>0& r >0 and
A2: s^2*r^2 - (s^2-1)*Py(a,n+1)*r -1, 0 are_congruent_mod 2*a*s-s^2-1 &
s*((s|^n)^2*(s|^n))< a & s* (r^2*r) < a;
set 2sa=2*a*s-s^2-1, P=Py(a,n+1);
A3:r,r are_congruent_mod 2sa by INT_1:11;
s^2*(s|^n)^2-(s^2-1)*P*(s|^n)-1,0 are_congruent_mod2sa by Th12;
then
A4: (s^2*(s|^n)^2-(s^2-1)*P*(s|^n)-1)*r,0*r are_congruent_mod2sa
by A3,INT_1:18;
A5: r^2 = r*r & (s|^n)^2 = (s|^n)*(s|^n) by SQUARE_1:def 1;
A6: (s^2*r^2 - (s^2-1)*P*r -1)*(s|^n) - (s^2*(s|^n)^2-(s^2-1)*P*(s|^n)-1)*r
= (r - (s|^n))*(s^2*r*(s|^n)+1) by A5;
s|^n,s|^n are_congruent_mod 2sa by INT_1:11;
then (s^2*r^2 - (s^2-1)*P*r -1)*(s|^n), 0*(s|^n) are_congruent_mod 2sa
by A2,INT_1:18;
then
A7: (r - (s|^n))*(s^2*r*(s|^n)+1),0-0 are_congruent_mod 2sa by A6,A4,INT_1:17;
set q=max(r,s|^n);
A8: r>=1+0 by A1,NAT_1:13;
A9: s|^n >=0+1 by A1,NAT_1:13;
A10: |. (r - (s|^n)).| <= q-1
proof
per cases;
suppose r - (s|^n) >=0; then
|. (r - (s|^n)).| = r - (s|^n) <= r -1
by ABSVALUE:def 1,A9,XREAL_1:10;
hence thesis by XXREAL_0:def 10,XREAL_1:49;
end;
suppose
A12: (r - (s|^n)) < 0; then
|. (r - (s|^n)).| = -(r - (s|^n)) by ABSVALUE:def 1;
then |. (r - (s|^n)).| = s|^n -r <= s|^n -1 by A8,XREAL_1:10;
hence thesis by A12,XXREAL_0:def 10,XREAL_1:48;
end;
end;
|.(s^2*r*(s|^n)+1) .| = (s^2*r*(s|^n)+1);
then |. (r-(s|^n))*(s^2*r*(s|^n)+1) .|=|. (r - (s|^n)).| * (s^2*r*(s|^n)+1)
by COMPLEX1:65;
then |. (r - (s|^n))*(s^2*r*(s|^n)+1) .| <= (q-1) * (s^2*r*(s|^n)+1)
by A10,XREAL_1:64;
then
A13: |. (r - (s|^n))*(s^2*r*(s|^n)+1) .| +( s^2+1) <=
(q-1) * (s^2*r*(s|^n)+1) +( s^2+1) by XREAL_1:7;
(s|^n)*r >= 1*1 by A1,NAT_1:13,A9;
then (s|^n)*r*(s^2) >= 1*s^2 by XREAL_1:64;
then
A14: s^2 - s^2*r*(s|^n) <= 0 by XREAL_1:47;
A15: s^2=s*s & r^2 =r*r by SQUARE_1:def 1;
then s^2*r*(s|^n) *q >= 1*q by A1,NAT_1:14,XREAL_1:64;
then q +(s^2 - s^2*r*(s|^n)) <= s^2*r*(s|^n) *q +0 by A14,XREAL_1:7;
then q* s^2*r*(s|^n) + (q +s^2 - s^2*r*(s|^n)) <=
q* s^2*r*(s|^n) + s^2*r*(s|^n) *q by XREAL_1:7;
then
A16: |. (r - (s|^n))*(s^2*r*(s|^n)+1) .| +(s^2+1) <=
2* q* s^2*r*(s|^n) by A13,XXREAL_0:2;
consider I be Integer such that
A17: 2sa*I = (r - (s|^n))*(s^2*r*(s|^n)+1)-0 by A7,INT_1:def 5;
q* s^2*r*(s|^n) < a*s
proof
A18: s*((s|^n)^2*(s|^n))*s < a*s by XREAL_1:68,A1,A2;
per cases;
suppose
A19: r <= s|^n;
then q = s|^n by XXREAL_0:def 10;
then q* s^2*r*(s|^n) = (s|^n)* s^2*(s|^n)*r;
then q* s^2*r*(s|^n) <= (s|^n)* s^2*(s|^n) *(s|^n) &
(s|^n)^2 = (s|^n)*(s|^n) by A19,XREAL_1:64,SQUARE_1:def 1;
hence thesis by A15,A18,XXREAL_0:2;
end;
suppose
A20: r > s|^n;
then
A21: q = r by XXREAL_0:def 10;
then q* s^2*r*(s|^n) = q* s^2*q*(s|^n) <= q* s^2*q*q by A20,XREAL_1:64;
then q* s^2*r*(s|^n) <= s* (r^2*r)*s < a*s by A1,A2,A21,A15,XREAL_1:68;
hence thesis by XXREAL_0:2;
end;
end;
then q* s^2*r*(s|^n)*2 < a*s*2 by XREAL_1:68;
then |. (r - (s|^n))*(s^2*r*(s|^n)+1) .| +(s^2+1) <a*s*2 by A16,XXREAL_0:2;
then |. (r - (s|^n))*(s^2*r*(s|^n)+1) .| < a*s*2 - (s^2+1) by XREAL_1:20;
then |.2sa.|*|.I.| < 2sa by A17,COMPLEX1:65;
then |.2sa.|*|.I.| < |.2sa.|*1 by ABSVALUE:def 1;
then |.I.| < 1+0 by XREAL_1:66;
then I=0 by INT_1:7;
then (r - (s|^n))=0 by A17;
hence thesis;
end;
theorem Th14:
for a,b,c,d be Nat st a <= b <= c & 2*c <= d & c > 0
for f be FinSequence of REAL st
len f = b-a+1 &
for i be Nat st i+1 in dom f holds f.(i+1) =
(c choose (a+i)) * (d |^(c-'(a+i)))
holds
0 < Sum f < 2*(c|^a) * (d|^(c-'a))
proof
defpred P[Nat] means
for a,b,c,d be Nat st a <= b <= c & 2*c <= d & c>0 & b-a=$1
for f be FinSequence of REAL st len f = b-a+1 &
for i be Nat st i+1 in dom f holds f.(i+1) =
(c choose (a+i)) * (d |^(c-'(a+i))) holds
0 <= 1-(c/d)|^(b+1-'a) &
0 < Sum f <= (1-(c/d)|^(b+1-'a))/ (1-(c/d)) *c|^a* d|^(c-'a);
A1: P[0]
proof
let a,b,c,d be Nat such that A2: a <= b <= c & 2*c <= d & c > 0 & b-a=0;
A3: d>0 by A2;
let f be FinSequence of REAL such that
A4: len f = b-a+1 and
A5: for i be Nat st i+1 in dom f holds f.(i+1) =
(c choose (a+i)) * (d |^(c-'(a+i)));
A6: f.1 = (c choose (a+0)) * (d |^(c-'(a+0))) by A5,FINSEQ_3:25,A2,A4;
then reconsider f1=f.1 as Nat;
c-'a =c-a by A2,XREAL_1:233;
then
A7: c-'a+a = c;
A8: f = <*f1*> by A2,A4,FINSEQ_1:40;
A9: 1-(c/d) > 0
proof
assume 1-(c/d)<=0;
then 1 <= c/d by XREAL_1:50;
then 1*d <= c/d*d by XREAL_1:64;
then d<=c by XCMPLX_1:87;
then c + c <=c+0 by A2,XXREAL_0:2;
hence thesis by A2,XREAL_1:6;
end;
b+1 >a by A2,NAT_1:13;
then b+1-'a = b+1-a by XREAL_1:233;
then
A10: (1-(c/d)|^(b+1-'a))/ (1-(c/d)) = 1 by A2,A9,XCMPLX_1:60;
c choose a <= (c|^a) / (a!)<= (c|^a)/ 1
by NAT_1:14,XREAL_1:118,A2,HILB10_6:8;
then c choose a <= c|^a by XXREAL_0:2;
hence thesis by A3,A6,A8,A7,A9,A10,XREAL_1:64;
end;
A11:P[n] implies P[n+1]
proof
assume
A12: P[n];
set n1=n+1;
let a,b,c,d be Nat such that
A13: a <= b <= c & 2*c <= d & c > 0 & b-a=n1;
A14: d>0 by A13;
let f be FinSequence of REAL such that
A15: len f = b-a+1 and
A16: for i be Nat st i+1 in dom f holds f.(i+1) =
(c choose (a+i)) * (d |^(c-'(a+i)));
set 1cd = 1-(c/d);
b<>0 by A13;
then reconsider B=b-1 as Nat;
set F = f|n1;
f = F ^ <* f.(n1+1) *> by A13,A15,FINSEQ_3:55;
then
A17: Sum f = (Sum F) + f.(n1+1) by RVSUM_1:74;
c choose (a+n1) <= (c|^ (a+n1) ) / ((a+n1) !)<= (c|^(a+n1))/ 1
by NAT_1:14,XREAL_1:118,A13,HILB10_6:8;
then
A18: c choose (a+n1) <= c|^(a+n1) by XXREAL_0:2;
1<= n1+1 by NAT_1:11;
then
A19: f.(n1+1) = (c choose (a+n1)) * (d |^(c-'(a+n1)))
by A16,A13,A15,FINSEQ_3:25;
then
A20: f.(n1+1) <= c|^(a+n1) * (d |^(c-'(a+n1))) by A18,XREAL_1:64;
A21: n1 < n1+1 by NAT_1:13;
A22: len F = B-a+1 by A21,A13,A15,FINSEQ_1:59;
A23: for i be Nat st i+1 in dom F holds F.(i+1) =
(c choose (a+i)) * (d |^(c-'(a+i)))
proof
let i be Nat such that
A24: i+1 in dom F;
i+1 in dom f & f.(i+1) = F.(i+1) by A24,RELAT_1:57,FUNCT_1:47;
hence thesis by A16;
end;
B+1<=c by A13;
then
A25: B < c by NAT_1:13;
A26: a<=a +n < a+n+1 by NAT_1:11,13;
A27: 0 < Sum F <= (1 -(c/d)|^(B+1-'a))/ (1cd) *c|^a* d|^(c-'a)
by A12,A26,A13,A22,A23,A25;
c/d*d =c by A14,XCMPLX_1:87;
then
A28: c|^n1 = ( (c/d) |^n1) * (d|^n1) by NEWTON:7;
c-'(a+n1) = c -(a+n1) & c-'a = c-a by A13,XXREAL_0:2,XREAL_1:233;
then
A29: c-'a = n1 + (c-'(a+n1));
A30: 1cd > 0
proof
assume 1cd<=0;
then 1 <= c/d by XREAL_1:50;
then 1*d <= c/d*d by XREAL_1:64;
then d<=c by XCMPLX_1:87;
then c + c <=c+0 by A13,XXREAL_0:2;
hence thesis by A13,XREAL_1:6;
end;
A31: ((1-(c/d) |^(B+1-'a))/ 1cd *c|^a* d|^(c-'a)) +
((c|^a)*( (c/d) |^n1) * d|^(c-'a) ) =
(((1-(c/d)|^(B+1-'a))/1cd + (c/d) |^n1)) * (c|^a* d|^(c-'a));
A32: b-'a = n1 by A13,XREAL_1:233;
a < b+1 by A13,NAT_1:13;
then
A33: b+1-'a = b+1-a by XREAL_1:233;
A34: ((1-(c/d)|^(B+1-'a)) + ((c/d) |^n1* 1cd))=
(1-(c/d)|^n1) + (c/d) |^n1 - ( (c/d) |^n1 * (c/d)) by A32
.= 1 - ( (c/d) |^(n1+1)) by NEWTON:6
.= 1 - ( (c/d) |^(b+1-'a)) by A33,A13;
A35:(1-(c/d)|^(B+1-'a))/ 1cd + (c/d) |^n1 =
(1-(c/d)|^(B+1-'a))/1cd + ((c/d) |^n1* 1cd) / 1cd by A30,XCMPLX_1:89
.= ((1-(c/d)|^(B+1-'a)) + ((c/d) |^n1* 1cd)) / 1cd by XCMPLX_1:62;
c|^(a+n1) * (d |^(c-'(a+n1))) =
(c|^a)*(( (c/d) |^n1) * (d|^n1)) * (d |^(c-'(a+n1)))
by NEWTON:8,A28
.= (c|^a)*( (c/d) |^n1) * ((d|^n1) * (d |^(c-'(a+n1))))
.= (c|^a)*( (c/d) |^n1) * d|^(c-'a) by A29,NEWTON:8;
hence thesis by A19,A35,A17,A27,A20, A30,A34,XREAL_1:7,A31;
end;
let a,b,c,d be Nat such that
A36: a <= b <= c & 2*c <= d & c >0;
A37: d>0 by A36;
let f be FinSequence of REAL such that
A38: len f = b-a+1 &
for i be Nat st i+1 in dom f holds f.(i+1) =
(c choose (a+i)) * (d |^(c-'(a+i)));
reconsider ba=b-a as Nat by A36,NAT_1:21;
P[n] from NAT_1:sch 2(A1,A11);
then
A39: P[ba];
then
A40: 0 < Sum f <= (1-(c/d)|^(b+1-'a))/ (1-(c/d)) *c|^a* d|^(c-'a) by A36,A38;
A41: (1-(c/d)|^(b+1-'a))>=0 by A36,A38,A39;
2*c <= d*1 by A36;
then c/d <=1/2 by A37,XREAL_1:102;
then 1 - c/d >= 1 - 1/2 by XREAL_1:10;
then
A42: (1-(c/d)|^(b+1-'a))/ (1-(c/d)) <= (1-(c/d)|^(b+1-'a)) /(1/2)
by A41,XREAL_1:118;
1-(c/d)|^(b+1-'a) < 1-0 by A36,A37,XREAL_1:10;
then (1-(c/d)|^(b+1-'a))*2 < (1-0)*2 by XREAL_1:68;
then (1-(c/d)|^(b+1-'a))/ (1-(c/d)) < 2 by A42,XXREAL_0:2;
then (1-(c/d)|^(b+1-'a))/ (1-(c/d)) *(c|^a* d|^(c-'a)) < 2*(c|^a* d|^(c-'a))
by A36,A37,XREAL_1:68;
hence thesis by A40,XXREAL_0:2;
end;
theorem Th15:
for f,k,m,r,s,t,u be Nat,W,M,U,S,T,Q be Integer st
f>0 & k >0 & m>0 & u>0 &
(M^2-1)*S^2 +1 is square &
((M*U)^2 -1)*T^2 + 1 is square &
W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
W = 100*f*k*(k+1) &
U = 100 * (u|^3)*(W|^3)+1 &
M = 100 * m * U *W+1 &
S = (M-1)*s+k+1 &
T = (M*U-1)*t +W-k+1 &
Q = 2*M*W-W^2 -1
holds
M*(U+1) is non trivial Nat & W is Nat &
for mu be non trivial Nat,w be Nat st mu = M*(U+1) & w = W &
r + W + 1 = Py(mu,w+1) holds f = k!
proof
let f,k,m,r,s,t,u be Nat,W,M,U,S,T,Q be Integer such that
A1: f>0 & k >0 & m>0 & u > 0 and
A2: (M^2-1)*S^2 +1 is square and
A3: ((M*U)^2 -1)*T^2 + 1 is square and
A4: W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q and
A5: (4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) and
A6: W = 100*f*k*(k+1) and
A7: U = 100 * (u|^3)*(W|^3)+1 and
A8: M = 100 * m * U *W+1 and
A9: S = (M-1)*s+k+1 and
A10: T = (M*U-1)*t +W-k+1 and
A11: Q = 2*M*W-W^2 -1;
set MM=M,UU=U,WW=W;
reconsider W,U,M,S as Element of NAT by A6,A7,A8,A9,INT_1:3;
A12: 100*f*k*(k+1) >= 1*(k+1) by A1, NAT_1:14,XREAL_1:64;
A13: W > k by A12,A6,NAT_1:13;
then
A14: W-k > 0 by XREAL_1:50;
then
A15:(M*U-1)*t +(W-k) >=0+0 by A7,A8;
then reconsider T as Element of NAT by A10,INT_1:3;
reconsider Wk=W-k as Nat by A13,NAT_1:21;
A16: M*W -1 >= 0 by A1,A6,A7,A8;
100 * m * U * W >= 1*W by XREAL_1:64,A1,A7,NAT_1:14;
then
A17: M > W by A8,NAT_1:13;
then M*W >= W*W = W^2 by XREAL_1:64,SQUARE_1:def 1;
then M*W+M*W >= M*W+W^2 by XREAL_1:7;
then M*W+M*W -(W^2+1) >= M*W+W^2 -(W^2+1) by XREAL_1:9;
then reconsider Q as Element of NAT by A16,A11,INT_1:3;
A18: U > 1 by A7,NAT_1:13,A1,A6,NAT_1:14;
A19: M>=1 & U+1>1 by A6,A7,A8,NAT_1:14,13;
then M*(U+1) > 1*1 & WW=W by XREAL_1:97;
hence MM*(UU+1) is non trivial Nat & WW is Nat by NEWTON03:def 1;
M*U > 1*1 by A19,A18,XREAL_1:97;
then reconsider MU=M*U as non trivial Nat by NEWTON03:def 1;
W>= 1 by A1,A6,NAT_1:14;
then M>1 by A17,XXREAL_0:2;
then reconsider M as non trivial Nat by NEWTON03:def 1;
reconsider M1=M-1 as Nat;
let mu be non trivial Nat, w be Nat such that
A20: mu = MM*(UU+1) & w = WW & r + WW + 1 = Py(mu,w+1);
set R = r - m*S*T*U;
A21: u^2 = u*u & S^2=S*S & R^2 = R*R & T^2=T*T & f^2=f*f by SQUARE_1:def 1;
0 < 8*f*u*S*T*R by A1,A21,A5;
then
A22:R>0;
m*T*U*S >= S*1 by XREAL_1:64,A1,A7,A15,A10,NAT_1:14;
then 0< r-S by A22,XREAL_1:10;
then
A23: S < r by XREAL_1:47;
m*S*U*T >= T*1 by XREAL_1:64,NAT_1:14,A1,A6,A7,A8,A9;
then 0< r-T by A22,XREAL_1:10;
then
A24: T < r by XREAL_1:47;
A25: ((u/(r/(S*T)-m*U)) -f)*((u/(r/(S*T)-m*U)) -f)<1/4
proof
4*f^2*R^2 -R^2 + 4*u^2*S^2*T^2 -8*f*u*S*T*R < 0
by A5,XREAL_1:49;
then 4*f^2*R^2 -R^2 + 4*u^2*S^2*T^2 -8*f*u*S*T*R +R^2 < 0+R^2
by XREAL_1:8;
then 4*((u*S*T-f*R)*(u*S*T-f*R)) < R*R*1 by A21;
then
A26: 1/4 > ((u*S*T-f*R)*(u*S*T-f*R))/(R*R) by XREAL_1:106;
(u*S*T-f*R)/R = (u*S*T)/R-(f*R)/R by XCMPLX_1:120
.= (u*(S*T))/R-f by A22,XCMPLX_1:89
.= (u/(R/(S*T)))-f by XCMPLX_1:77
.= (u/(r/(S*T)-((m*U)*(S*T))/(S*T)))-f by XCMPLX_1:120
.= (u/(r/(S*T)-m*U)) -f by XCMPLX_1:89,A8,A9,A15,A10;
hence thesis by A26,XCMPLX_1:76;
end;
A27: r < Py(M,M1) & r < Py(M,MU-1)
proof
A28: r+0 < r+(W+1) by XREAL_1:8;
A29: Py(mu,w+1) <= (2*(M*(U+1))) |^ W by A20,HILB10_1:17;
U>=1+1 by NAT_1:13,A18;
then reconsider u2=U-2 as Nat by NAT_1:21;
A30: (M|^2)*1<= (M|^2)*(M|^u2) = M|^(2+u2)
by NAT_1:14,NEWTON:8,XREAL_1:64;
A31: M|^(1+1)=M * M|^1 & M|^1 = M by NEWTON:6;
100 * m * W * U >= 1*U by XREAL_1:64,A1,A6,NAT_1:14;
then M > U by A8,NAT_1:13;
then M>= U+1 by NAT_1:13;
then M*(U+1) <= M*M by XREAL_1:64;
then 0<M*(U+1) <=M|^U by A30,A31,XXREAL_0:2;
then
A32:2*(M*(U+1)) <=2*(M|^U) by XREAL_1:64;
U>=1 by A6,A7,NAT_1:14;
then 2*(M|^U) <= 2|^U*(M|^U) by PREPOWER:12,XREAL_1:64;
then 2*(M|^U) <= (2*M)|^U by NEWTON:7;
then 2*(M*(U+1)) <= (2*M)|^U by A32,XXREAL_0:2;
then (2*(M*(U+1))) |^W <= ((2*M)|^U)|^W by PREPOWER:9;
then A33: (2*(M*(U+1))) |^W <= (2*M) |^(U*W) by NEWTON:9;
((2*M) |^(U*W))|^1 = (2*M) |^(U*W);
then A34: (2*M) |^(U*W) *(2*M) |^(U*W)=((2*M) |^(U*W))|^(1+1) by NEWTON:6
.= (2*M) |^(U*W*2) by NEWTON:9;
U*W>=1 & 2*M >=1 & M>=1 by A1,A6,A7,NAT_1:14;
then (2*M) |^(U*W) >=2*M >=2*1 by PREPOWER:12,XREAL_1:64;
then 1*2<=(2*M) |^(U*W) by XXREAL_0:2;
then 1<= (2*M) |^(U*W) /2 by XREAL_1:77;
then (2*M) |^(U*W)*1 <= (2*M) |^(U*W) * ((2*M) |^(U*W)*(1 /2))
by XREAL_1:64;
then
A35: (2*(M*(U+1))) |^W <= (2*M) |^(U*W*2) *(1 /2) by A34,A33,XXREAL_0:2;
100 * U *W*m>= 100 * U *W *1 by A1,NAT_1:14,XREAL_1:64;
then
A36: M > 100 *U*W by A8,NAT_1:13;
A37: 4*(U*W) <= 100 *(U*W) & 2*(U*W) <= 100 *(U*W) by XREAL_1:64;
then
A38: 4*U*W < M & 2*U*W < M by A36,XXREAL_0:2;
consider t be _Theta such that
A39: Py(M,2*U*W+1) = (2*M) |^(U*W*2) * (1+t*((2*U*W)/M))
by A37,A36,XXREAL_0:2,Th10;
-1 <=t by Def1;
then
A40: (-1)*(4*U*W) <= t * (4*U*W) by XREAL_1:64;
(-1)*M <= (-1) * (4*U*W) by A38,XREAL_1:65;
then -M <= t * (2*U*W)*2 by A40,XXREAL_0:2;
then M*(-1/2)=(M * (-1)) /2 <= t * (2*U*W) by XREAL_1:79;
then (-1/2) <= (t * (2*U*W)) / M by XREAL_1:77;
then (-1/2) <= t * ((2*U*W) / M) by XCMPLX_1:74;
then 1/2 = 1+(-1/2) <= 1+ t * ((2*U*W) / M) by XREAL_1:7;
then (2*M) |^(U*W*2) * (1/2) <= (2*M) |^(U*W*2) *
(1+ t * ((2*U*W) / M)) by XREAL_1:64;
then
A41: (2*(M*(U+1))) |^W <= Py(M,2*U*W+1) by A35,A39,XXREAL_0:2;
A42: 2*U>=2*1 by A7,A6,NAT_1:14,XREAL_1:64;
m*U >= 1 & W>=1 by A1,A6,A7,NAT_1:14;
then 100*(m*U) >= 3*1 by XREAL_1:66;
then 100*(m*U)*W >= 3*W by XREAL_1:64;
then M >= 2*W+W+1 =2*W+1+W >= 2*W +1+1 by A1,A6,NAT_1:14,XREAL_1:6,A8;
then 2*W+2 <= M by XXREAL_0:2;
then (2*W+2)*U <= MU by XREAL_1:64;
then 2*W*U +2 <= 2*W*U +2*U <=MU by A42,XREAL_1:6;
then 2*W*U +1 + 1 <= MU by XXREAL_0:2;
then 2*W*U +1 <= MU-1 by XREAL_1:19;
then 2*(U*W)+1 < MU-1 or 2*(U*W)+1 = MU-1 by XXREAL_0:1;
then
A43: Py(M,2*U*W+1) <= Py(M,MU-1) by HILB10_1:11;
2*(U*W)+1 <= 100 *(U*W) by NAT_1:13,A1,A6,A7,XREAL_1:68;
then 2*(U*W)+1< M=M1+1 by A36,XXREAL_0:2;
then 2*(U*W)+1<= M1 by NAT_1:13;
then 2*(U*W)+1< M1 or 2*(U*W)+1 = M1 by XXREAL_0:1;
then
A44: Py(M,2*U*W+1) <= Py(M,M1) by HILB10_1:11;
r < (2*(M*(U+1))) |^W by A28,A20,A29,XXREAL_0:2;
then r < Py(M,2*U*W+1) by A41,XXREAL_0:2;
hence thesis by A43,A44,XXREAL_0:2;
end;
A45: U>=1 by A6,A7,NAT_1:14;
A46: 100 * m * U *W>= 1*W by XREAL_1:64,A1,A7,NAT_1:14;
then W+1 <= M-1+1 by A8,XREAL_1:6;
then
A47: (W+1)*1 <= M*U by A45,XREAL_1:66;
A48: S = Py(M,k+1)
proof
A49: S < Py(M,M1) by A27,A23,XXREAL_0:2;
A50: M-1 >= k+1 by A46,A8,A6,A12,XXREAL_0:2;
S-(k+1) = s*(M-1) by A9;
then S,(k+1) are_congruent_mod M-1 by INT_1:def 3,def 4;
hence thesis by A2,A49,A50,Th11,A9;
end;
A51: T = Py(MU,Wk+1)
proof
M*1 <= MU by XREAL_1:64,A6,A7,NAT_1:14;
then Py(M,MU-1) <= Py(MU,MU-1) by HILB10_6:15;
then r < Py(MU,MU-1) by A27,XXREAL_0:2;
then
A52: T < Py(MU,MU-1) by A24,XXREAL_0:2;
A53: 1-k <= 1-1=0 by XREAL_1:10,A1,NAT_1:14;
(1-k)+(W+1) <= 0+(W+1) <= MU by A47,A53,XREAL_1:6;
then Wk+1+1<= MU by XXREAL_0:2;
then
A54: Wk+1<= MU-1 by XREAL_1:19;
T-(Wk+1) = (MU-1)*t by A10;
hence thesis by A54,A52,A10,A15,A3,Th11,INT_1:def 5;
end;
A55: R < 3*u*S*T
proof
(4*f^2 -1)*R^2 + 0 <= (4*f^2 -1)*R^2 + 4*u^2*S^2*T^2 by XREAL_1:6;
then
A56: (4*f^2 -1)*R^2 < 8*f*u*S*T*R by A5,XXREAL_0:2;
A57: 4*1 <= 4*f & 12*f*1 <= 12*f*f by XREAL_1:64,A1,NAT_1:14;
then 4*1 +8*f <= 4*f +8*f by XREAL_1:6;
then 3 +8*f +1 <= 12 *f^2 by A57,A21,XXREAL_0:2;
then 8*f + 3 < 12 *f^2 by NAT_1:13;
then 8*f < 12*f^2 - 3 by XREAL_1:20;
then (8*f)*(u*S*T*R) <= 3*(4*f^2-1)* (u*S*T*R) by A22,XREAL_1:64;
then (4*f^2 -1)*R^2 < (4*f^2-1)* (3*u*S*T*R) by A56,XXREAL_0:2;
then R*R < 3*u*S*T*R by A1,XREAL_1:64,A21;
hence thesis by XREAL_1:64;
end;
A58: m*U + 3*u > r / (S*T)
proof
r < 3*u*S*T + m*S*T*U by A55,XREAL_1:19;
then r < (3*u + m*U)* (S*T);
hence thesis by A15,A10,A8,A9,XREAL_1:83;
end;
U < U+1 by NAT_1:13;
then M*U <=M*(U+1) by XREAL_1:64;
then W+1 <= M*(U+1) by A47,XXREAL_0:2;
then W < M*(U+1) by NAT_1:13;
then consider t1 be _Theta such that
A59: Py(mu,w+1) = (2*mu) |^w *(1+t1*(w/mu)) by A20,Th10;
reconsider I=1 as _Theta by Def1;
set E=t1*(w/mu)- ( W+1) / (2*mu) |^w;
W|^(1+1) = W* W|^1 & W|^1=W by NEWTON:6;
then
A60: W|^(2+1) = W*W*W by NEWTON:6;
u|^(1+1) = u* u|^1 & u|^1=u by NEWTON:6;
then
A61: u|^(2+1) = u*u*u by NEWTON:6;
A62: W>=1 by A1,A6,NAT_1:14;
A63: m>=1 by A1,NAT_1:14;
A64: 2*mu >=1 by NAT_1:14;
(f*k*100)*(k+1) >= (f*k*100)*1 & f >=1 by XREAL_1:64,A1,NAT_1:14;
then W >= f*(100*k) >= 1*(100*k) by A6, XREAL_1:64;
then
A65: W>= 100*k>=5*k & 100*k>=1*k by XXREAL_0:2,XREAL_1:64;
then
A66: k <= W by XXREAL_0:2;
U > 100 * ((u|^3)*(W|^3))>= 1*(u|^3*W|^3) by A7,NAT_1:13,XREAL_1:64;
then U > u|^3*W|^3 by A7,NAT_1:13;
then
A67: U|^k >= (u|^3*W|^3)|^k by A1,A6,PREPOWER:9;
A68: u>=1 by NAT_1:14,A1;
then
A69: u|^3 >= u & W|^3 >=1 & W|^3 >= W & u|^3 >=1
by A62,PREPOWER:12,NAT_1:14;
then u|^3*W|^3 >= u*1 & u|^3*W|^3 >= W*1 by XREAL_1:66;
then U > 100*(u|^3*W|^3) >= 100*u & 100*(u|^3*W|^3) >=100*W
by XREAL_1:64,NAT_1:13,A7;
then
A70: U >= 100 *u >= 12* u&U >= 100*W&100*u >= 16* u by XXREAL_0:2,XREAL_1:64;
then
A71: U>=12* u by XXREAL_0:2;
W|^k|^(1+1) =(W|^k|^1) * (W|^k) & W|^k|^1 = (W|^k) by NEWTON:6;
then W|^k|^(2+1) = (W|^k)*(W|^k)*(W|^k) by NEWTON:6;
then A72: (W|^k)^2*(W|^k) = W|^k|^3 by SQUARE_1:def 1;
k>=1 by A1,NAT_1:14;
then u|^k >= u by A68,PREPOWER:12;
then ( u|^k|^3) >= u|^3 by A1,PREPOWER:9;
then
A73: ( u|^k|^3) >=u^2*u by A61,SQUARE_1:def 1;
m*U >=1 by NAT_1:14,A1,A20,A7;
then (100*W)*(m*U) >= 100*W*1 >= 5 * k by A66,XREAL_1:66;
then (100*W)*(m*U) >= 5*k by XXREAL_0:2;
then
A74: 5*k <= M by NAT_1:13,A8;
then
A75: (5*k)/M <=1 by XREAL_1:183;
A76: 2*k <= 5*k by XREAL_1:64;
then
A77: M>=2*k by A74,XXREAL_0:2;
then (2*k)/M <=1 by XREAL_1:183;
then
A78: 2*(k/M)<=1 by XCMPLX_1:74;
A79: 4*W <= 100*W & 2*W <= 100*W by XREAL_1:64;
then
A80: 4*W <= U & 2*W <= U by A70,XXREAL_0:2;
then
A81: (2*W) <= U+1 by NAT_1:13;
W <= W+W by NAT_1:11;
then
A82: W <=U by A80,XXREAL_0:2;
Wk <= W-0 by XREAL_1:10;
then 4* Wk <= 4*W & 2* Wk <= 2*W by XREAL_1:64;
then
A83: 4*Wk <= U & 2*Wk <= U by A80,XXREAL_0:2;
then (4*Wk)/U <=1 by XREAL_1:183;
then
A84: (4*Wk)/U* (1/M) <= 1 * (1/M) by XREAL_1:64;
2*(2*(Wk/MU)) = 4 *(Wk/MU)
.= (4*Wk)/MU by XCMPLX_1:74
.= (4*Wk)/U* (1/M) by XCMPLX_1:103;
then
A85: 2*(1/M)+ 2*(2*(Wk/MU)) <= 2*(1/M) + 1*(1/M) = 3*(1/M) =(3*1)/M
by A84,XREAL_1:6,XCMPLX_1:74;
3*1 <= 3*k by XREAL_1:64,A1,NAT_1:14;
then (3*1)/M <= (3*k) /M by XREAL_1:72;
then 2*(1/M) + 2*(2*(Wk/MU)) <= (3*k) /M by A85,XXREAL_0:2;
then
A86: 2*(k/M)+ (2*(1/M)+ 2*(2*(Wk/MU))) <= 2*(k/M)+ (3*k) /M by XREAL_1:6;
2*(k/M) = (2*k)/M by XCMPLX_1:74;
then
A87: 2*(k/M)+ (3*k) /M = (2*k+3*k)/M by XCMPLX_1:62;
2*(k/M)+ 2*(1/M) + 0 <= 2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU)) <= 1
by A86,A87,A75,XXREAL_0:2,XREAL_1:6;
then
A88: 2*(k/M)+ 2*(1/M) <= 1 by XXREAL_0:2;
A89: 2*W <= U by A79,A70,XXREAL_0:2;
M>=1 by NAT_1:14;
then
A90: MU>=1*(2*Wk) by A83,XREAL_1:66;
(3*2)*u <= 12*u by XREAL_1:64;
then 3*u*2 <= 1*U by A71,XXREAL_0:2;
then
A91: (3*u/U) <= 1/2 by XREAL_1:102,A20,A7;
4*u*4 <= 1*U by A70,XXREAL_0:2;
then
A92: (4*u/U) <= 1/4 by XREAL_1:102,A20,A7;
1* mu >= M * (2*W) by A81,A20,XREAL_1:64;
then (W*(2*M))/mu <= 1 by XREAL_1:79;
then (2*M)*(W/mu) <= 1 by XCMPLX_1:74;
then
A93: W/mu <= 1/(2*M) by XREAL_1:77;
then
A94: -(W/mu) >= - 1/(2*M) by XREAL_1:24;
-1 <= t1 <= 1 by Def1;
then (-1)*(w/mu) <= t1*(w/mu) <= 1*(w/mu) by XREAL_1:64;
then
A95: -(1/(2*M)) <= t1*(w/mu) <= 1/(2*M) by A20,A93,A94,XXREAL_0:2;
W+1 <= U+1 by A82,XREAL_1:6;
then
A96: (W+1)*(2*M) <= (U+1) * (2*M) by XREAL_1:64;
(2*mu) <= (2*mu) |^w by A64,A20,A62,PREPOWER:12;
then (W+1) *(2*M) <= 1 * (2*mu) |^w by A20,A96,XXREAL_0:2;
then ( W+1) / (2*mu) |^w <= 1/(2*M) by XREAL_1:102;
then 1/(2*M) >= - ( W+1) / (2*mu) |^w >= - 1/(2*M) by XREAL_1:24;
then
A97: - 1/(2*M) + -1/(2*M) <= t1*(w/mu) + - ( W+1) / (2*mu) |^w
<= 1/(2*M)+1/(2*M) by A95,XREAL_1:7;
A98: (1*1)/(2*M) = 1/2 * (1/M) by XCMPLX_1:76;
A99:t1*(w/mu)- ( W+1) / (2*mu) |^w <= I* (1/M) by A97,A98;
A100: (-I) * (1/M) <= t1*(w/mu)- ( W+1) / (2*mu)|^w by A97,A98;
consider t2 be _Theta such that
A101: t1*(w/mu)- ( W+1) / (2*mu)|^W = t2 * (1/M) by A20,A99,A100,Th4;
A102: r = (2*mu) |^w *(1+t1*(w/mu)) - (W+1) by A59,A20;
r = (2*mu) |^w *(1+t1*(w/mu)) - ( ((W+1) / (2*mu)|^W) * ((2*mu)|^W))
by A102,XCMPLX_1:87;
then r = (2*mu) |^w *((1+t1*(w/mu)) - (W+1) / (2*mu)|^W ) by A20;
then
A103: r = (2*mu) |^w * (1 + t2 * (1/M)) by A101;
S <= (2*M)|^k & T <= (2*MU)|^Wk by A48,A51,HILB10_1:17;
then S*T <= ((2*M)|^k) * ((2*MU)|^Wk) by XREAL_1:66;
then
A104:r / (S*T) >= r / (((2*M)|^k) * ((2*MU)|^Wk)) by XREAL_1:118,A9,A10,A15;
((2*M)*U)|^Wk = (2*M) |^Wk * U|^Wk by NEWTON:7;
then
A105:((2*M)|^k) * ((2*MU)|^Wk) = (2*M)|^k * (2*M) |^Wk * U|^Wk
.= (2*M)|^(k+Wk) * U|^Wk by NEWTON:8;
(2*mu) |^w = ((2*M)*(U+1)) |^W by A20
.= (2*M)|^W * (U+1) |^W by NEWTON:7;
then
A106: r / (((2*M)|^k) * ((2*MU)|^Wk)) =
( (2*M)|^W *( (U+1) |^W * (1 + t2 * (1/M))))/ ((2*M)|^W * U|^Wk)
by A103,A105
.= ((U+1) |^W * (1 + t2 * (1/M)) ) / (( U|^Wk)* 1) by XCMPLX_1:91
.= (((U+1) |^W )/ ( U|^Wk)) * ((1 + t2 * (1/M)) / 1) by XCMPLX_1:76
.= (((U+1) |^W )/ ( U|^Wk)) * (1 + t2 * (1/M));
1/M <= 1/2 by NAT_2:29,XREAL_1:118;
then
A107: -(1/M) >= -(1/2) by XREAL_1:24;
-1<= t2 <= 1 by Def1;
then (-1)*(1/M) <= t2*(1/M) by XREAL_1:64;
then -(1/2) <= t2*(1/M) by A107,XXREAL_0:2;
then 1+-(1/2) <= 1+ t2 * (1/M) by XREAL_1:6;
then (((U+1) |^W )/ ( U|^Wk)) * (1 + t2 * (1/M)) >=
(1/2) * (((U+1) |^W )/ ( U|^Wk)) by XREAL_1:66;
then
A108: r/(S*T) >= (1/2) * (((U+1) |^W )/ ( U|^Wk))
by A104,A106,XXREAL_0:2;
U < U+1 by NAT_1:13;
then U |^W < (U+1) |^W by PREPOWER:10,A1,A6,NAT_1:14;
then
A109:(U |^W)/ ( U|^Wk) < (U+1) |^W / ( U|^Wk) by A7,XREAL_1:74;
A110: U |^(Wk+k)= (U |^Wk) * (U |^k) by NEWTON:8;
then (U |^W)/ (( U|^Wk)*1) = ((U |^k)/1) by A7,XCMPLX_1:91;
then (1/2)*(U |^k) < (1/2)*(((U+1) |^W)/ ( U|^Wk)) by XREAL_1:68,A109;
then
A111: r/(S*T) > 1/2 * (U |^k) by A108,XXREAL_0:2;
m *U >= 1*(12*u) by A71,A63,XREAL_1:66;
then 20*(m*U) >= 20*(12*u) by XREAL_1:66;
then 20*m*U*W >= 240*u*W by XREAL_1:66;
then
A112: 80*(m*U*W) + 20*(m*U*W) >= 80*(m*U*W) + (80*3)*u*W by XREAL_1:6;
m*U+3*u > 1/2 * (U |^k) >= 1/2 * (((u|^3)*(W|^3))|^k)
by A58,A67,A111,XXREAL_0:2,XREAL_1:66;
then m*U+3*u > 1/2 * (((u|^3)*(W|^3))|^k) by XXREAL_0:2;
then
A113: (m*U+3*u)*(80*W) >= (1/2 * (((u|^3)*(W|^3))|^k)) * (80*W) by
XREAL_1:66;
A114: M > 80*(m*U+3*u)*W by NAT_1:13,A8,A112;
(((u|^3)*(W|^3))|^k) *W = (((u|^3)|^k)*((W|^3)|^k)) *W
by NEWTON:7
.= ((u|^(k*3)) * ((W|^3)|^k)) *W by NEWTON:9
.= ((u|^(k*3)) * (W|^(3*k))) *W by NEWTON:9
.= (( (u|^k)|^3)) * (W|^(3*k)) *W by NEWTON:9
.= ( u|^k|^3) * (W|^k|^3) *W by NEWTON:9;
then
A115: M > 40 * ( u|^k|^3) * (W|^k|^3) *W by A113,A114,XXREAL_0:2;
(40 *(u|^k|^3)) * ((W|^k|^3) *W) >= 1* ((W|^k|^3) *W)
by A1,NAT_1:14,XREAL_1:64;
then
A116: M > W*((W|^k)^2*(W|^k)) by A72,A115,XXREAL_0:2;
40* (W|^k|^3)>=1 by NAT_1:14,A6,A1;
then (40* (W|^k|^3)) * (u|^k|^3) >= 1*(u^2*u) by A73, XREAL_1:66;
then (40* (W|^k|^3)) * (u|^k|^3)*W >= 1*(u^2*u)*W by XREAL_1:66;
then W* (u^2*u) < M by A115,XXREAL_0:2;
then
A117: u=W|^k by A116,Th13,A6,A1,A4,A48,A11;
A118: R/(S*T*U) = r/(S*T*U) - (m*(S*T*U))/(1*(S*T*U)) by XCMPLX_1:120
.= r/(S*T*U) - (m/1) by A15,A10,A7,A8,A9,XCMPLX_1:91;
R/(S*T*U) < (3*u*(S*T))/(S*T*U) by A55,A8,A9,A15,A10,A7,XREAL_1:74;
then r/(S*T*U) - (m/1) < (3*u)/U by A118,A8,A9,A15,A10,XCMPLX_1:91;
then
A119 : r/(S*T*U) - (m/1) < 1/2 by A91,XXREAL_0:2;
2*k >= 1*k by XREAL_1:64;
then consider t3 be _Theta such that
A120: Py(M,k+1) = (2*M)|^k *(1+ t3*(k/M)) by Th10,A77,XXREAL_0:2;
2*Wk >= 1*Wk by XREAL_1:64;
then consider t4 be _Theta such that
A121: Py(MU,Wk+1) = (2*MU)|^Wk *(1+ t4*(Wk/MU)) by Th10,A90,XXREAL_0:2;
1*M>=2*k by A76,A74,XXREAL_0:2;
then k/M <=1/2 by XREAL_1:102;
then consider T3 be _Theta such that
A122: 1/ (1+ t3*(k/M)) = 1+T3*2*(k/M) by Th7;
1*MU>=2*Wk by A90;
then Wk/MU <=1/2 by XREAL_1:102;
then consider T4 be _Theta such that
A123: 1/ (1+ t4*(Wk/MU)) = 1+T4*2*(Wk/MU) by Th7;
consider T5 be _Theta such that
A124: (1+T3*(2*(k/M)))* (1 + t2 * (1/M)) = 1+T5*(2*(k/M)+ 2*(1/M))by A78,Th3;
consider T6 be _Theta such that
A125: (1+T5*(2*(k/M)+ 2*(1/M)))* (1+T4*(2*(Wk/MU))) =
1+T6 *(2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU))) by A88,Th3;
A126: |.2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU)).|
= 2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU));
|.(5*k)/M.| = (5*k)/M;
then consider T7 be _Theta such that
A127: T6*(2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU))) = T7* ((5*k)/M)
by A87,A126, Th2,A86;
A128: 1/S = (1/(2*M)|^k) * (1+T3*2*(k/M)) by A120,A48,XCMPLX_1:102,A122;
A129: 1/T = (1/(2*MU)|^Wk) *(1+T4*2*(Wk/MU)) by A123,A121,A51,XCMPLX_1:102;
A130:(2*mu) |^w = ((2*M)*(U+1)) |^W by A20
.= ((2*M)|^W) *((U+1) |^W) by NEWTON:7;
(1/(2*M)|^k) * (1/(2*MU)|^Wk)
= 1/ ( (2*M)|^W * U|^Wk) by A105,XCMPLX_1:102;
then
A131: ((2*mu) |^w) * (1/(2*M)|^k) * (1/(2*MU)|^Wk) =
(((2*M)|^W) *((U+1) |^W)) *(1 / ( (2*M)|^W * U|^Wk)) by A130
.= (((2*M)|^W) *((U+1) |^W)) / ( (2*M)|^W * U|^Wk) by XCMPLX_1:99
.= ((U+1) |^W) / (U|^Wk) by XCMPLX_1:91;
A132: r/(S*T) = r * (1/(S*T)) by XCMPLX_1:99
.= r * ((1/S) *(1/T)) by XCMPLX_1:102
.= (((U+1) |^W) / (U|^Wk)) *((1+t2*(1/M))*(1+T3*2*(k/M))*(1+T4*2*(Wk/MU)))
by A131,A103,A129,A128
.= (((U+1) |^W) / (U|^Wk)) *(1+T7* ((5*k)/M)) by A124,A125,A127;
then
A133: r/(S*T*U) = ( (((U+1) |^W) / (U|^Wk)) *(1+T7* ((5*k)/M))) * (1/U)
by XCMPLX_1:103
.= (((U+1) |^W) / (U|^Wk))* (1/U) *(1+T7* ((5*k)/M))
.= ((U+1) |^W) / ((U|^Wk)*U) *(1+T7* ((5*k)/M)) by XCMPLX_1:103
.= ((U+1) |^W) / (U|^(Wk+1)) *(1+T7* ((5*k)/M)) by NEWTON:6;
set IW = (U,1) In_Power W, IWk=IW|k;
A134: len IW = W+1 by NEWTON:def 4;
A135: k < W+1 by A66,NAT_1:13;
then
A136:len IWk = k by A134,FINSEQ_1:59;
consider IWW be FinSequence such that
A137: IW = IWk^IWW by FINSEQ_1:80;
reconsider IWW as FinSequence of REAL by A137,FINSEQ_1:36;
reconsider k1=k-1 as Nat by A1;
A138: len (IWk^IWW) = k+ len IWW by A136,FINSEQ_1:22;
then
A139: len IWW = Wk+1 by A134,A137;
A140: len IWk = k1-0+1 by A135,A134,FINSEQ_1:59;
A141: for i be Nat st i+1 in dom IWk holds IWk.(i+1) =
(W choose (0+i)) * (U |^(W-'(0+i)))
proof
let i be Nat such that
A142: i+1 in dom IWk;
A143: i+1 in dom IW by A142,RELAT_1:57;
i+1 <= k by A142,FINSEQ_3:25,A136;
then i+1 <= W by A66,XXREAL_0:2;
then i < W by NAT_1:13;
then
A144: W-'i = W -i by XREAL_1:233;
A145: i+1-1=i;
IWk.(i+1) = IW.(i+1) by A142,FUNCT_1:47
.= (W choose i) * U|^(W-'i) * 1|^i by A143,A145,A144,NEWTON:def 4;
hence thesis;
end;
A146: W|^0=1 & W-'0=W-0 by XREAL_1:233,NEWTON:4;
k1 <k1+1 by NAT_1:13;
then k1 < W by A66,XXREAL_0:2;
then
A147: 0 < Sum IWk < 2*(W|^0) * (U|^(W-'0)) by Th14,A89,A140,A141;
set UIWk = (1/ (U|^(Wk+1)))* IWk;
A148: 1 / U * U = 1 by A7,A6,XCMPLX_1:87;
U|^(Wk+1) = (U|^Wk)* U by NEWTON:6;
then 1/ (U|^(Wk+1)) = (1/ U) * (1/(U|^Wk)) by XCMPLX_1:102;
then
A149: (1/ (U|^(Wk+1)))* (U |^Wk) = (1/ U) * ((1/(U|^Wk)) * (U |^Wk))
.= (1/ U)*1 by XCMPLX_1:87,A7;
rng UIWk c= NAT
proof
let y be object such that
A150:y in rng UIWk;
consider i be object such that
A151: i in dom UIWk & UIWk.i = y by A150,FUNCT_1:def 3;
reconsider i as Nat by A151;
A152: dom UIWk = dom IWk by VALUED_1:def 5;
then
A153: 1<= i <= k by A151, FINSEQ_3:25,A136;
then reconsider i1 = i-1 as Nat;
i=i1+1;
then i1 <k by A153,NAT_1:13;
then
A154: k-'i1 = k-i1 & W-'i1 = W-i1 & k-'i = k-i
by A66,XXREAL_0:2,A153,XREAL_1:233;
then
A155: W-'i1 = Wk + (k-'i1);
k-'i1 = (k-'i)+1 by A154;
then
A156: (U|^ (k-'i1)) * (1/U) = ((U|^ (k-'i))*U) * (1/U) by NEWTON:6
.=(U|^ (k-'i))*(U * (1/U))
.= U|^ (k-'i) by A148;
IWk.(i1+1) = (W choose (0+i1)) * (U |^(W-'(0+i1))) by A152,A151,A141;
then UIWk.i = (1/(U|^(Wk+1)))*((W choose i1)*(U |^(W-'i1))) by VALUED_1:6
.= (1/ (U|^(Wk+1)))* ((W choose i1) * ((U|^Wk) * (U|^ (k-'i1))))
by A155,NEWTON:8
.= (W choose i1)*(U|^ (k-'i)) by A156,A149;
hence thesis by A151;
end;
then reconsider UIWk as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Z=Sum UIWk as Element of NAT by ORDINAL1:def 12;
A157: (1/ (U|^(Wk+1)))* (2* (U |^Wk) * (U |^k)) =
2*((1/ U) * (U |^(k1+1))) by A149
.= 2*((1/ U) * ((U |^k1) * U)) by NEWTON:6
.= 2* (1 / U * U) * (U |^k1)
.= 2*1 *(U|^k1) by A6,A7,XCMPLX_1:87;
A158: Z = (1/ (U|^(Wk+1)))* Sum IWk < (1/(U|^(Wk+1)))* (2*(U |^Wk)*(U |^k))
by A7,A110, XREAL_1:68,A147,A146,RVSUM_1:87;
A159: for i be Nat st i+1 in dom IWW holds IWW.(i+1) =
(W choose (k+i)) * (U |^(W-'(k+i)))
proof
let i be Nat such that
A160: i+1 in dom IWW;
A161: k+(i+1) in dom IW by A160,A136,A137,FINSEQ_1:28;
then k+i+1 <= W+1 by A134,FINSEQ_3:25;
then
A162: W-'(k+i) = W-(k+i) by XREAL_1:6,233;
A163: k+(i+1)-1 = k+i;
IWW.(i+1) = IW.(k+(i+1)) by FINSEQ_1:def 7,A136,A137,A160
.= (W choose (k+i)) * U|^(W-'(k+i)) * 1|^(k+i)
by A161,A163,A162,NEWTON:def 4;
hence thesis;
end;
A164: 0 < Sum IWW < 2*(W|^k) * (U|^(W-'k)) by A139,Th14,A89,A66,A1,A159;
set UIWW = (1/ (U|^(Wk+1)))* IWW;
set D = Sum UIWW;
A165: W-'k = Wk by A65,XXREAL_0:2,XREAL_1:233;
A166: D = (1/ (U|^(Wk+1)))* Sum IWW < (1/ (U|^(Wk+1)))* (2*(W|^k) * (U|^Wk))
by A7,A165, XREAL_1:68,A164,RVSUM_1:87;
(U+1) |^W = Sum IW = Sum IWk + Sum IWW by A137,RVSUM_1:75,NEWTON:30;
then
A167: Z+D = (1/ (U|^(Wk+1))) * ((U+1) |^W) by A166,A158
.= ((U+1) |^W) / (U|^(Wk+1)) by XCMPLX_1:99;
A168: |.D.| = D by A166,A164,ABSVALUE:def 1;
A169: |.T7.| <=1 & |.(5*k)/M.| <=1 by Th1,A74,XREAL_1:183;
|.D*T7* ((5*k)/M) .| = |.D*T7 .|*|. ((5*k)/M) .| by COMPLEX1:65
.= |.D.| * |. T7 .|*|. ((5*k)/M) .| by COMPLEX1:65
.= (|. ((5*k)/M) .|*|. T7 .|) * D by A168;
then |.D*T7* ((5*k)/M) .| <= 1*D by A166,A164,A169,XREAL_1:160,XREAL_1:64;
then
A170: |.D.|+ |.D*T7* ((5*k)/M) .| <= D+1*D by A168,XREAL_1:6;
|. T7* (Z* ((5*k)/M)) .| = |. T7.|* |.Z* ((5*k)/M) .| by COMPLEX1:65;
then
A171: |. T7* (Z* ((5*k)/M)) .| <= 1 * |.Z* ((5*k)/M) .| by Th1,XREAL_1:64;
D*(1+T7* ((5*k)/M)) = D+ D*T7* ((5*k)/M);
then |.D*(1+T7* ((5*k)/M)).| <= |.D.|+ |.D*T7* ((5*k)/M) .| by COMPLEX1:56;
then |.D*(1+T7* ((5*k)/M)).| <= D+D by A170,XXREAL_0:2;
then
A172: |.D*(1+T7* ((5*k)/M)).| + |.Z* T7* ((5*k)/M).| <= D+D +Z* ((5*k)/M)
by A171,XREAL_1:7;
|. D*(1+T7* ((5*k)/M)) + Z* T7* ((5*k)/M).| <=
|.D*(1+T7* ((5*k)/M)).| + |.Z* T7* ((5*k)/M).| by COMPLEX1:56;
then
A173: |.D*(1+T7* ((5*k)/M)) + Z* T7* ((5*k)/M).| <= D+D +Z* ((5*k)/M)
by A172,XXREAL_0:2;
A174: 2*(2* (1/ U)* u ) = (4*u)*(1/U)
.= (4*u*1)/U by XCMPLX_1:74;
2*D < 2*(2* (1/ U)* u ) by A166,A149,A117,XREAL_1:68;
then
A175: 2*D < 1/4 by A174,A92,XXREAL_0:2;
A176: U|^(k1+1) = U|^k1 * U by NEWTON:6;
1/2 < 1<=m by A1,NAT_1:14;
then 1/2 <= m by XXREAL_0:2;
then
A177: 1/2 + m <= m+m by XREAL_1:6;
A178: r/(S*T*U) < 1/2 + (m/1) by A119,XREAL_1:19;
then
A179: r/(S*T*U) <= 2*m by A177,XXREAL_0:2;
A180: (1/2 * (U |^k))*(1/U) * (50*U) = 25* (U |^k) * (U *(1/U))
.= 25* (U |^k)*1 by XCMPLX_1:87,A7,A6;
r/(S*T*U) = r/(S*T) *(1/U) by XCMPLX_1:103;
then r/(S*T*U) >= (1/2 * (U |^k))*(1/U) by A111,XREAL_1:64;
then 2*m >= (1/2 * (U |^k))*(1/U) by A179,XXREAL_0:2;
then 2*m*(50*U) >= 25* (U |^k) by XREAL_1:64,A180;
then M> 100*m*U*W >= 25* (U |^k) *W by XREAL_1:64,NAT_1:13,A8;
then M> 25* ((U |^k) *W) >= 24* ((U |^k) *W) by XXREAL_0:2,XREAL_1:64;
then
A181: M> 24* ((U |^k) *W) by XXREAL_0:2;
(10*f*k) * (10*(k+1)) >= 10*f*k*1 by NAT_1:14,XREAL_1:64;
then
A182: 24* (U |^k) *W >= 24* (U |^k)*(10*f*k ) by A6,XREAL_1:64;
then
A183: 240 * f * k * U|^k < M by A181,XXREAL_0:2;
(f*k)*k <= (f*k)*(k+1) by XREAL_1:64,NAT_1:11;
then (f*k)*k*96 <= (f*k)*(k+1)*100 by XREAL_1:66;
then
A184: 96*f*(k*k) <= W & k^2=k*k by A6,SQUARE_1:def 1;
then 12* (8*f*k^2) <= 1*W;
then
A185: (8*f*k^2)/W <=1/12 by XREAL_1:102,A1,A6;
1<=f by A1,NAT_1:14;
then 24*1 <= 96*f by XREAL_1:66;
then
A186: 24*1 *k^2 <= 96*f *k^2 by XREAL_1:64;
then
A187: 24*1 *k^2 <= W by A184,XXREAL_0:2;
A188:1*k^2 <= 24*k^2 by XREAL_1:64;
2*k^2 <= 24*k^2 by XREAL_1:64;
then 2* k^2 <= W*1 by A187,XXREAL_0:2;
then
A189: k^2/W <=1/2 by XREAL_1:102,A1,A6;
6*(4*k^2) <= 1*W by A186,A184,XXREAL_0:2;
then (4*k^2)/W <=1/6 by XREAL_1:102,A1,A6;
then
A190: (4*(k^2/W)) <=1/6 by XCMPLX_1:74;
k * U|^k *1 <= k * U|^k * f by A1,NAT_1:14,XREAL_1:64;
then k * U|^k *1 *120 <= k * U|^k * f * 240 by XREAL_1:66;
then 12*(((U|^k) * 10 *k)) <= 1*M by A183,XXREAL_0:2;
then
A191: (((U|^k) * 10 *k))/M <=1/12 by XREAL_1:102;
A192: 1*(u|^3*W|^3)<= 100*(u|^3*W|^3) by XREAL_1:64;
W*W*1 <= W|^3 by A60,A1,A6,NAT_1:14,XREAL_1:64;
then W*W * u <= W|^3 * (u|^3) < U by A69,XREAL_1:66,A7,NAT_1:13,A192;
then W*(W * W|^k) <= U by XXREAL_0:2,A117;
then
A193: W*( W|^(k+1)) <= U by NEWTON:6;
1<= k*(k+1) by A1,NAT_1:14;
then 96*1<= k*(k+1)*100 by XREAL_1:66;
then 96*1*f <= k*(k+1)*100*f by XREAL_1:64;
then 96*f *( W|^(k+1)) <= W*( W|^(k+1)) by A6,XREAL_1:64;
then 12* (8*f*W|^(k+1)) <=1 *U by A193,XXREAL_0:2;
then
A194: (8*f*W|^(k+1))/ U<=1/12 by XREAL_1:102,A7;
1<= f*k*(k+1) by A1,NAT_1:14;
then 1*24 <= 100*(f*k*(k+1)) by XREAL_1:66;
then 24*( W|^(k+1)) <= W*( W|^(k+1)) by A6,XREAL_1:64;
then 12*(2* W|^(k+1)) <= U*1 by A193,XXREAL_0:2;
then (2* W|^(k+1)) /U <=1/12 by XREAL_1:102,A7;
then 2* (W|^(k+1) /U) <=1/12 by XCMPLX_1:74;
then
A195: 2*((W|^(k+1)) * (1/U)) <= 1/12 by XCMPLX_1:99;
A196: 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M <= 1/12+1/12 = 1/6 <=1/2
by A195,A191,XREAL_1:7;
then
A197: 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M <= 1/2 by XXREAL_0:2;
A198: 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) <= 2*(1/6)<=1
by A196,XREAL_1:64;
then
A199: 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) + 2* (2*(k^2/W))
<= 2*1/6+ 1/6 by A190,XREAL_1:7;
A200: 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) <=1 by A198,XXREAL_0:2;
(6*f*U)* (40*k*(U|^k1)) >= 1*(40*k*(U|^k1))
by XREAL_1:64,NAT_1:14,A1,A20,A7;
then
A201: 2*(U|^k1)*(20*k) <=M by A176,A183,XXREAL_0:2;
Z*(20*k) <= 2*(U|^k1)*(20*k) by A158,A157,XREAL_1:64;
then 4*(Z*(5*k)) <= 1*M by A201,XXREAL_0:2;
then (Z*(5*k))/M <=1/4 by XREAL_1:102;
then Z* ((5*k)/M) <=1/4 by XCMPLX_1:74;
then 2*D + Z* ((5*k)/M) < 1/4+1/4 =1/2 by A175,XREAL_1:8;
then |.D*(1+T7* ((5*k)/M)) + Z* T7* ((5*k)/M).| <1/2 by A173,XXREAL_0:2;
then
A202: -(1/2) <= D*(1+T7* ((5*k)/M)) + Z* T7* ((5*k)/M) <= 1/2
by ABSVALUE:5;
m-Z > r/(S*T*U) -(1/2) - Z by XREAL_1:9,A178,XREAL_1:19;
then m-Z> D*(1+T7* ((5*k)/M)) + Z* T7* ((5*k)/M) - (1/2) >= -(1/2)-(1/2)
by A167,A133,A202,XREAL_1:9;
then m-Z> -1 by XXREAL_0:2;
then
A203: m-Z>= -1+1 by INT_1:7;
m-Z < r/(S*T*U)-Z by XREAL_1:9,XREAL_1:47,A118,A22,A15,A10,A7,A8,A9;
then m-Z <= 1/2 by A202,XXREAL_0:2,A167,A133;
then m-Z < 1+0 by XXREAL_0:2;
then
A204: m-Z=0 by A203,INT_1:7;
A205: (U+1)/U = U/U +1/U by XCMPLX_1:62
.= 1+I*(1/U) by XCMPLX_1:60,A6,A7;
1/U <= 1/(2*W) by A80,XREAL_1:118,A1,A6;
then consider T8 be _Theta such that
A206: (1+I*(1/U))|^W = 1+ T8*2*W* (1/U) by Th9;
A207: ((U+1) |^W) / (U|^Wk) = (U|^k) * (((U+1) |^W) / ((U|^Wk) * (U|^k)))
by A7,XCMPLX_1:92
.= (U|^k) * (((U+1) |^W) / ((U|^ (Wk+k)))) by NEWTON:8
.= (U|^k) * (1+ T8*2*W* (1/U)) by A206,A205,PREPOWER:8;
A208:|. 2 .| = 2;
A209: (2*W)/U <=1 by XREAL_1:183,A80;
then
A210: -((2*W)/U) >= -1 by XREAL_1:24;
-1<= T8<=1 by Def1;
then (-1)*((2*W)/U)<= T8*((2*W)/U)<=1 *((2*W)/U) by XREAL_1:64;
then -1 <= T8*((2*W)/U)<= 1 by A209,A210,XXREAL_0:2;
then
A211: -1+1 <= T8*((2*W)/U)+1<= 1+1 by XREAL_1:6;
A212:(2*W)* (1/U) = (2*W)/U by XCMPLX_1:99;
then |.(1+ T8*2*W* (1/U)).| = (1+ T8*2*W* (1/U)) by A211,ABSVALUE:def 1;
then consider T9 be _Theta such that
A213: T7* (1+ T8*2*W* (1/U)) = T9*2 by Th2,A208,A211,A212;
A214: (U|^k) * (1+ T8*2*W* (1/U)) * (T7* ((5*k)/M)) =
(U|^k) * ((1+ T8*2*W* (1/U)) * T7)* ((5*k)/M)
.= (U|^k) * (2*T9)* ((5*k)/M) by A213
.= T9 * ( ((U|^k) * 2) * ((5*k)/M))
.= T9 * ((((U|^k) * 2) * (5*k))/M) by XCMPLX_1:74;
A215: (1/ (U|^(Wk+1))) * U = (1/ (U* U|^Wk)) * U by NEWTON:6
.= 1/ (U|^Wk) by XCMPLX_1:92,A7;
A216: D*U = U*((1/ (U|^(Wk+1)))* Sum IWW) by RVSUM_1:87;
IWW<>{} by A139;
then consider iww be FinSequence of REAL,x be Element of REAL such that
A217: IWW = <*x*>^iww by FINSEQ_2:130;
1<= Wk+1 by NAT_1:11;
then
A218: (W choose (k+0)) * (U |^(W-'(k+0))) = IWW.(0+1)
by A159,A138,A134,A137,FINSEQ_3:25
.= x by A217;
reconsider Wk1=Wk-1 as Nat by A14;
A219: len <*x*> = 1 by FINSEQ_1:40;
then Wk+1 = 1 +len iww by A217,A138,A134,A137,FINSEQ_1:22;
then
A220: len iww = W-(k+1)+1;
for i be Nat st i+1 in dom iww holds iww.(i+1) =
(W choose ((k+1)+i)) * (U |^(W-'((k+1)+i)))
proof
let i be Nat such that
A221: i+1 in dom iww;
iww.(i+1) = IWW.(1+(i+1)) by A217,A219,A221,FINSEQ_1:def 7
.= (W choose (k+(i+1))) * (U |^(W-'(k+(i+1))))
by A159,FINSEQ_1:28,A221,A217,A219;
hence thesis;
end;
then
A222: 0 < Sum iww < 2*(W|^(k+1)) * (U|^(W-'(k+1))) by Th14,A12,A6,A89,A220;
A223: (1/ (U|^Wk)) *x = (1/ (U|^Wk)) * (U |^Wk) * (W choose k) by A218,A165
.=1 * (W choose k) by A7, XCMPLX_1:87;
Sum IWW = x+ Sum iww by A217,RVSUM_1:76;
then
A224: D*U = (W choose k) + (1/ (U|^Wk))*Sum iww by A216,A215,A223;
A225: W-'(k+1) = W-(k+1) = Wk1 by A6,A12,XREAL_1:233;
Wk = Wk1+1;
then
A226:(1/ (U|^Wk)) * (U|^(W-'(k+1))) = 1/(U * U|^Wk1) * (U|^Wk1)
by A225,NEWTON:6
.= 1/U by XCMPLX_1:92,A7;
(1/ (U|^Wk))*Sum iww < (1/ (U|^Wk))* (2*(W|^(k+1)) * (U|^(W-'(k+1))))
by A222, XREAL_1:68,A7;
then consider T10 be _Theta such that
A227: I*((1/ (U|^Wk))*Sum iww) = T10*(2*(W|^(k+1))*(1/U))by A226,A222,Th5;
A228: (Wk+k) choose k >= Wk+1 > Wk by NAT_1:14,A1,NAT_1:13,RAMSEY_1:11;
then W choose k >=1 by NAT_1:14;
then reconsider T12 = 1/ (W choose k) as _Theta by Def1,XREAL_1:183;
A229: (W choose k) * T12 = 1 by XCMPLX_1:87,A228;
consider T11 be _Theta such that
A230: T10* (2*(W|^(k+1)) * (1/U)) + T9 * ((((U|^k) * 10 *k))/M) =
T11* ( 2*(W|^(k+1))* (1/U) + (((U|^k) * 10 *k))/M) by Th6;
(Z+D)*U = ((U+1) |^W) / (U|^Wk*U) * U by A167,NEWTON:6
.= ((U+1) |^W) / (U|^Wk) by XCMPLX_1:92,A7;
then
A231: r/(S*T) - m*U = D*U + (((U+1) |^W)/(U|^Wk))*(T7*((5*k)/M)) by A204,A132
.= (W choose k) + T10* (2*(W|^(k+1)) * (1/U)) + T9 * ((((U|^k) * 10 *k))/M)
by A214,A207,A227,A224
.= (W choose k) + T11* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) by A230
.= (W choose k) + (W choose k) * T12 * T11*
( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) by A229
.= (W choose k) *(1+ (T12*T11)*
( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M));
consider T131 be _Theta such that
A232: W choose k = W|^k/(k!)*(1+T131*(k^2/W)) by A188,A187,XXREAL_0:2,Th8;
consider T13 be _Theta such that
A233: 1 / (1+T131*(k^2/W)) = 1+T13*2*(k^2/W) by Th7,A189;
A234: 1 / (W|^k / (k!) * (1+T131*(k^2/W))) =
(1 / (W|^k / (k!))) * ( 1/ (1+T131*(k^2/W))) by XCMPLX_1:102
.= (k! / (W|^k)) * ( 1/ (1+T131*(k^2/W))) by XCMPLX_1:57;
consider T14 be _Theta such that
A235: 1 / (1+(T12*T11)* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)) =
1+T14*2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) by Th7,A197;
A236: k! / (W|^k) * W|^k = k! by XCMPLX_1:87,A1,A6;
consider T15 be _Theta such that
A237: ( 1+T14* (2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)) ) *
( 1+T13*(2*(k^2/W))) = 1 + T15 * ( 2* ( 2*(W|^(k+1)) * (1/U) +
(((U|^k) * 10 *k))/M) + 2* (2*(k^2/W)) ) by A200,Th3;
T15 >= - 1 by Def1;
then T15*(2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+ 2* (2*(k^2/W)))
>= (-1)*(2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+
2* (2*(k^2/W)))
& (-1)*(2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+
2* (2*(k^2/W))) >= (-1) * (1/2) by A199,XREAL_1:64,65;
then T15*(2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+ 2* (2*(k^2/W)))
>= -(1/2) by XXREAL_0:2;
then 1 + T15*(2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+
2* (2*(k^2/W))) >= 1+-(1/2)=1/2 by XREAL_1:6;
then
A238: k! * (1 + T15*(2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+
2* (2*(k^2/W)))) >= k!*(1/2) by XREAL_1:64;
A239: 1 * (u / (r/(S*T) - m*U)) = (1 / (r/(S*T) - m*U)) * 1 *u
by XCMPLX_1:101
.= (k! / (W|^k)) * ( 1/ (1+T131*(k^2/W))) *
( 1+T14*2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) )*(W|^k)
by A117,A232,A234,A235,A231, XCMPLX_1:102
.= k! * (( 1+T13*(2*(k^2/W))) * ( 1+T14*(2* ( 2*(W|^(k+1)) * (1/U) +
(((U|^k) * 10 *k))/M)) )) by A236,A233
.= k! * (1 + T15 * ( 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) +
2* (2*(k^2/W)))) by A237;
then
A240: (u / (r/(S*T) - m*U))-f >= k!*(1/2)-f by A238,XREAL_1:9;
(1/2)^2 = (1/2)*(1/2) by SQUARE_1:def 1;
then ((u/(r/(S*T)-m*U)) -f)^2< (1/2) ^2 by A25,SQUARE_1:def 1;
then
A241: -(1/2) < (u/(r/(S*T)-m*U)) -f <1/2 by SQUARE_1: 48;
then k!*(1/2)-f < 1/2 by A240,XXREAL_0:2;
then (k!*(1/2)-f)*2 < 1/2*2=1 by XREAL_1:68;
then k!-f*2=k!*(1/2)*2-f*2 < 1/2*2=1+0;
then k!-f*2 <=0 by INT_1:7;
then k! -f*2+2*f<= 0+2*f by XREAL_1:6;
then reconsider T16= k!/(2*f) as _Theta by Def1,XREAL_1:183;
A242: (2*f) * ( 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) +
2* (2*(k^2/W)))
= (8*f*W|^(k+1)) * (1/U) + (4*f* (((U|^k) * 10 *k)/M)) +
(2*f)*(2* (2*(k^2/W)))
.= (8*f*W|^(k+1))/ U + (4*f* (((U|^k) * 10 *k)/M)) + (8*f*(k^2/W))
by XCMPLX_1:99
.= (8*f*W|^(k+1))/ U + ( ( 4*f)* ((U|^k) * 10 *k))/M + (8*f*(k^2/W))
by XCMPLX_1:74
.= (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M + (8*f*k^2)/W by XCMPLX_1:74;
k! = T16*(2*f) by XCMPLX_1:87,A1;
then
A243:u / (r/(S*T) - m*U) =
k!+ (T15* T16)*((2*f) * ( 2* ( 2*(W|^(k+1)) * (1/U) +
(((U|^k) * 10 *k))/M) + 2* (2*(k^2/W)))) by A239
.= k!+ (T15* T16)*((8*f*W|^(k+1))/U+(40*f *(U|^k)*k)/M+(8*f*k^2)/W)by A242;
6*( 40*f *(U|^k)*k) < 1*M by A182,A181,XXREAL_0:2;
then
A244: ( 40*f *(U|^k)*k)/M < 1/6 by XREAL_1:106;
(8*f*W|^(k+1))/ U + (8*f*k^2)/W <= (1/12) +(1/12) by A185,A194,XREAL_1:7;
then
A245: (8*f*W|^(k+1))/ U + (8*f*k^2)/W + (40*f *(U|^k)*k)/M <
(1/12) +(1/12)+(1/6) by A244,XREAL_1:8;
-1 <= (T15* T16)<=1 by Def1;
then (1/3) *(-1) < (-1) * ( (8*f*W|^(k+1))/ U +
( 40*f *(U|^k)*k)/M + (8*f*k^2)/W ) <=
(T15* T16)*( (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M + (8*f*k^2)/W )
<= 1 *( (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M + (8*f*k^2)/W ) < 1/3
by A245,XREAL_1:64,69;
then (1/3) *(-1) < (T15* T16)*( (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M
+ (8*f*k^2)/W ) < 1/3 by XXREAL_0:2;
then -1/3 +k! < u / (r/(S*T) - m*U) < 1/3 +k! by A243,XREAL_1:6;
then (-1/3 +k!) -(1/2) < (u/(r/(S*T) - m*U)) - ((u/(r/(S*T)-m*U)) -f) <
(1/3 +k!) - (- (1/2)) by A241,XREAL_1:15;
then -5/6 +k!-k! < f- k! < k!+5/6-k! by XREAL_1:9;
then -1+0 < f- k! < 1+0 by XXREAL_0:2;
then -1+1 <= f- k! <= 0 by INT_1:7;
then f-k!=0;
hence thesis;
end;
theorem Th16:
for f,k be Nat st f = k! & k > 0 holds
ex m,r,s,t,u be Nat,W,U,S,T,Q be Nat, M be non trivial Nat st
m>0 & u>0 &
r + W + 1 = Py(M*(U+1),W+1) &
(M^2-1)*S^2 +1 is square &
((M*U)^2 -1)*T^2 + 1 is square &
W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
W = 100*f*k*(k+1) &
U = 100 * (u|^3)*(W|^3)+1 &
M = 100 * m * U *W+1 &
S = (M-1)*s+k+1 &
T = (M*U-1)*t +W-k+1 &
Q = 2*M*W-W^2 -1
proof
let f,k be Nat such that
A1: f = k! & k > 0;
set W = 100*f*k*(k+1),u = W|^k,U = 100 * (u|^3)*(W|^3)+1;
set IW = (U,1) In_Power W, IWk=IW|k;
A2: len IW = W+1 by NEWTON:def 4;
(f*k*100)*(k+1) >= (f*k*100)*1 & f >=1 by XREAL_1:64,A1,NAT_1:14;
then W >= f*(100*k) >= 1*(100*k) by XREAL_1:64;
then
A3: W>= 100*k>=5*k & 100*k>=1*k & 100*k>=3*k by XXREAL_0:2,XREAL_1:64;
then
A4: W>= 5*k & W>= k & W>= 3*k by XXREAL_0:2;
A5: k <= W by A3,XXREAL_0:2;
k>=1 by A1,NAT_1:14;
then 1+0 < k+k by XREAL_1:8;
then
A6: 1+0 +k < k+k+k by XREAL_1:6;
then
A7: k +1 < W by A4,XXREAL_0:2;
W|^(1+1) = W* W|^1 & W|^1=W by NEWTON:6;
then
A8: W|^(2+1) = W*W*W by NEWTON:6;
u|^(1+1) = u* u|^1 & u|^1=u by NEWTON:6;
then
A9: u|^(2+1) = u*u*u by NEWTON:6;
u|^(2+1) >= u*1 & W|^3 >=1 & u|^3 >= 1 & W|^3 >=W*1
by A1,NAT_1:14,A8,A9,XREAL_1:64;
then u|^3 * W|^3 >= 1*u & u|^3 * W|^3 >= 1*W by XREAL_1:66;
then
A10: u|^3 * W|^3 *100 >= (1*u)*12 & u|^3 * W|^3 *100 >= (1*W)*2 by XREAL_1:66;
A11: 2*W <= U by A10,NAT_1:13;
reconsider Wk=W-k as Nat by A3,XXREAL_0:2,NAT_1:21;
A12: k < W+1 by A5,NAT_1:13;
then A13:len IWk = k by A2,FINSEQ_1:59;
consider IWW be FinSequence such that
A14: IW = IWk^IWW by FINSEQ_1:80;
reconsider IWW as FinSequence of REAL by A14,FINSEQ_1:36;
reconsider k1=k-1 as Nat by A1;
A15: len (IWk^IWW) = k+ len IWW by A13,FINSEQ_1:22;
then
A16: len IWW = Wk+1 by A2,A14;
A17: len IWk = k1-0+1 by A12,A2,FINSEQ_1:59;
A18: for i be Nat st i+1 in dom IWk holds IWk.(i+1) =
(W choose (0+i)) * (U |^(W-'(0+i)))
proof
let i be Nat such that
A19: i+1 in dom IWk;
A20: i+1 in dom IW by A19,RELAT_1:57;
i+1 <= k by A19,FINSEQ_3:25,A13;
then i+1 <= W by A5,XXREAL_0:2;
then i < W by NAT_1:13;
then
A21: W-'i = W -i by XREAL_1:233;
A22: i+1-1=i;
IWk.(i+1) = IW.(i+1) by A19,FUNCT_1:47
.= (W choose i) * U|^(W-'i) * 1|^i by A20,A22,A21,NEWTON:def 4;
hence thesis;
end;
A23: W|^0=1 & W-'0=W-0 by XREAL_1:233,NEWTON:4;
k1 <k1+1 by NAT_1:13;
then k1 < W by A5,XXREAL_0:2;
then
A24: 0 < Sum IWk < 2*(W|^0) * (U|^(W-'0)) by Th14,A11,A17,A18;
set UIWk = (1/ (U|^(Wk+1)))* IWk;
A25: 1 / U * U = 1 by XCMPLX_1:87;
U|^(Wk+1) = (U|^Wk)* U by NEWTON:6;
then 1/ (U|^(Wk+1)) = (1/ U) * (1/(U|^Wk)) by XCMPLX_1:102;
then
A26: (1/ (U|^(Wk+1)))* (U |^Wk) = (1/ U) * ((1/(U|^Wk)) * (U |^Wk))
.= (1/ U)*1 by XCMPLX_1:87;
rng UIWk c= NAT
proof
let y be object such that
A27: y in rng UIWk;
consider i be object such that
A28: i in dom UIWk & UIWk.i = y by A27,FUNCT_1:def 3;
reconsider i as Nat by A28;
A29: dom UIWk = dom IWk by VALUED_1:def 5;
then
A30: 1<= i <= k by A28, FINSEQ_3:25,A13;
then reconsider i1 = i-1 as Nat;
i=i1+1;
then i1 <k by A30,NAT_1:13;
then
A31: k-'i1 = k-i1 & W-'i1 = W-i1 & k-'i = k-i
by A5,XXREAL_0:2,A30,XREAL_1:233;
then
A32: W-'i1 = Wk + (k-'i1);
k-'i1 = (k-'i)+1 by A31;
then
A33: (U|^ (k-'i1)) * (1/U) = ((U|^ (k-'i))*U) * (1/U) by NEWTON:6
.=(U|^ (k-'i))*(U * (1/U))
.= U|^ (k-'i) by A25;
IWk.(i1+1) = (W choose (0+i1)) * (U |^(W-'(0+i1))) by A29,A28,A18;
then UIWk.i = (1/(U|^(Wk+1)))*((W choose i1)*(U|^(W-'i1))) by VALUED_1:6
.= (1/ (U|^(Wk+1)))* ((W choose i1) * ((U|^Wk) * (U|^ (k-'i1))))
by A32,NEWTON:8
.= (W choose i1)*(U|^ (k-'i)) by A33,A26;
hence thesis by A28;
end;
then reconsider UIWk as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Z=Sum UIWk as Element of NAT by ORDINAL1:def 12;
A34: U |^(Wk+k)= (U |^Wk) * (U |^k) by NEWTON:8;
A35: Z = (1/ (U|^(Wk+1)))* Sum IWk < (1/ (U|^(Wk+1)))* (2* (U |^Wk) * (U |^k))
by A34, XREAL_1:68,A24,A23,RVSUM_1:87;
set m=Z,M = 100 * m * U *W+1;
set mu = M*(U+1);
reconsider M as non trivial Nat by A35,A24,A1;
reconsider MU=M*U as non trivial Nat;
set S = Py(M,k+1);
set T = Py(MU,Wk+1);
reconsider r = Py(mu,W+1) - (W+1) as Nat by NAT_1:21,HILB10_1:13;
consider s be Integer such that
A36: (M-1)*s = S -(k+1) by INT_1:def 5,HILB10_1:24;
S -(k+1) >=k+1 -(k+1) by XREAL_1:9,HILB10_1:13;
then s >=0 by A36;
then reconsider s as Element of NAT by INT_1:3;
consider t be Integer such that
A37: (MU-1)*t = T -(Wk+1) by INT_1:def 5,HILB10_1:24;
T -(Wk+1) >=Wk+1 -(Wk+1) by XREAL_1:9,HILB10_1:13;
then t >=0 by A37;
then reconsider t as Element of NAT by INT_1:3;
A38: (MU-1)*t + Wk+1 = T by A37;
set Q = 2*M*W-W^2 -1;
A39: M*W -1 >= 0 by A1;
100 * m * U * W >= 1*W by XREAL_1:64,A35,A24,NAT_1:14;
then M> 1*W by NAT_1:13;
then M*W >= W*W = W^2 by XREAL_1:64,SQUARE_1:def 1;
then M*W+M*W >= M*W+W^2 by XREAL_1:7;
then M*W+M*W -(W^2+1) >= M*W+W^2 -(W^2+1) by XREAL_1:9;
then reconsider Q as Element of NAT by A39,INT_1:3;
M^2=M*M by SQUARE_1:def 1;
then
A40: M^2-'1 = M^2-1 by NAT_1:14,XREAL_1:233;
A41: Px(M,k+1)^2 - (M^2-1) *S^2 = 1 by A40,HILB10_1:7;
MU^2=MU*MU by SQUARE_1:def 1;
then
A42: MU^2-'1 = MU^2-1 by XREAL_1:233,NAT_1:14;
Px(MU,Wk+1)^2 - (MU^2-1) *T^2 = 1 by A42,HILB10_1:7;
then
A43: (MU^2 -1)*T^2 + 1 is square;
A44: for i be Nat st i+1 in dom IWW holds IWW.(i+1) =
(W choose (k+i)) * (U |^(W-'(k+i)))
proof
let i be Nat such that
A45: i+1 in dom IWW;
A46: k+(i+1) in dom IW by A45,A13,A14,FINSEQ_1:28;
then k+i+1 <= W+1 by A2,FINSEQ_3:25;
then
A47: W-'(k+i) = W-(k+i) by XREAL_1:6,233;
A48: k+(i+1)-1 = k+i;
IWW.(i+1) = IW.(k+(i+1)) by FINSEQ_1:def 7,A13,A14,A45
.= (W choose (k+i)) * U|^(W-'(k+i)) * 1|^(k+i) by A46,A48,A47,NEWTON:def 4;
hence thesis;
end;
A49: 0 < Sum IWW < 2*(W|^k) * (U|^(W-'k)) by A16,Th14,A11,A5,A1,A44;
set UIWW = (1/ (U|^(Wk+1)))* IWW;
set D = Sum UIWW;
A50: W-'k = Wk by A3,XXREAL_0:2,XREAL_1:233;
A51: U>=1 by NAT_1:14;
100 * m * U *W>= 1*W by A35,A24,NAT_1:14,XREAL_1:64;
then W+1 <= M-1+1 by XREAL_1:6;
then
A52: (W+1)*1 <= M*U by A51,XREAL_1:66;
U < U+1 by NAT_1:13;
then M*U <=M*(U+1) by XREAL_1:64;
then W+1 <= M*(U+1) by A52,XXREAL_0:2;
then W < M*(U+1) by NAT_1:13;
then consider t1 be _Theta such that
A53: Py(mu,W+1) = (2*mu) |^W *(1+t1*(W/mu)) by Th10;
reconsider I=1 as _Theta by Def1;
set E=t1*(W/mu)- ( W+1) / (2*mu) |^W;
W|^(1+1) = W* W|^1 & W|^1=W by NEWTON:6;
then
A54: W|^(2+1) = W*W*W by NEWTON:6;
A55: W>=1 by A1,NAT_1:14;
A56:2*mu >=1 by NAT_1:14;
(f*k*100)*(k+1) >= (f*k*100)*1 & f >=1 by XREAL_1:64,A1,NAT_1:14;
then W >= f*(100*k) >= 1*(100*k) by XREAL_1:64;
then W>= 100*k>=5*k & 100*k>=1*k by XXREAL_0:2,XREAL_1:64;
then
A57: k <= W by XXREAL_0:2;
u>=1 by NAT_1:14,A1;
then
A58: u|^3 >= u & W|^3 >=1 & W|^3 >= W & u|^3 >=1 by A55,PREPOWER:12,NAT_1:14;
then u|^3*W|^3 >= u*1 & u|^3*W|^3 >= W*1 by XREAL_1:66;
then U > 100*(u|^3*W|^3) >= 100*u & 100*(u|^3*W|^3) >=100*W
by XREAL_1:64,NAT_1:13;
then
A59: U >= 100 *u >= 12* u & U >= 100*W & 100*u >= 16* u
by XXREAL_0:2,XREAL_1:64;
m*U >=1 by NAT_1:14,A35,A24;
then (100*W)*(m*U) >= 100*W*1 >= 5 * k by A57,XREAL_1:66;
then (100*W)*(m*U) >= 5*k by XXREAL_0:2;
then
A60: 5*k <= M by NAT_1:13;
then
A61: (5*k)/M <=1 by XREAL_1:183;
A62: 2*k <= 5*k by XREAL_1:64;
then
A63: M>=2*k by A60,XXREAL_0:2;
then (2*k)/M <=1 by XREAL_1:183;
then
A64: 2*(k/M)<=1 by XCMPLX_1:74;
A65: 4*W <= 100*W & 2*W <= 100*W by XREAL_1:64;
then
A66: 4*W <= U & 2*W <= U by A59,XXREAL_0:2;
then
A67: (2*W) <= U+1 by NAT_1:13;
W <= W+W by NAT_1:11;
then
A68: W <=U by A66,XXREAL_0:2;
Wk <= W-0 by XREAL_1:10;
then 4* Wk <= 4*W & 2* Wk <= 2*W by XREAL_1:64;
then
A69: 4*Wk <= U & 2*Wk <= U by A66,XXREAL_0:2;
then (4*Wk)/U <=1 by XREAL_1:183;
then
A70: (4*Wk)/U* (1/M) <= 1 * (1/M) by XREAL_1:64;
2*(2*(Wk/MU)) = 4 *(Wk/MU)
.= (4*Wk)/MU by XCMPLX_1:74
.= (4*Wk)/U* (1/M) by XCMPLX_1:103;
then
A71: 2*(1/M) + 2*(2*(Wk/MU)) <= 2*(1/M) + 1 * (1/M) = 3*(1/M) =(3*1)/M
by A70,XREAL_1:6,XCMPLX_1:74;
3*1 <= 3*k by XREAL_1:64,A1,NAT_1:14;
then (3*1)/M <= (3*k) /M by XREAL_1:72;
then 2*(1/M) + 2*(2*(Wk/MU)) <= (3*k) /M by A71,XXREAL_0:2;
then
A72: 2*(k/M)+ (2*(1/M) + 2*(2*(Wk/MU))) <= 2*(k/M)+ (3*k) /M
by XREAL_1:6;
2*(k/M) = (2*k)/M by XCMPLX_1:74;
then
A73: 2*(k/M)+ (3*k) /M = (2*k+3*k)/M by XCMPLX_1:62;
then 2*(k/M)+ 2*(1/M) + 0 <= 2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU)) <= 1
by A72,A61,XXREAL_0:2,XREAL_1:6;
then
A74: 2*(k/M)+ 2*(1/M) <= 1 by XXREAL_0:2;
A75: 2*W <= U by A65,A59,XXREAL_0:2;
M>=1 by NAT_1:14;
then
A76: MU>=1*(2*Wk) by A69,XREAL_1:66;
2*k >= 1*k by XREAL_1:64;
then consider t3 be _Theta such that
A77: Py(M,k+1) = (2*M)|^k *(1+ t3*(k/M)) by Th10,A63,XXREAL_0:2;
2*Wk >= 1*Wk by XREAL_1:64;
then consider t4 be _Theta such that
A78: Py(MU,Wk+1) = (2*MU)|^Wk *(1+ t4*(Wk/MU)) by Th10,A76,XXREAL_0:2;
1*M>=2*k by A62,A60,XXREAL_0:2;
then k/M <=1/2 by XREAL_1:102;
then consider T3 be _Theta such that
A79: 1/ (1+ t3*(k/M)) = 1+T3*2*(k/M) by Th7;
1*MU>=2*Wk by A76;
then Wk/MU <=1/2 by XREAL_1:102;
then consider T4 be _Theta such that
A80: 1/ (1+ t4*(Wk/MU)) = 1+T4*2*(Wk/MU) by Th7;
1* mu >= M * (2*W) by A67,XREAL_1:64;
then (W*(2*M))/mu <= 1 by XREAL_1:79;
then (2*M)*(W/mu) <= 1 by XCMPLX_1:74;
then
A81: W/mu <= 1/(2*M) by XREAL_1:77;
then
A82: -(W/mu) >= - 1/(2*M) by XREAL_1:24;
-1 <= t1 <= 1 by Def1;
then (-1)*(W/mu) <= t1*(W/mu) <= 1*(W/mu) by XREAL_1:64;
then
A83: -(1/(2*M)) <= t1*(W/mu) <= 1/(2*M) by A81,A82,XXREAL_0:2;
W+1 <= U+1 by A68,XREAL_1:6;
then
A84: (W+1)*(2*M) <= (U+1) * (2*M) by XREAL_1:64;
(2*mu) <= (2*mu) |^W by A56,A55,PREPOWER:12;
then (W+1) *(2*M) <= 1 * (2*mu) |^W by A84,XXREAL_0:2;
then ( W+1) / (2*mu) |^W <= 1/(2*M) by XREAL_1:102;
then 1/(2*M) >= - ( W+1) / (2*mu) |^W >= - 1/(2*M) by XREAL_1:24;
then
A85: - 1/(2*M) + -1/(2*M) <= t1*(W/mu) + - ( W+1) / (2*mu) |^W
<= 1/(2*M)+1/(2*M) by A83,XREAL_1:7;
A86: (1*1)/(2*M) = 1/2 * (1/M) by XCMPLX_1:76;
A87:t1*(W/mu)- ( W+1) / (2*mu) |^W <= I* (1/M) by A85,A86;
A88: (-I) * (1/M) <= t1*(W/mu)- ( W+1) / (2*mu)|^W by A85,A86;
consider t2 be _Theta such that
A89: t1*(W/mu)- ( W+1) / (2*mu)|^W = t2 * (1/M) by A87,A88,Th4;
consider T5 be _Theta such that
A90: (1+T3*(2*(k/M)))* (1 + t2 * (1/M)) =1+T5*(2*(k/M)+ 2*(1/M))by A64,Th3;
consider T6 be _Theta such that
A91: (1+T5*(2*(k/M)+ 2*(1/M)))* (1+T4*(2*(Wk/MU))) =
1+T6 *(2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU))) by A74,Th3;
A92: |.2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU)).| = 2*(k/M)+ 2*(1/M)
+ 2*(2*(Wk/MU));
A93:|.(5*k)/M.| = (5*k)/M;
consider T7 be _Theta such that
A94: T6*(2*(k/M)+ 2*(1/M) + 2*(2*(Wk/MU))) = T7* ((5*k)/M)
by A73,A72,A92,A93,Th2;
A95: 1/S = (1/(2*M)|^k) * (1+T3*2*(k/M)) by A79,A77,XCMPLX_1:102;
A96: 1/T = (1/(2*MU)|^Wk) *(1+T4*2*(Wk/MU)) by A80,A78,XCMPLX_1:102;
A97:(2*mu) |^W = ((2*M)*(U+1)) |^W
.= ((2*M)|^W) *((U+1) |^W) by NEWTON:7;
((2*M)*U)|^Wk = (2*M) |^Wk * U|^Wk by NEWTON:7;
then
A98:((2*M)|^k) * ((2*MU)|^Wk) = (2*M)|^k * (2*M) |^Wk * U|^Wk
.= (2*M)|^(k+Wk) * U|^Wk by NEWTON:8;
(1/(2*M)|^k) * (1/(2*MU)|^Wk)
= 1/ ( (2*M)|^W * U|^Wk) by A98,XCMPLX_1:102;
then
A99: ((2*mu) |^W) * (1/(2*M)|^k) * (1/(2*MU)|^Wk) =
(((2*M)|^W) *((U+1) |^W)) *(1 / ( (2*M)|^W * U|^Wk)) by A97
.= (((2*M)|^W) *((U+1) |^W)) / ( (2*M)|^W * U|^Wk) by XCMPLX_1:99
.= ((U+1) |^W) / (U|^Wk) by XCMPLX_1:91;
r = (2*mu) |^W *(1+t1*(W/mu)) - ( ((W+1) / (2*mu)|^W) * ((2*mu)|^W))
by A53,XCMPLX_1:87;
then r = (2*mu) |^W *((1+t1*(W/mu)) - (W+1) / (2*mu)|^W );
then
A100: r = (2*mu) |^W * (1 + t2 * (1/M)) by A89;
A101: r/(S*T) = r * (1/(S*T)) by XCMPLX_1:99
.= r * ((1/S) *(1/T)) by XCMPLX_1:102
.= (((U+1) |^W) / (U|^Wk)) *
( (1 + t2 * (1/M)) * (1+T3*2*(k/M)) * (1+T4*2*(Wk/MU))) by A96,A95,A99,A100
.= (((U+1) |^W) / (U|^Wk)) *(1+T7* ((5*k)/M)) by A90,A91,A94;
A102: D = (1/ (U|^(Wk+1)))* Sum IWW < (1/ (U|^(Wk+1)))* (2*(W|^k) * (U|^Wk))
by A50, XREAL_1:68,A49,RVSUM_1:87;
(U+1) |^W = Sum IW = Sum IWk + Sum IWW by A14,RVSUM_1:75,NEWTON:30;
then
A103: Z+D = (1/ (U|^(Wk+1))) * ((U+1) |^W) by A102,A35
.= ((U+1) |^W) / (U|^(Wk+1)) by XCMPLX_1:99;
A104: W >= k+1 by A6,A4,XXREAL_0:2;
A105: W > k by NAT_1:13,A7;
A106: k >=1 by A1,NAT_1:14;
A107: k-'0 = k-0 & W-'0 = W-0 & k-'1 = k-1 by A1,NAT_1:14,XREAL_1:233;
then W-'0 = Wk + (k-'0);
then
A108: U|^(W-'0) = (U|^Wk) * (U|^ (k-'0)) by NEWTON:8;
k-'0 = (k-'1)+1 by A107;
then
A109: (U|^ (k-'0)) * (1/U) = ((U|^ (k-'1))*U) * (1/U) by NEWTON:6
.=(U|^ (k-'1))*(U * (1/U))
.= U|^ (k-'1) by A25;
IWk.(0+1)= (W choose (0+0)) * (U |^(W-'(0+0))) by A13,FINSEQ_3:25,A106,A18;
then
A110: UIWk.1 = (1/ (U|^(Wk+1)))* ((W choose 0) * (U |^(W-'0))) by VALUED_1:6
.= (W choose 0)*(U|^ k1) by A107,A109,A26,A108
.= 1*(U|^ k1) by NEWTON:19;
reconsider Z=Sum UIWk as Element of NAT by ORDINAL1:def 12;
consider uiwk be FinSequence of NAT,y be Element of NAT such that
A111: UIWk = <*y*>^uiwk by A17,FINSEQ_2:130;
Sum UIWk = y+ Sum uiwk by A111,RVSUM_1:76;
then
A112: Sum UIWk>=y+0 by XREAL_1:6;
A113: U*U|^ k1 = U|^(k1+1) by NEWTON:6;
100*U*W*m >= 100*U*W * U|^ k1 by A112,A110,A111,XREAL_1:64;
then
A114: M > 100*W * U|^k by A113,NAT_1:13;
(k+1) * (f * k) >= 1* (f * k) by NAT_1:11,XREAL_1:64;
then (k+1) * (f * k)*100 >= 1* (f * k)*3 by XREAL_1:66;
then 100 * U|^k *W >= 100 * U|^k *(3 * f * k) by XREAL_1:64;
then
A115: M > 300 * (U|^k *( f * k)) by A114,XXREAL_0:2;
A116: 300 * (U|^k *( f * k)) >= 240 * (U|^k *( f * k)) by XREAL_1:64;
then
A117: 240 * f * k * U|^k < M by XXREAL_0:2,A115;
(f*k)*k <= (f*k)*(k+1) by NAT_1:11,XREAL_1:64;
then (f*k)*k*96 <= (f*k)*(k+1)*100 by XREAL_1:66;
then
A118: 96*f*(k*k) <= W & k^2=k*k by SQUARE_1:def 1;
then 12* (8*f*k^2) <= 1*W;
then
A119: (8*f*k^2)/W <=1/12 by XREAL_1:102,A1;
1<=f by A1,NAT_1:14;
then 24*1 <= 96*f by XREAL_1:66;
then 24*1 *k^2 <= 96*f *k^2 by XREAL_1:64;
then
A120: 24*1 *k^2 <= W by A118,XXREAL_0:2;
A121: 1*k^2 <= 24*k^2 by XREAL_1:64;
2*k^2 <= 24*k^2 by XREAL_1:64;
then 2* k^2 <= W*1 by A120,XXREAL_0:2;
then
A122: k^2/W <=1/2 by XREAL_1:102,A1;
k * U|^k *1 <= k * U|^k * f by A1,NAT_1:14,XREAL_1:64;
then k * U|^k *1 *120 <= k * U|^k * f * 240 by XREAL_1:66;
then 12*(((U|^k) * 10 *k)) <= 1*M by A117,XXREAL_0:2;
then
A123: (((U|^k) * 10 *k))/M <=1/12 by XREAL_1:102;
A124: 1*(u|^3*W|^3)<= 100*(u|^3*W|^3) by XREAL_1:64;
W*W*1 <= W|^3 by A54,A1,NAT_1:14,XREAL_1:64;
then W*W * u <= W|^3 * (u|^3) < U by A58,XREAL_1:66,NAT_1:13,A124;
then W*(W * W|^k) <= U by XXREAL_0:2;
then
A125: W*( W|^(k+1)) <= U by NEWTON:6;
1<= k*(k+1) by A1,NAT_1:14;
then 96*1<= k*(k+1)*100 by XREAL_1:66;
then 96*1*f <= k*(k+1)*100*f by XREAL_1:64;
then 96*f *( W|^(k+1)) <= W*( W|^(k+1)) by XREAL_1:64;
then 12* (8*f*W|^(k+1)) <=1 *U by A125,XXREAL_0:2;
then
A126: (8*f*W|^(k+1))/ U<=1/12 by XREAL_1:102;
1<= f*k*(k+1) by A1,NAT_1:14;
then 1*24 <= 100*(f*k*(k+1)) by XREAL_1:66;
then 24*( W|^(k+1)) <= W*( W|^(k+1)) by XREAL_1:64;
then 12*(2* W|^(k+1)) <= U*1 by A125,XXREAL_0:2;
then (2* W|^(k+1)) /U <=1/12 by XREAL_1:102;
then 2* (W|^(k+1) /U) <=1/12 by XCMPLX_1:74;
then
A127:2*((W|^(k+1)) * (1/U)) <= 1/12 by XCMPLX_1:99;
A128: 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M <= 1/12+1/12 = 1/6 <=1/2
by A127,A123,XREAL_1:7;
then
A129: 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M <= 1/2 by XXREAL_0:2;
A130: 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) <= 2*(1/6)<=1
by A128,XREAL_1:64;
A131: 2* ( 2*(W|^(k+1)) * (1/U)+(((U|^k) * 10 *k))/M)<=1 by A130,XXREAL_0:2;
A132: (U+1)/U = U/U +1/U by XCMPLX_1:62
.= 1+I*(1/U) by XCMPLX_1:60;
1/U <= 1/(2*W) by A66,XREAL_1:118,A1;
then consider T8 be _Theta such that
A133: (1+I*(1/U))|^W = 1+ T8*2*W* (1/U) by Th9;
A134: ((U+1) |^W) / (U|^Wk) = (U|^k) * (((U+1) |^W) / ((U|^Wk) * (U|^k)))
by XCMPLX_1:92
.= (U|^k) * (((U+1) |^W) / ((U|^ (Wk+k)))) by NEWTON:8
.= (U|^k) * (1+ T8*2*W* (1/U)) by A133,A132,PREPOWER:8;
A135:|. 2 .| = 2;
A136: (2*W)/U <=1 by XREAL_1:183,A66;
then
A137: -((2*W)/U) >= -1 by XREAL_1:24;
-1<= T8<=1 by Def1;
then (-1)*((2*W)/U)<= T8*((2*W)/U)<=1 *((2*W)/U) by XREAL_1:64;
then -1 <= T8*((2*W)/U)<= 1 by A136,A137,XXREAL_0:2;
then
A138: -1+1 <= T8*((2*W)/U)+1<= 1+1 by XREAL_1:6;
A139:(2*W)* (1/U) = (2*W)/U by XCMPLX_1:99;
then |.(1+ T8*2*W* (1/U)).| = (1+ T8*2*W* (1/U)) by A138,ABSVALUE:def 1;
then consider T9 be _Theta such that
A140: T7* (1+ T8*2*W* (1/U)) = T9*2 by Th2,A135,A138,A139;
A141: (U|^k) * (1+ T8*2*W* (1/U)) * (T7* ((5*k)/M)) =
(U|^k) * ((1+ T8*2*W* (1/U)) * T7)* ((5*k)/M)
.= (U|^k) * (2*T9)* ((5*k)/M) by A140
.= T9 * ( ((U|^k) * 2) * ((5*k)/M))
.= T9 * ((((U|^k) * 2) * (5*k))/M) by XCMPLX_1:74;
A142: (1/ (U|^(Wk+1))) * U = (1/ (U* U|^Wk)) * U by NEWTON:6
.= 1/ (U|^Wk) by XCMPLX_1:92;
A143: D*U = U*((1/ (U|^(Wk+1)))* Sum IWW) by RVSUM_1:87;
IWW<>{} by A16;
then consider iww be FinSequence of REAL,x be Element of REAL such that
A144: IWW = <*x*>^iww by FINSEQ_2:130;
1<= Wk+1 by NAT_1:11;
then (W choose(k+0))*(U|^(W-'(k+0)))=IWW.(0+1) by A44,A15,A2,A14,FINSEQ_3:25
.= x by A144;
then
A145: x = (W choose k) * (U |^Wk) by A3,XXREAL_0:2,XREAL_1:233;
Wk>0 by A105,XREAL_1:50;
then reconsider Wk1=Wk-1 as Nat;
A146: len <*x*> = 1 by FINSEQ_1:40;
then Wk+1 = 1 +len iww by A144,A15,A2,A14,FINSEQ_1:22;
then
A147: len iww = W-(k+1)+1;
for i be Nat st i+1 in dom iww holds iww.(i+1) =
(W choose ((k+1)+i)) * (U |^(W-'((k+1)+i)))
proof
let i be Nat such that
A148: i+1 in dom iww;
iww.(i+1) = IWW.(1+(i+1)) by A144,A146,A148,FINSEQ_1:def 7
.= (W choose (k+(i+1))) * (U |^(W-'(k+(i+1))))
by A44,FINSEQ_1:28,A148,A144,A146;
hence thesis;
end;
then
A149: 0 < Sum iww < 2*(W|^(k+1)) * (U|^(W-'(k+1))) by Th14,A104,A75,A147;
A150: (1/ (U|^Wk)) *x = (1/ (U|^Wk)) * (U |^Wk) * (W choose k) by A145
.=1 * (W choose k) by XCMPLX_1:87;
Sum IWW = x+ Sum iww by A144,RVSUM_1:76;
then
A151: D*U = (W choose k) + (1/ (U|^Wk))*Sum iww by A143,A142,A150;
A152: W-'(k+1) = W-(k+1) = Wk1 by A6,A4,XXREAL_0:2,XREAL_1:233;
Wk = Wk1+1;
then
A153:(1/(U|^Wk))*(U|^(W-'(k+1)))=1/(U*U|^Wk1)*(U|^Wk1) by A152,NEWTON:6
.= 1/U by XCMPLX_1:92;
(1/ (U|^Wk))*Sum iww < (1/ (U|^Wk))* (2*(W|^(k+1)) * (U|^(W-'(k+1))))
by A149, XREAL_1:68;
then consider T10 be _Theta such that
A154: I*((1/ (U|^Wk))*Sum iww)=T10*(2*(W|^(k+1))*(1/U)) by A153,A149,Th5;
A155: (Wk+k) choose k >= Wk+1 > Wk by NAT_1:13,14,A1,RAMSEY_1:11;
then W choose k >=1 by NAT_1:14;
then reconsider T12 = 1/ (W choose k) as _Theta by Def1,XREAL_1:183;
A156: (W choose k) * T12 = 1 by XCMPLX_1:87,A155;
consider T11 be _Theta such that
A157: T10* (2*(W|^(k+1)) * (1/U)) + T9 * ((((U|^k) * 10 *k))/M) =
T11* ( 2*(W|^(k+1))* (1/U) + (((U|^k) * 10 *k))/M) by Th6;
(Z+D)*U = ((U+1) |^W) / (U|^Wk*U) * U by A103,NEWTON:6
.= ((U+1) |^W) / (U|^Wk) by XCMPLX_1:92;
then
A158: r/(S*T) - m*U = D*U+(((U+1) |^W)/(U|^Wk)) *(T7*((5*k)/M)) by A101
.= (W choose k) + T10* (2*(W|^(k+1)) * (1/U)) + T9 * ((((U|^k) * 10 *k))/M)
by A151,A154,A141,A134
.= (W choose k) + T11* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) by A157
.= (W choose k) + (W choose k) * T12 * T11*
( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) by A156
.= (W choose k) *(1+ (T12*T11)*
( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M));
consider T131 be _Theta such that
A159: W choose k = W|^k / (k!) * (1+T131*(k^2/W))
by A121,A120,XXREAL_0:2,Th8;
consider T13 be _Theta such that
A160: 1 / (1+T131*(k^2/W)) = 1+T13*2*(k^2/W) by Th7,A122;
A161: 1 / (W|^k / (k!) * (1+T131*(k^2/W))) =
(1 / (W|^k / (k!))) * ( 1/ (1+T131*(k^2/W))) by XCMPLX_1:102
.= (k! / (W|^k)) * ( 1/ (1+T131*(k^2/W))) by XCMPLX_1:57;
consider T14 be _Theta such that
A162: 1 / (1+(T12*T11)* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)) =
1+T14*2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) by Th7,A129;
A163: k! / (W|^k) * W|^k = k! by XCMPLX_1:87,A1;
consider T15 be _Theta such that
A164: ( 1+T14*(2* ( 2*(W|^(k+1))*(1/U) + (((U|^k) * 10 *k))/M)) ) *
( 1+T13*(2*(k^2/W)))
= 1 + T15 * ( 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) +
2* (2*(k^2/W)) ) by A131,Th3;
A165: 1 * (u / (r/(S*T) - m*U)) = (1 / (r/(S*T) - m*U)) * 1 *u
by XCMPLX_1:101
.= ( 1 / (W choose k)) * ( 1+T14*2* ( 2*(W|^(k+1)) * (1/U) +
(((U|^k) * 10 *k))/M) )* u by A162,A158,XCMPLX_1:102
.= k! * (( 1+T13*(2*(k^2/W))) * ( 1+T14*(2* ( 2*(W|^(k+1)) * (1/U) +
(((U|^k) * 10 *k))/M)) )) by A160,A163,A159,A161
.= k! * (1 + T15 * ( 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) +
2* (2*(k^2/W)))) by A164;
-f <=0;
then k! -f*2+2*f<= 0+2*f by A1,XREAL_1:6;
then reconsider T16= k!/(2*f) as _Theta by Def1,XREAL_1:183;
A166: (2*f) * ( 2* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) +
2* (2*(k^2/W)))
= (8*f*(W|^(k+1))) * (1/U) + (2*f)*(2*( (((U|^k) * 10 *k))/M)) +
(2*f)*(2* (2*(k^2/W)))
.= (8*f*W|^(k+1))/ U + (4*f* (((U|^k) * 10 *k)/M)) + (8*f*(k^2/W))
by XCMPLX_1:99
.= (8*f*W|^(k+1))/ U + ( ( 4*f)* ((U|^k) * 10 *k))/M + (8*f*(k^2/W))
by XCMPLX_1:74
.= (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M + (8*f*k^2)/W by XCMPLX_1:74;
k! = T16*(2*f) by XCMPLX_1:87,A1;
then
A167: u / (r/(S*T) - m*U)
= k!+ (T15* T16)*((2*f) * ( 2* ( 2*(W|^(k+1)) * (1/U) +
(((U|^k) * 10 *k))/M) + 2* (2*(k^2/W)))) by A165
.= k!+ (T15* T16)*((8*f*W|^(k+1))/ U+(40*f*(U|^k)*k)/M+(8*f*k^2)/W)by A166;
6*( 40*f *(U|^k)*k) < 1*M by A116,XXREAL_0:2,A115;
then
A168: ( 40*f *(U|^k)*k)/M < 1/6 by XREAL_1:106;
(8*f*W|^(k+1))/ U + (8*f*k^2)/W <= (1/12) +(1/12) by A119,A126,XREAL_1:7;
then
A169: (8*f*W|^(k+1))/ U + (8*f*k^2)/W + (40*f *(U|^k)*k)/M <
(1/12) +(1/12)+(1/6) by A168,XREAL_1:8;
-1 <= (T15* T16)<=1 by Def1;
then (1/3) *(-1) < (-1) * ( (8*f*W|^(k+1))/ U +
( 40*f *(U|^k)*k)/M + (8*f*k^2)/W ) <=
(T15* T16)*( (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M + (8*f*k^2)/W )
<= 1 *( (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M + (8*f*k^2)/W ) < 1/3
by A169,XREAL_1:64,69;
then (1/3) *(-1) < (T15* T16)*( (8*f*W|^(k+1))/ U + ( 40*f *(U|^k)*k)/M
+ (8*f*k^2)/W ) < 1/3 by XXREAL_0:2;
then -1/2 < u / (r/(S*T) - m*U)-f < 1/2 by A1,A167, XXREAL_0:2;
then (u /(r/(S*T) - m*U)-f)^2 < (1/2)^2 = (1/2)*(1/2) by SQUARE_1:def 1,50;
then
A170: (u / (r/(S*T) - m*U)-f)* (u / (r/(S*T)-m*U)-f)<1/4 by SQUARE_1:def 1;
set R = r - m*S*T*U;
A171:R<>0
proof
assume R=0; then
A172: r/(S*T) = (m*U*(S*T))/(S*T)
.= m*U * ((S*T)/(S*T)) by XCMPLX_1:74
.= m*U * 1 by XCMPLX_1:60;
A173: - (2*(W|^(k+1))*(1/U) + (((U|^k)*10*k))/M)>=-1/2
by A129,XREAL_1:24;
-1 <= (T12*T11) by Def1;
then (-1) *( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M) <=
(T12*T11)*( 2*(W|^(k+1))*(1/U)+(((U|^k)*10*k))/M) by XREAL_1:64;
then -1/2 <= (T12*T11)* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)
by A173,XXREAL_0:2;
then -1/2+1 <= (T12*T11)* ( 2*(W|^(k+1)) * (1/U) + (((U|^k) * 10 *k))/M)+1
by XREAL_1:6;
hence thesis by A158,XCMPLX_1:87,A155,A172;
end;
A174: u^2 = u*u & S^2=S*S & R^2 = R*R & T^2=T*T & f^2=f*f by SQUARE_1:def 1;
A175: (u*S*T-f*R)/R = (u*S*T)/R-(f*R)/R by XCMPLX_1:120
.=(u*(S*T))/R-f by A171,XCMPLX_1:89
.= (u/(R/(S*T)))-f by XCMPLX_1:77
.= (u/(r/(S*T)-((m*U)*(S*T))/(S*T)))-f by XCMPLX_1:120
.= (u/(r/(S*T)-m*U)) -f by XCMPLX_1:89;
((u*S*T-f*R)/R) * ((u*S*T-f*R)/R)*4 <1/4 *4
by XREAL_1:68,A170,A175;
then ((u*S*T-f*R)/R) * ((u*S*T-f*R)/R)*4 *(R*R) <1 *(R*R) by A171,XREAL_1:68;
then ((u*S*T-f*R)/R*R) * ((u*S*T-f*R)/R*R)*4 <1 *(R*R);
then ((u*S*T-f*R)/R*R) * (u*S*T-f*R) *4 < R*R by A171, XCMPLX_1:87;
then (u*S*T-f*R) * (u*S*T-f*R) *4 < R*R by A171, XCMPLX_1:87;
then (u^2)*(S^2)*(T^2)*4 - 8 * (u*S*T)*(f*R) +
4 * (f^2)*(R^2)+8 * (u*S*T)*(f*R)
< R^2 + 8 * (u*S*T)*(f*R) by A174,XREAL_1:6;
then
A176:(u^2)*(S^2)*(T^2)*4 - 8 * (u*S*T)*(f*R) + 4 * (f^2)*(R^2)+
8 *(u*S*T)*(f*R) - R^2 < R^2 + 8 * (u*S*T)*(f*R)-R^2 by XREAL_1:14;
take m,r,s,t,u,W,U,S,T,Q,M;
thus thesis by A1,A176,Th12,A36,A38,A41,A43;
end;
theorem Th17:
for A be non trivial Nat for C,B be Nat, e st 0 < B holds
C = Py(A,B) implies
ex i,j be Nat, D,E,F,G,H,I be Nat st
D*F*I is square &
F divides (H - C) &
B <= C &
D = (A^2-1)*C^2+1 & E = 2*(i+1)*D*(e+1)*C^2 & F= (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*j*C & I = (G^2-1)*H^2+1
proof
let A be non trivial Nat;
let C,B be Nat,e such that
A1: B>0 and
A2: C= Py(A,B);
set x = Px(A,B),D=x^2;
Px(A,0) = 1 & Py(A,0) = 0 by HILB10_1:3;
then
A3: Px(A,0+1) = 1*A + 0*(A^2-'1) & Py(A,0+1) = 1 + 0*A by HILB10_1:6;
A4: x*x <>0;
A5: D>0 by A4,SQUARE_1:def 1;
ex q,i be Nat st 2*D*(e+1)*C^2 *(i+1) = Py(A,q)
proof
set t = e+1;
A6: 2^2=2*2 & D^2=D*D & t^2=t*t&C^2^2=C^2*C^2&C^2=C*C by SQUARE_1:def 1;
then reconsider dd=(A^2-'1) * (2^2)*(D^2) *(t^2) *(C^2^2)
as non square Nat by A5,A1,A2;
consider x,y be Nat such that
A7: x^2 -dd *y^2 =1 & y <>0 by PELLS_EQ:14;
reconsider i=y-1 as Nat by A7;
A8: (2^2)*(D^2)*(t^2)*(C^2^2) *(y^2) = (2*2)*(D*D)*(t*t)*(C^2*C^2)*(y*y)
by A6,SQUARE_1:def 1
.= (2*D*t*C^2*y)*(2*D*t*C^2*y)
.= (2*D*t*C^2*y)^2 by SQUARE_1:def 1;
x^2 - (A^2-'1) * (2*D * t *C^2 *y)^2 = 1 by A7,A8;
then [x,2*D * t *C^2 *y] is Pell's_solution of A^2-'1 by Lm1;
then consider n such that
A9: x= Px(A,n) & 2*D * t *C^2 *y = Py(A,n) by HILB10_1:4;
take n,i;
thus thesis by A9;
end;
then consider q,i be Nat such that
A10: 2*D*(e+1)*C^2*(i+1) = Py(A,q);
set E=Py(A,q), F = Px(A,q)^2;
x^2 - (A^2-'1) *C^2 = 1 by A2,HILB10_1:7;
then
A11:D= (A^2-'1)*C^2+1;
A12: F - (A^2-'1) *(E^2) = 1 by HILB10_1:7;
then
A13: F = (A^2-'1)*E^2+1;
A14: C^2=C*C by SQUARE_1:def 1;
q<>0 by A5,A1,A2,A14,HILB10_1:3,A10;
then q>=1+0 by NAT_1:13;
then
A15: A <= Px(A,q) by A3,HILB10_1:10;
then Px(A,q) > 1 by NEWTON03:def 1,XXREAL_0:2;
then
A16: A*1 < Px(A,q)*Px(A,q) = F by A15,XREAL_1:97,SQUARE_1:def 1;
then
F-A > 0 by XREAL_1:50;
then reconsider G=A +F*(F-A) as non trivial Nat by A16;
set H=Py(G,B), I=Px(G,B)^2;
A17: I - (G^2-'1) *(H^2) = 1 by HILB10_1:7;
H,B are_congruent_mod (2*C)
proof
A18: E^2 = E*E by SQUARE_1:def 1;
A19: (A^2 -'1) *E, (A^2 -'1) *E are_congruent_mod 2*C by INT_1:11;
A20: 1,1 are_congruent_mod 2*C by INT_1:11;
A21: A,A are_congruent_mod 2*C by INT_1:11;
C^2 = C*C by SQUARE_1:def 1;
then ((i+1)*D*(e+1)*C)*(2*C) = E-0 by A10;
then E,0 are_congruent_mod 2*C by INT_1:def 5;
then (A^2 -'1) *E*E,(A^2 -'1) *E*0 are_congruent_mod 2*C by A19,INT_1:18;
then
A22: (A^2 -'1)*E^2+1,0+1 are_congruent_mod 2*C by A18,A20,INT_1:16;
then F-A, 1-A are_congruent_mod 2*C by A12,A21,INT_1:17;
then F*(F-A), 1*(1-A) are_congruent_mod 2*C by A22,A12,INT_1:18;
then A+ F*(F-A), A+ 1*(1-A) are_congruent_mod 2*C by A21,INT_1:16;
then ex i4 be Integer st 2*C*i4 = G-1 by INT_1:def 5;
hence thesis by HILB10_1:24,INT_1:20;
end;
then consider j be Integer such that
A23: H-B = (2*C)*j by INT_1:def 5;
j*(2*C) >=B-B by A23,HILB10_1:13,XREAL_1:9;
then j >= 0 by A1,A2;
then reconsider j as Element of NAT by INT_1:3;
A*A=A^2 by SQUARE_1:def 1;
then
A24: A^2>=1+0 by NAT_1:13;
G*G=G^2 by SQUARE_1:def 1;
then
A25: G^2>=1+0 by NAT_1:13;
A +F*(F-A) - A = F*(F-A);
then
A26: H,C are_congruent_mod F by A2,HILB10_1:26,INT_1:def 5;
take i,j, D,E,F,G,H,I;
thus D*F*I is square & F divides (H - C) & B <= C
by A2,HILB10_1:13,A26,INT_1:def 4;
I - (G^2-1) *(H^2) = 1 by A17,A25,XREAL_1:233;
hence thesis by A11,A24,A10,A13,A23,XREAL_1:233;
end;
theorem Th18:
for A be non trivial Nat for C,B be Nat, e be Nat st 0 < B
for i,j be Nat, D,E,F,G,H,I be Integer st
D*F*I is square & F divides (H - C) & B <= C &
D= (A^2-1)*C^2+1 & E= 2*(i+1)*D*(e+1)*C^2 & F= (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*j*C & I = (G^2-1)*H^2+1
holds C = Py(A,B)
proof
let A be non trivial Nat, C,B be Nat, e be Nat such that
A1: 0 < B;
let i,j be Nat, D,E,F,G,H,I be Integer such that
A2: D*F*I is square & F divides (H - C) & B <= C and
A3: D= (A^2-1)*C^2+1 and
A4: E= 2*(i+1)*D*(e+1)*C^2 and
A5: F= (A^2 -1) *E^2+1 and
A6: G = A+F*(F-A) and
A7: H = B+2*j*C and
A8: I = (G^2-1)*H^2+1;
A9: A*A=A^2 by SQUARE_1:def 1;
then A^2>=1+0 by NAT_1:13;
then
A10: A^2-'1 = A^2-1 by XREAL_1:233;
A11: C^2=C*C>0 by A1,A2,SQUARE_1:def 1;
reconsider D as Element of NAT by INT_1:3,A9,A3;
reconsider E as Element of NAT by A9,A3,A4,INT_1:3;
E^2=E*E>0 by A9,A3,A11,A4,SQUARE_1:def 1;
then
A12:E^2>=1 by NAT_1:14;
reconsider F as Element of NAT by A9,A5,INT_1:3;
A13: A>=2 by NAT_2:29;
A-1 >=2-1 by NAT_2:29,XREAL_1:9;
then (A-1) *(A+1)>= 1*(A+1) by XREAL_1:64;
then (A-1) *(A+1)*E^2>= 1*(A+1)*1 by A12,XREAL_1:66;
then (A-1) *(A+1)*E^2+1>= A+1+0 by XREAL_1:7;
then
A14: F>A by A9,A5,NAT_1:13;
then
A15:F-A>A-A by XREAL_1:14;
then G >0+A by A6,XREAL_1:8,A9,A5;
then
A16:G >1+1 by A13,XXREAL_0:2;
reconsider G as Element of NAT by A15,A6,INT_1:3;
G>1 by NAT_1:13,A16;
then reconsider G as non trivial Element of NAT by NEWTON03:def 1;
reconsider H as Element of NAT by A7,INT_1:3;
A17: G*G=G^2 by SQUARE_1:def 1;
then G^2>=1+0 by NAT_1:13;
then
A18:G^2-'1 = G^2-1 by XREAL_1:233;
reconsider I as Element of NAT by A17,A8,INT_1:3;
A19: E^2 = E*E by SQUARE_1:def 1;
A20: (A^2 -'1) *E, (A^2 -'1) *E are_congruent_mod 2*C by INT_1:11;
A21: 1,1 are_congruent_mod 2*C by INT_1:11;
A22: A,A are_congruent_mod 2*C by INT_1:11;
A23: (A^2 -'1) *E, (A^2 -'1) *E are_congruent_mod D by INT_1:11;
A24: 1,1 are_congruent_mod D by INT_1:11;
A25: F-A,F-A are_congruent_mod D by INT_1:11;
A26: A,A are_congruent_mod D by INT_1:11;
A27: H^2,H^2 are_congruent_mod D by INT_1:11;
A28: 1,1 are_congruent_mod F by INT_1:11;
E-0=2*(i+1)*(e+1)*C^2*D by A4;
then
A29: E,0 are_congruent_mod D by INT_1:def 5;
((A^2 -'1) *E)*E, ((A^2 -'1) *E)*0 are_congruent_mod D by A29,A23,INT_1:18;
then
A30:(A^2 -'1) * E^2+1, 0+1 are_congruent_mod D by A19,A24,INT_1:16;
then F*(F-A),1*(F-A) are_congruent_mod D by A10,A5,A25,INT_1:18;
then G,1*(F-A)+A are_congruent_mod D by A6,A26,INT_1:16;
then G,1 are_congruent_mod D by A30,A10,A5,INT_1:15;
then G*G,1*1 are_congruent_mod D by INT_1:18;
then G^2,1 are_congruent_mod D by SQUARE_1:def 1;
then G^2-1,1-1 are_congruent_mod D by A24,INT_1:17;
then (G^2-1)*H^2,0*H^2 are_congruent_mod D by A27,INT_1:18;
then
A31: I,0+1 are_congruent_mod D by A24,A8,INT_1:16;
A32: G-A = F*(F-A) by A6;
then
A33: G,A are_congruent_mod F by INT_1:def 5;
A34: H*H=H^2 by SQUARE_1:def 1;
A35:H,C are_congruent_mod F by A2,INT_1:def 4;
then
A36: H^2,C^2 are_congruent_mod F &
G^2,A^2 are_congruent_mod F by A11,A9,A17,A34,A33,INT_1:18;
then G^2-1,A^2-1 are_congruent_mod F by INT_1:17,A28;
then
A37: (G^2-1)*H^2,(A^2-1)*C^2 are_congruent_mod F by A36,INT_1:18;
A38: F gcd D = 1 gcd D =1 by WSIERP_1:8,43,A30,A10,A5;
then
A39: F,D are_coprime by INT_2:def 3;
I gcd D = 1 gcd D by WSIERP_1:43,A31;
then I,D are_coprime by WSIERP_1:8,INT_2:def 3;
then
A40: F*I,D are_coprime by A39,INT_2:26;
I gcd F = D gcd F by WSIERP_1:43,A37,A3,A8,A28,INT_1:16;
then
A41: I,F are_coprime by A38,INT_2:def 3;
(F*I)*D is square by A2;
then
A42: F*I is square & D is square by A40,PYTHTRIP:1;
then
A43: F is square & I is square by A41,PYTHTRIP:1;
consider d be Nat such that
A44:d^2 =D by A42,PYTHTRIP:def 3;
consider f be Nat such that
A45: f^2 =F by A43,PYTHTRIP:def 3;
consider ii be Nat such that
A46:ii^2 =I by A43,PYTHTRIP:def 3;
d^2 - (A^2-'1)*C^2 = 1 by A44,A3,A10;
then [d,C] is Pell's_solution of (A^2-'1) by Lm1;
then consider i1 be Nat such that
A47: d = Px(A,i1) & C = Py(A,i1) by HILB10_1:4;
f^2 - (A^2-'1)*E^2 = 1 by A5,A45,A10;
then [f,E] is Pell's_solution of (A^2-'1) by Lm1;
then consider n1 be Nat such that
A48: f = Px(A,n1) & E = Py(A,n1) by HILB10_1:4;
ii^2 - (G^2-'1)*H^2 = 1 by A18,A46,A8;
then [ii,H] is Pell's_solution of (G^2-'1) by Lm1;
then consider j1 be Nat such that
A49: ii = Px(G,j1) & H = Py(G,j1) by HILB10_1:4;
A50: Py(G,j1),j1 are_congruent_mod (2*C)
proof
C^2 = C*C by SQUARE_1:def 1;
then ((i+1)*D*(e+1)*C)*(2*C) = E-0 by A4;
then E,0 are_congruent_mod 2*C by INT_1:def 5;
then (A^2 -'1) *E*E,(A^2 -'1) *E*0 are_congruent_mod 2*C by A20,INT_1:18;
then
A51: (A^2 -'1)*E^2+1,0+1 are_congruent_mod 2*C by A19,A21,INT_1:16;
then F-A, 1-A are_congruent_mod 2*C by A10,A5,A22,INT_1:17;
then F*(F-A), 1*(1-A) are_congruent_mod 2*C
by A10,A51,A5,INT_1:18;
then A+ F*(F-A), A+ 1*(1-A) are_congruent_mod 2*C by A22,INT_1:16;
then ex i4 be Integer st 2*C*i4 = G-1 by A6,INT_1:def 5;
hence thesis by INT_1:20,HILB10_1:24;
end;
B-H = (2*C)*(-j) by A7;
then B,Py(G,j1) are_congruent_mod (2*C) by A49,INT_1:def 5;
then
A52: B,j1 are_congruent_mod (2*C) by A50,INT_1:15;
Py(G,j1), Py(A,j1) are_congruent_mod F by A32,INT_1:def 5,HILB10_1:26;
then
A53: Py(A,j1), Py(G,j1) are_congruent_mod F by INT_1:14;
A54: F divides Py(A,j1) - Py(A,i1) by A35,A47,A49,A53,INT_1:15,INT_1:def 4;
Px(A,n1) divides Px(A,n1)*Px(A,n1) = Px(A,n1)^2 = F
by A48,SQUARE_1:def 1,INT_1:def 3,A45;
then
A55: Py(A,j1),Py(A,i1) are_congruent_mod Px(A,n1)
by A54,INT_2:9,INT_1:def 4;
Py(A,i1) divides n1 by A47,A48,HILB10_1:37,A4,INT_1:def 3;
then
A57:2*Py(A,i1) divides 2*n1 by PYTHTRIP:7;
f*f = F > 2 by A13,A14,XXREAL_0:2, A45,SQUARE_1:def 1;
then f<>1 = Px(A,0) by HILB10_1:3;
then n1<>0 by A48;
then j1,i1 are_congruent_mod 2*n1 or j1,-i1 are_congruent_mod 2*n1
by A55,HILB10_1:33;
then 2*n1 divides j1-i1 or 2*n1 divides j1-(-i1) by INT_1:def 4;
then
A58: j1,i1 are_congruent_mod 2*Py(A,i1) or j1,-i1 are_congruent_mod 2*Py(A,i1)
by INT_1:def 4,INT_2:9,A57;
A59: i1 <=C by A47,HILB10_1:13;
per cases by A58,A47,A52,INT_1:15;
suppose
B,i1 are_congruent_mod 2*C;
then consider z be Integer such that
A60: 2*C*z = B-i1 by INT_1:def 5;
A61: 1*C < 2*C by A2,A1,XREAL_1:68;
then
A62: (-1)*(2*C) < (-1) *C by XREAL_1:69;
0-C <= B-i1 <= C-0 by A2,A59,XREAL_1:13;
then (-1)*(2*C) < 2*C*z < 2*C*1 by A60,A62,A61,XXREAL_0:2;
then -1 < z <1+0 by XREAL_1:64;
then -1+1 <= z <= 0 by INT_1:7;
then z=0;
hence thesis by A60,A47;
end;
suppose B,-i1 are_congruent_mod 2*C;
then consider z be Integer such that
A63: 2*C*z = B--i1 by INT_1:def 5;
0+0< B+i1 <= C+C by A2,A1,A59,XREAL_1:7;
then 0*(2*C) < z*(2*C) <= (2*C)*1 by A63;
then 0 < z <= 1 by XREAL_1:68;
then 0+1 <=z <=1 by INT_1:7;
then
A64: z=1 by XXREAL_0:1;
then
A65: B+i1 = C+C by A63;
B=C
proof
assume B<>C;
then B<C by A2,XXREAL_0:1;
hence thesis by A65,A47,HILB10_1:13,XREAL_1:8;
end;
hence thesis by A64,A63,A47;
end;
end;
::$N Diophantine Representation of Solutions to Pell's Equation
::with 2 Explicite Unknowns $i$, $j$
theorem
:: Theorem 4
:: Y. Matiyasevich, J Robinson:
:: Reduction of an Arbitrary Diophantine Equation to One in 13 Unknowns
:: Acta Arithmetica, 27, 1975.
for A be non trivial Nat,C,B be Nat,e st 0 < B holds
C = Py(A,B) iff
ex i,j be Nat, D,E,F,G,H,I be Integer st
D*F*I is square & F divides (H - C) & B <= C &
D= (A^2-1)*C^2+1 & E= 2*(i+1)*D*(e+1)*C^2 & F= (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*j*C & I = (G^2-1)*H^2+1
proof
let A be non trivial Nat, C,B be Nat, e such that
A1:0 < B;
thus C = Py(A,B) implies ex i,j be Nat, D,E,F,G,H,I be Integer st
D*F*I is square & F divides (H - C) & B <= C & D= (A^2-1)*C^2+1 &
E= 2*(i+1)*D*(e+1)*C^2 & F= (A^2 -1) *E^2+1 & G = A+F*(F-A) &
H = B+2*j*C & I = (G^2-1)*H^2+1
proof
assume C = Py(A,B);
then consider i,j be Nat, D,E,F,G,H,I be Nat such that
A2:D*F*I is square & F divides (H - C) & B <= C & D= (A^2-1)*C^2+1 &
E= 2*(i+1)*D*(e+1)*C^2 & F= (A^2 -1) *E^2+1 & G = A+F*(F-A) &
H = B+2*j*C & I = (G^2-1)*H^2+1 by A1,Th17;
take i,j,D,E,F,G,H,I;
thus thesis by A2;
end;
thus thesis by A1,Th18;
end;
theorem Th20:
for A be non trivial Nat, C be Nat, B,L be positive Nat holds
C = Py(A,B) iff
ex i,j be positive Nat, D,E,F,G,H,I be Integer st
D*F*I is square & F divides (H - C) & B <= C &
D = (A^2-1)*C^2+1 & E = 2*i*C^2*L*D & F = (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1
proof
let A be non trivial Nat, C be Nat, B,L be positive Nat;
reconsider L1=L-1 as Nat;
thus C = Py(A,B) implies
ex i,j be positive Nat, D,E,F,G,H,I be Integer st
D*F*I is square & F divides (H - C) & B <= C &
D = (A^2-1)*C^2+1 & E = 2*i*C^2*L*D & F = (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1
proof
assume C = Py(A,B);
then consider i,j be Nat, D,E,F,G,H,I be Nat such that
A1: D*F*I is square & F divides (H - C) & B <= C &
D= (A^2-1)*C^2+1 & E= 2*(i+1)*D*(L1+1)*C^2 & F= (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*j*C & I = (G^2-1)*H^2+1 by Th17;
take i+1,j+1,D,E,F,G,H,I;
thus thesis by A1;
end;
given i,j be positive Nat, D,E,F,G,H,I be Integer such that
A2:D*F*I is square & F divides (H - C) & B <= C & D= (A^2-1)*C^2+1 and
A3: E= 2*i*C^2*L*D and
A4: F= (A^2 -1) *E^2+1 & G = A+F*(F-A) and
A5: H = B+2*(j-1)*C and
A6: I = (G^2-1)*H^2+1;
reconsider ii=i-1,jj=j-1 as Nat;
E= 2*(ii+1)*D*(L1+1)*C^2 & H = B+2*(jj)*C by A3,A5;
hence thesis by A2,A4,A6,Th18;
end;
begin :: Prime Diophantine Representation
theorem
for k be Nat, L be positive Nat st k>0 holds
k+1 is prime iff
ex f,i,j,m,u be positive Nat,r,s,t be Nat,
A,B,C,D,E,F,G,H,I,W,U,M,S,T,Q be Integer st
D*F*I is square & F divides (H - C) &
(M^2-1)*S^2 +1 is square &
((M*U)^2 -1)*T^2 + 1 is square &
W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
k+1 divides f+1 &
A = M*(U+1) & B = W+1 & C = r + W + 1 & D= (A^2-1)*C^2+1 & E= 2*i*C^2*L*D &
F= (A^2-1)*E^2+1 & G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 &
W = 100*f*k*(k+1) & U = 100*(u|^3)*(W|^3)+1 & M = 100*m*U*W+1 &
S = (M-1)*s+k+1 & T = (M*U-1)*t+W-k+1 & Q = 2*M*W-W^2-1
proof
let k be Nat, L be positive Nat such that
A1:k>0;
A2: k+1-'1 = k+1-1 by XREAL_1:233,NAT_1:11;
thus k+1 is prime implies
ex f,i,j,m,u be positive Nat, r,s,t be Nat,
A,B,C,D,E,F,G,H,I,W,U,M,S,T,Q be Integer st
D*F*I is square & F divides (H - C) & (M^2-1)*S^2 +1 is square &
((M*U)^2 -1)*T^2 + 1 is square &
W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
k+1 divides f+1 &
A = M*(U+1) & B = W+1 & C = r + W + 1 & D= (A^2-1)*C^2+1 & E= 2*i*C^2*L*D &
F= (A^2 -1) *E^2+1 & G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 &
W = 100*f*k*(k+1) & U = 100 * (u|^3)*(W|^3)+1 & M = 100 * m * U *W+1 &
S = (M-1)*s+k+1 & T = (M*U-1)*t +W-k+1 & Q = 2*M*W-W^2 -1
proof
assume k+1 is prime;
then
A3: (k+1-'1)!+1 mod (k+1) =0 & (k+1) >1 by NAT_5:22;
set f= k!;
consider m,r,s,t,u be Nat,
W,U,S,T,Q be Nat, M be non trivial Nat such that
A4: m>0 & u>0 and
A5: r + W + 1 = Py(M*(U+1),W+1) and
A6: (M^2-1)*S^2 +1 is square & ((M*U)^2 -1)*T^2 + 1 is square &
W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) and
A7: W = 100*f*k*(k+1) & U = 100 * (u|^3)*(W|^3)+1 & M = 100 * m * U *W+1 &
S = (M-1)*s+k+1 & T = (M*U-1)*t +W-k+1 & Q = 2*M*W-W^2 -1 by Th16,A1;
set C = r + W + 1, B = W+1, A = M*(U+1);
consider i,j be positive Nat,D,E,F,G,H,I be Integer such that
A8: D*F*I is square & F divides (H - C) & B <= C and
A9: D= (A^2-1)*C^2+1 & E= 2*i*C^2*L*D & F= (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 by A5,Th20;
reconsider m,u as positive Nat by A4;
take f,i,j,m,u,r,s,t,A,B,C,D,E,F,G,H,I,W,U,M,S,T,Q;
thus D*F*I is square & F divides (H - C) by A8;
thus (M^2-1)*S^2 +1 is square & ((M*U)^2 -1)*T^2 + 1 is square &
W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
k+1 divides f+1 by A3,A6,INT_1:62,A2;
thus thesis by A9,A7;
end;
given f,i,j,m,u be positive Nat, r,s,t be Nat,
A,B,C,D,E,F,G,H,I,W,U,M,S,T,Q be Integer such that
A10: D*F*I is square and
A11: F divides (H - C) and
A12: (M^2-1)*S^2 +1 is square and
A13: ((M*U)^2 -1)*T^2 + 1 is square and
A14: W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q and
A15: (4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) and
A16: k+1 divides f+1 and
A17: A = M*(U+1) and
A18: B = W+1 and
A19: C = r + W + 1 and
A20: D= (A^2-1)*C^2+1 and
A21: E= 2*i*C^2*L*D & F= (A^2 -1) *E^2+1 & G = A+F*(F-A) &
H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 and
A22: W = 100*f*k*(k+1) and
A23: U = 100 * (u|^3)*(W|^3)+1 and
A24: M = 100 * m * U *W+1 and
A25: S = (M-1)*s+k+1 and
A26: T = (M*U-1)*t +W-k+1 and
A27: Q = 2*M*W-W^2 -1;
A28: r + (W + 1) >= W+1+0 by XREAL_1:6;
reconsider W,U,M,S as Element of NAT by A22,A23,A24,A25,INT_1:3;
A29: 100*f*k*(k+1) >= 1*(k+1) by A1, NAT_1:14,XREAL_1:64;
A30: W > k by A29,A22,NAT_1:13;
then W-k > 0 by XREAL_1:50;
then (M*U-1)*t +(W-k) >=0+0 by A23,A24;
then reconsider T as Element of NAT by A26,INT_1:3;
reconsider Wk=W-k as Nat by A30,NAT_1:21;
A31: M*W -1 >= 0 by A1,A22,A23,A24;
100 * m * U * W >= 1*W by XREAL_1:64,A23,NAT_1:14;
then
A32: M > W by A24,NAT_1:13;
then M*W >= W*W = W^2 by XREAL_1:64,SQUARE_1:def 1;
then M*W+M*W >= M*W+W^2 by XREAL_1:7;
then M*W+M*W -(W^2+1) >= M*W+W^2 -(W^2+1) by XREAL_1:9;
then reconsider Q as Element of NAT by A31,A27,INT_1:3;
M>=1 & U+1>1 by A22,A23,A24,NAT_1:14,13;
then M*(U+1) > 1*1 by XREAL_1:97;
then reconsider mu1 = M*(U+1) as non trivial Nat by NEWTON03:def 1;
W>= 1 by A1,A22,NAT_1:14;
then M>1 by A32,XXREAL_0:2;
then reconsider M as non trivial Nat by NEWTON03:def 1;
M*(U+1) is non trivial Nat;
then reconsider A as non trivial Nat by A17;
W+1>0;
then reconsider B as positive Nat by A18;
r + W + 1 is Nat;
then reconsider C as Nat by A19;
A33: (k+1) >0+1 by A1,XREAL_1:6;
C = Py(A,B) by A28,A18,A19,A10,A11,A20,A21,Th20;
then f = k! by A1,A12,A13,A14,A15,A22,A23,A24,A25,A26,A27,Th15,A17,A18,A19;
then ((k+1-'1)! +1) mod (k+1) =0 by A16,INT_1:62,A2;
hence k+1 is prime by A33,NAT_5:22;
end;
theorem Th22:
for a,b,A,B be Integer st a,b are_coprime holds
a divides A & b divides B iff a*b divides a*B + b*A
proof
let a,b,A,B be Integer such that
A1: a,b are_coprime;
thus a divides A & b divides B implies a*b divides a*B + b*A
proof
assume
A2: a divides A & b divides B;
then consider x be Integer such that
A3: A= a*x by INT_1:def 3;
consider y be Integer such that
A4: B= b*y by A2,INT_1:def 3;
a*B +b*A = (a*b)*(y+x) by A3,A4;
hence thesis by INT_1:def 3;
end;
assume a*b divides a*B + b*A;
then consider x be Integer such that
A5: a*B+b*A = (a*b)*x by INT_1:def 3;
a*(-B+b*x) = b*A by A5;
hence a divides A by A1,INT_2:25,INT_1:def 3;
b*(-A+a*x) = a*B by A5;
hence b divides B by A1,INT_2:25,INT_1:def 3;
end;
::$N Diophantine Representation of Prime Numbers with 8 Explicite Unknowns
theorem
for k be Nat st k>0 holds
k+1 is prime iff
ex f,i,j,m,u be positive Nat,r,s,t be Nat,
A,B,C,D,E,F,G,H,I,L,W,U,M,S,T,Q be Integer st
D*F*I is square & (M^2-1)*S^2 +1 is square &
((M*U)^2 -1)*T^2 + 1 is square &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
F*L divides (H-C)*L + F*(f+1)*Q + F*(k+1) *((W^2-1)*S*u-W^2*u^2 +1) &
A = M*(U+1) & B = W+1 & C = r + W + 1 & D = (A^2-1)*C^2+1 & E = 2*i*C^2*L*D &
F= (A^2 -1) *E^2+1 & G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 &
L = (k+1)*Q & W = 100*f*k*(k+1) & U = 100 * (u|^3)*(W|^3)+1 &
M = 100 * m * U *W+1 & S = (M-1)*s+k+1 & T = (M*U-1)*t +W-k+1 & Q = 2*M*W-W^2-1
proof
let k be Nat such that
A1: k>0;
A2: k+1-'1 = k+1-1 by XREAL_1:233,NAT_1:11;
thus k+1 is prime implies ex f,i,j,m,u be positive Nat, r,s,t be Nat,
A,B,C,D,E,F,G,H,I, L, W,U,M,S,T,Q be Integer st
D*F*I is square &
(M^2-1)*S^2 +1 is square &
((M*U)^2 -1) *T^2 + 1 is square &
(4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
F*L divides (H-C)*L + F*(f+1)*Q + F*(k+1) *((W^2-1)*S*u-W^2*u^2 +1) &
A = M*(U+1) & B = W+1 & C = r + W + 1 & D= (A^2-1)*C^2+1 & E= 2*i*C^2*L*D &
F= (A^2 -1) *E^2+1 & G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 &
L = (k+1)*Q & W = 100*f*k*(k+1) & U = 100 * (u|^3)*(W|^3)+1 &
M = 100*m*U*W+1 & S = (M-1)*s+k+1 & T = (M*U-1)*t+W-k+1 & Q = 2*M*W-W^2-1
proof
assume k+1 is prime;
then (k+1-'1)!+1 mod (k+1) =0 & (k+1) >1 by NAT_5:22;
then
A3: k+1 divides k!+1 by INT_1:62,A2;
set f= k!;
consider m,r,s,t,u be Nat,W,U,S,T,Q be Nat, M be non trivial Nat such that
A4: m>0 & u>0 and
A5: r + W + 1 = Py(M*(U+1),W+1) and
A6: (M^2-1)*S^2 +1 is square and
A7: ((M*U)^2 -1)*T^2 + 1 is square and
A8: W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q and
A9: (4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) and
A10: W = 100*f*k*(k+1) and
A11: U = 100 * (u|^3)*(W|^3)+1 and
A12: M = 100 * m * U *W+1 and
A13: S = (M-1)*s+k+1 and
A14: T = (M*U-1)*t +W-k+1 and
A15: Q = 2*M*W-W^2 -1 by Th16,A1;
A16: 100*f*k*(k+1) >= 1*(k+1) by A1, NAT_1:14,XREAL_1:64;
A17: W > k by A16,A10,NAT_1:13;
reconsider Wk=W-k as Nat by A17,NAT_1:21;
A18: M*W - 1 >= 0+1 by INT_1:7,A1,A10;
100 * m * U * W >= 1*W by XREAL_1:64,A4,A11,NAT_1:14;
then M > W by A12,NAT_1:13;
then M*W > W*W = W^2 by A10,A1,XREAL_1:68,SQUARE_1:def 1;
then M*W+M*W > M*W+W^2 by XREAL_1:8;
then M*W+M*W -(W^2+1) > M*W+W^2 -(W^2+1) by XREAL_1:9;
then reconsider Q as positive Nat by A15,A18;
set L = (k+1)*Q;
reconsider L as positive Nat;
set C = r + W + 1;
set B = W+1;
set A = M*(U+1);
consider i,j be positive Nat, D,E,F,G,H,I be Integer such that
A19: D*F*I is square & F divides (H - C) & B <= C and
A20: D= (A^2-1)*C^2+1 & E= 2*i*C^2*L*D & F= (A^2 -1) *E^2+1 &
G = A+F*(F-A) & H = B+2*(j-1)*C & I = (G^2-1)*H^2+1 by A5,Th20;
A21: 1,1 are_congruent_mod k+1 by INT_1:11;
A22: 2*M,2*M are_congruent_mod k+1 by INT_1:11;
W-0 = (100*f*k)*(k+1) by A10;
then W,0 are_congruent_mod k+1 by INT_1:def 3,def 4;
then W*W,0*0 are_congruent_mod k+1 &
W*(2*M),0 *(2*M) are_congruent_mod k+1 by A22,INT_1:18;
then 2*M*W-W*W,0-0 are_congruent_mod k+1 by INT_1:17;
then 2*M*W-W*W-1,0-0-1 are_congruent_mod k+1 by A21,INT_1:17;
then Q,-1 are_congruent_mod (k+1) by A15,SQUARE_1:def 1;
then Q gcd (k+1) = -1 gcd (k+1) by WSIERP_1:43;
then Q gcd (k+1) = 1 gcd (k+1)=1 by NEWTON02:1,WSIERP_1:8;
then
A23: Q,k+1 are_coprime by INT_2:def 3;
Q divides -(W^2*u^2 - (W^2-1)*S*u-1-0) by INT_2:10,A8,INT_1:def 4;
then
A24: L divides Q*(f+1) + (k+1)* ((W^2-1)*S*u-W^2*u^2+1) by Th22,A3,A23;
A25: (A^2 -1) *E, (A^2 -1) *E are_congruent_mod L by INT_1:11;
A26: 1,1 are_congruent_mod L by INT_1:11;
E-0 = 2*i*C^2*D*L by A20;
then E,0 are_congruent_mod L by INT_1:def 3,def 4;
then (A^2 -1) *E*E, (A^2 -1) *E*0 are_congruent_mod L by A25,INT_1:18;
then (A^2 -1) *(E*E)+1,0+1 are_congruent_mod L by A26,INT_1:16;
then (A^2 -1) *(E^2)+1,0+1 are_congruent_mod L by SQUARE_1:def 1;
then F gcd L = 1 gcd L=1 by A20,WSIERP_1:8,43;
then F,L are_coprime by INT_2:def 3;
then
A27: F*L divides (Q*(f+1)+(k+1)* ((W^2-1)*S*u-W^2*u^2+1))*F + (H-C)*L
by Th22,A19,A24;
reconsider m,u as positive Nat by A4;
take f,i,j,m,u,r,s,t,A,B,C,D,E,F,G,H,I,L,W,U,M,S,T,Q;
thus D*F*I is square & (M^2-1)*S^2 +1 is square &
((M*U)^2 -1)*T^2 + 1 is square by A19,A6,A7;
thus (4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) &
F*L divides (H-C)*L + F*(f+1)*Q + F*(k+1) *((W^2-1)*S*u-W^2*u^2 +1)
by A9,A27;
thus A = M*(U+1) & B = W+1 & C = r + W + 1 & D= (A^2-1)*C^2+1 &
E= 2*i*C^2*L*D & F= (A^2 -1) *E^2+1 & G = A+F*(F-A) & H = B+2*(j-1)*C &
I = (G^2-1)*H^2+1 by A20;
thus L = (k+1)*Q & W = 100*f*k*(k+1) & U = 100 * (u|^3)*(W|^3)+1 &
M = 100 * m * U *W+1 & S = (M-1)*s+k+1 & T = (M*U-1)*t +W-k+1 &
Q = 2*M*W-W^2 -1 by A10,A11,A12,A13,A14,A15;
end;
given f,i,j,m,u be positive Nat, r,s,t be Nat,
A,B,C,D,E,F,G,H,I, L, W,U,M,S,T,Q be Integer such that
A28: D*F*I is square and
A29: (M^2-1)*S^2 +1 is square and
A30: ((M*U)^2 -1)*T^2 + 1 is square and
A31: (4*f^2 -1)*(r-m*S*T*U)^2 + 4*u^2*S^2*T^2 < 8*f*u*S*T*(r-m*S*T*U) and
A32: F*L divides (H-C)*L + F*(f+1)*Q + F*(k+1) *((W^2-1)*S*u-W^2*u^2 +1) and
A33: A = M*(U+1) and
A34: B = W+1 and
A35: C = r + W + 1 and
A36: D= (A^2-1)*C^2+1 and
A37: E= 2*i*C^2*L*D & F= (A^2 -1) *E^2+1 & G = A+F*(F-A) & H = B+2*(j-1)*C &
I = (G^2-1)*H^2+1 and
A38: L = (k+1)*Q and
A39: W = 100*f*k*(k+1) and
A40: U = 100 * (u|^3)*(W|^3)+1 and
A41: M = 100 * m * U *W+1 and
A42: S = (M-1)*s+k+1 and
A43: T = (M*U-1)*t +W-k+1 and
A44: Q = 2*M*W-W^2 -1;
A45: r + (W + 1) >= W+1+0 by XREAL_1:6;
reconsider W,U,M,S as Element of NAT by A39,A40,A41,A42,INT_1:3;
A46: 100*f*k*(k+1) >= 1*(k+1) by A1, NAT_1:14,XREAL_1:64;
A47: W > k by A46,A39,NAT_1:13;
then W-k > 0 by XREAL_1:50;
then (M*U-1)*t +(W-k) >=0+0 by A40,A41;
then reconsider T as Element of NAT by A43,INT_1:3;
reconsider Wk=W-k as Nat by A47,NAT_1:21;
A48: M*W - 1 >= 0+1 by INT_1:7,A1,A39,A40,A41;
100 * m * U * W >= 1*W by XREAL_1:64,A40,NAT_1:14;
then
A49: M > W by A41,NAT_1:13;
then M*W > W*W = W^2 by A1,A39,XREAL_1:68,SQUARE_1:def 1;
then M*W+M*W > M*W+W^2 by XREAL_1:8;
then M*W+M*W -(W^2+1) > M*W+W^2 -(W^2+1) by XREAL_1:9;
then reconsider Q as positive Nat by A44,A48;
M>=1 & U+1>1 by A39,A40,A41,NAT_1:14,13;
then M*(U+1) > 1*1 by XREAL_1:97;
then reconsider mu1 = M*(U+1) as non trivial Nat by NEWTON03:def 1;
W>= 1 by A1,A39,NAT_1:14;
then M>1 by A49,XXREAL_0:2;
then reconsider M as non trivial Nat by NEWTON03:def 1;
M*(U+1) is non trivial Nat;
then reconsider A as non trivial Nat by A33;
W+1>0;
then reconsider B as positive Nat by A34;
r + W + 1 is Nat;
then reconsider C as Nat by A35;
A50: 1,1 are_congruent_mod k+1 by INT_1:11;
A51: 2*M,2*M are_congruent_mod k+1 by INT_1:11;
W-0 = (100*f*k)*(k+1) by A39;
then W,0 are_congruent_mod k+1 by INT_1:def 3,def 4;
then W*W,0*0 are_congruent_mod k+1 &
W*(2*M),0 *(2*M) are_congruent_mod k+1 by A51,INT_1:18;
then 2*M*W-W*W,0-0 are_congruent_mod k+1 by INT_1:17;
then 2*M*W-W*W-1,0-0-1 are_congruent_mod k+1 by A50,INT_1:17;
then Q,-1 are_congruent_mod (k+1) by A44,SQUARE_1:def 1;
then Q gcd (k+1) = -1 gcd (k+1) by WSIERP_1:43;
then Q gcd (k+1) = 1 gcd (k+1)=1 by NEWTON02:1,WSIERP_1:8;
then
A52: Q,k+1 are_coprime by INT_2:def 3;
A53: (A^2 -1) *E, (A^2 -1) *E are_congruent_mod L by INT_1:11;
A54: 1,1 are_congruent_mod L by INT_1:11;
E-0 = 2*i*C^2*D*L by A37;
then E,0 are_congruent_mod L by INT_1:def 3,def 4;
then (A^2 -1) *E*E, (A^2 -1) *E*0 are_congruent_mod L by A53,INT_1:18;
then (A^2 -1) *(E*E)+1,0+1 are_congruent_mod L by A54,INT_1:16;
then (A^2 -1) *(E^2)+1,0+1 are_congruent_mod L by SQUARE_1:def 1;
then F gcd L = 1 gcd L=1 by A37,WSIERP_1:8,43;
then
A55: F,L are_coprime by INT_2:def 3;
F*L divides (H-C)*L + F*((f+1)*Q + (k+1) *((W^2-1)*S*u-W^2*u^2 +1)) by A32;
then
A56: F divides H-C & Q*(k+1) divides (f+1)*Q+(k+1) *((W^2-1)*S*u-W^2*u^2 +1)
by A38,A55,Th22;
then
A57: Q divides (W^2-1)*S*u-W^2*u^2 +1 & k+1 divides f+1 by A52,Th22;
then Q divides - ((W^2-1)*S*u-W^2*u^2 +1) by INT_2:10;
then Q divides W^2*u^2 - (W^2-1)*S*u-1 - 0;
then
A58:W^2*u^2 - (W^2-1)*S*u-1,0 are_congruent_mod Q by INT_1:def 4;
A59: (k+1) >0+1 by A1,XREAL_1:6;
C = Py(A,B) by A38,A45,A34,A35,A28,A56,A36,A37,Th20;
then f = k! by A1,A29,A30,A58,A31,A39,A40,A41,A42,A43,A44,Th15,A33,A34,A35;
then ((k+1-'1)! +1) mod (k+1) =0 by A57,INT_1:62,A2;
hence k+1 is prime by A59,NAT_5:22;
end;