:: On the Partial Product and Partial Sum of Series and Related Basic
:: Inequalities
:: by Fuguo Ge and Xiquan Liang
::
:: Received November 23, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XXREAL_0, SEQ_1, NEWTON, ARYTM_1, RELAT_1, SQUARE_1,
ARYTM_3, POWER, COMPLEX1, CARD_1, FUNCT_1, SERIES_1, SERIES_3, NAT_1,
REAL_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, NAT_1,
SQUARE_1, NEWTON, SEQ_1, POWER, SERIES_1, SERIES_3;
constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, NEWTON, SERIES_1, SERIES_3,
VALUED_1, ABIAN;
registrations XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, NEWTON, SERIES_3,
NUMBERS, VALUED_0, RELSET_1, FUNCT_2, ORDINAL1;
requirements REAL, SUBSET, NUMERALS, ARITHM;
equalities SQUARE_1;
theorems XCMPLX_1, SQUARE_1, SIN_COS2, NEWTON, POWER, XREAL_1, PREPOWER,
SERIES_1, SERIES_3, COMPLEX1, ABSVALUE, XXREAL_0;
schemes NAT_1;
begin
reserve a,b,c,d for positive Real,
m,u,w,x,y,z for Real,
n,k for Nat,
s,s1 for Real_Sequence;
Lm1: x|^3-y|^3=(x-y)*(x^2+x*y+y^2)
proof
(x-y)*(x^2+x*y+y^2) = x*x^2+x*x*y+x*y^2-(y*x^2+y*x*y+y*y^2)
.=x*x|^2+x*x*y+x*y^2-(y*x^2+y*x*y+y*y^2) by NEWTON:81
.=x|^(2+1)+x*x*y+x*y^2-(y*x^2+y*x*y+y*y^2) by NEWTON:6
.=x|^3+x*(y*y)-y*x*y-y*y^2
.=x|^3-y|^2*y by NEWTON:81
.=x|^3-y|^(2+1) by NEWTON:6;
hence thesis;
end;
Lm2: 2/((1/a)+(1/b))=2*(a*b)/(a+b)
proof
1/((1/a)+(1/b)) = 1/((1*b+1*a)/(a*b)) by XCMPLX_1:116
.=((a*b)*1)/(b+a) by XCMPLX_1:77
.=(a*b)/(b+a);
then (2*1)/((1/a)+(1/b))=2*((a*b)/(b+a)) by XCMPLX_1:74;
hence thesis by XCMPLX_1:74;
end;
Lm3: (1/x)*(1/y)*(1/z)=1/(x*y*z)
proof
(1/x)*(1/y)*(1/z) = 1/(x*y)*(1/z) by XCMPLX_1:102
.=1/((x*y)*z) by XCMPLX_1:102;
hence thesis;
end;
Lm4: for b being Real holds (a/c) to_power -b=(c/a) to_power b
proof
let b be Real;
(a/c) to_power (-b) = (1/(a/c)) to_power b by POWER:32
.=(c/a*1) to_power b by XCMPLX_1:80
.=(c/a) to_power b;
hence thesis;
end;
Lm5: ((sqrt(a*b))^2+(sqrt(c*d))^2)*((sqrt(a*c))^2+(sqrt(b*d))^2) >=b*c*(a+d)^2
proof
a*b^2*d+c^2*d*a>=2*sqrt((a*b^2*d)*(c^2*d*a)) by SIN_COS2:1;
then
(a*b^2*d+c^2*d*a)+((a^2)*b*c+b*c*(d^2))>= 2*sqrt(a^2*b^2*c^2*d^2)+((a^2)
*b*c+b*c*(d^2)) by XREAL_1:7;
then
a*b^2*d+c^2*d*a+(a^2)*b*c+b*c*(d^2)>= 2*sqrt(((a*b)*(c*d))^2)+(a^2)*b*c+
b*c*(d^2);
then
A1: a*b^2*d+c^2*d*a+(a^2)*b*c+b*c*(d^2)>= 2*(a*b*c*d)+(a^2)*b*c+b*c*(d^2) by
SQUARE_1:22;
((sqrt(a*b))^2+(sqrt(c*d))^2)*((sqrt(a*c))^2+(sqrt(b*d))^2) =(a*b+(sqrt(
c*d))^2)*((sqrt(a*c))^2+(sqrt(b*d))^2) by SQUARE_1:def 2
.=(a*b+c*d)*((sqrt(a*c))^2+(sqrt(b*d))^2) by SQUARE_1:def 2
.=(a*b+c*d)*(a*c+(sqrt(b*d))^2) by SQUARE_1:def 2
.=(a*b+c*d)*(a*c+b*d) by SQUARE_1:def 2
.=(a^2)*b*c+a*b^2*d+c^2*d*a+b*c*(d^2);
hence thesis by A1;
end;
Lm6: (x+y+z)^2=x^2+y^2+z^2+2*x*y+2*y*z+2*z*x;
Lm7: |.x.|<1 implies x^2<1
proof
assume |.x.|<1;
then (|.x.|)^2<1^2 by SQUARE_1:16;
hence thesis by COMPLEX1:75;
end;
Lm8: x^2<1 implies |.x.|<1
proof
assume x^2<1;
then sqrt(x^2)<1 by SQUARE_1:18,27,XREAL_1:63;
hence thesis by COMPLEX1:72;
end;
Lm9: 2*a^2*sqrt(b*c)*2*b^2*sqrt(a*c)*2*c^2*sqrt(a*b) = (2*a*b*c)|^3
proof
2*a^2*sqrt(b*c)*2*b^2*sqrt(a*c)*2*c^2*sqrt(a*b) =2^2*2*a^2*b^2*c^2*sqrt(
b*c)*sqrt(a*c)*sqrt(a*b)
.=2|^2*2*a^2*b^2*c^2*sqrt(b*c)*sqrt(a*c)*sqrt(a*b) by NEWTON:81
.=2|^(2+1)*a^2*b^2*c^2*sqrt(b*c)*sqrt(a*c)*sqrt(a*b) by NEWTON:6
.=2|^3*a^2*b^2*c^2*(sqrt(b*c)*sqrt(a*c))*sqrt(a*b)
.=2|^3*a^2*b^2*c^2*sqrt((b*c)*(a*c))*sqrt(a*b) by SQUARE_1:29
.=2|^3*a^2*b^2*c^2*(sqrt(b*c*a*c)*sqrt(a*b))
.=2|^3*a^2*b^2*c^2*sqrt((b*c*a*c)*(a*b)) by SQUARE_1:29
.=2|^3*a^2*b^2*c^2*sqrt((a*b*c)^2)
.=2|^3*a^2*b^2*c^2*(a*b*c) by SQUARE_1:22
.=2|^3*(a^2*a)*(b^2*b)*(c^2*c)
.=2|^3*(a|^2*a)*(b^2*b)*(c^2*c) by NEWTON:81
.=2|^3*(a|^2*a)*(b|^2*b)*(c^2*c) by NEWTON:81
.=2|^3*(a|^2*a)*(b|^2*b)*(c|^2*c) by NEWTON:81
.=2|^3*a|^(2+1)*(b|^2*b)*(c|^2*c) by NEWTON:6
.=2|^3*a|^3*b|^3*(c|^2*c) by NEWTON:6
.=2|^3*a|^3*b|^3*c|^(2+1) by NEWTON:6
.=(2*a)|^3*b|^3*c|^3 by NEWTON:7
.=(2*a*b)|^3*c|^3 by NEWTON:7
.=(2*a*b*c)|^3 by NEWTON:7;
hence thesis;
end;
Lm10: sqrt(a^2+a*b+b^2)=(1/2)*sqrt(4*(a^2+b^2)+4*a*b)
proof
A1: ((1/2)*sqrt(4*(a^2+b^2)+4*a*b))^2 =(1/2)*(1/2)*(sqrt(4*(a^2+b^2)+4*a*b)) ^2
.=(1/4)*(4*(a^2+b^2)+4*a*b) by SQUARE_1:def 2
.=(sqrt(a^2+a*b+b^2))^2 by SQUARE_1:def 2;
A2: sqrt(a^2+a*b+b^2)>0 by SQUARE_1:25;
sqrt(4*(a^2+b^2)+4*a*b)>0 by SQUARE_1:25;
then sqrt((sqrt(a^2+a*b+b^2))^2) =(1/2)*sqrt(4*(a^2+b^2)+4*a*b) by A1,
SQUARE_1:22;
hence thesis by A2,SQUARE_1:22;
end;
Lm11: sqrt(a^2+a*b+b^2)>=(1/2)*sqrt(3)*(a+b)
proof
a^2+b^2>=2*a*b by SERIES_3:6;
then a^2+b^2+(3*(a^2+b^2)+4*a*b)>=2*a*b+(3*(a^2+b^2)+4*a*b) by XREAL_1:6;
then sqrt(4*(a^2+b^2)+4*a*b)>=sqrt(3*(a^2+b^2)+6*a*b) by SQUARE_1:26;
then
A1: (1/2)*sqrt(4*(a^2+b^2)+4*a*b)>=(1/2)*sqrt(3*(a^2+b^2)+6*a*b) by XREAL_1:64;
sqrt(3*(a^2+b^2)+6*a*b) = sqrt(3*(a+b)^2);
then sqrt(3*(a^2+b^2)+6*a*b) = sqrt(3)*sqrt((a+b)^2) by SQUARE_1:29
.=sqrt(3)*(a+b) by SQUARE_1:22;
hence thesis by A1,Lm10;
end;
Lm12: sqrt((a^2+a*b+b^2)/3)<=sqrt((a^2+b^2)/2)
proof
(a^2+b^2)/2>=a*b by SERIES_3:7;
then (a^2+b^2)/2+(a^2+b^2)>=a*b+(a^2+b^2) by XREAL_1:6;
then (a^2+b^2+(a^2+b^2)/2)/3>=(a^2+a*b+b^2)/3 by XREAL_1:72;
hence thesis by SQUARE_1:26;
end;
Lm13: ((b*c)/a)^2+((c*a)/b)^2>=2*c^2
proof
((b*c)/a)^2+((c*a)/b)^2>=2*((b*c)/a)*((c*a)/b) by SERIES_3:6;
then ((b*c)/a)^2+((c*a)/b)^2>=2*(((b*c)/a)*((c*a)/b));
then ((b*c)/a)^2+((c*a)/b)^2>=2*(((b*c)*(c*a))/(a*b)) by XCMPLX_1:76;
then ((b*c)/a)^2+((c*a)/b)^2>=2*(((b*a)*(c*c))/((a*b)*1));
then ((b*c)/a)^2+((c*a)/b)^2>=2*((c*c)/1) by XCMPLX_1:91;
hence thesis;
end;
Lm14: ((b*c)/a)*((c*a)/b)=c^2
proof
((b*c)/a)*((c*a)/b) = ((b*c)*(c*a))/(a*b) by XCMPLX_1:76
.=((c*c)*(a*b))/(a*b)
.=(c*c)*((a*b)/(a*b)) by XCMPLX_1:74
.=(c*c)*1 by XCMPLX_1:60;
hence thesis;
end;
Lm15: 2*((b*c)/a)*((c*a)/b)+2*((b*c)/a)*((a*b)/c)+2*((c*a)/b)*((a*b)/c) =2*(a
^2+b^2+c^2)
proof
2*((b*c)/a)*((c*a)/b)+2*((b*c)/a)*((a*b)/c)+2*((c*a)/b)*((a*b)/c) =2*(((
b*c)/a)*((c*a)/b))+2*((b*c)/a)*((a*b)/c)+2*((c*a)/b)*((a*b)/c)
.=2*c^2+2*(((b*c)/a)*((a*b)/c))+2*((c*a)/b)*((a*b)/c) by Lm14
.=2*c^2+2*b^2+2*(((c*a)/b)*((a*b)/c)) by Lm14
.=2*c^2+2*b^2+2*a^2 by Lm14
.=2*(c^2+b^2+a^2);
hence thesis;
end;
Lm16: ((b*c)/a+(c*a)/b+(a*b)/c)^2=((c*a)/b)^2+((a*b)/c)^2+((b*c)/a)^2+ 2*(a^2+
b^2+c^2)
proof
((b*c)/a+(c*a)/b+(a*b)/c)^2 =((b*c)/a)^2+((c*a)/b)^2+((a*b)/c)^2+(2*((b*
c)/a)*((c*a)/b)+2*((b*c)/a) *((a*b)/c)+2*((c*a)/b)*((a*b)/c))
.=((b*c)/a)^2+((c*a)/b)^2+((a*b)/c)^2+2*(a^2+b^2+c^2) by Lm15;
hence thesis;
end;
Lm17: a+b+c = 1 implies 1/a-1=(b+c)/a
proof
assume a+b+c =1;
then 1/a-1 = (a+(b+c))/a-1 .=a/a+(b+c)/a-1 by XCMPLX_1:62
.=1+(b+c)/a-1 by XCMPLX_1:60;
hence thesis;
end;
Lm18: ((2*sqrt(b*c))/a)*((2*sqrt(a*c))/b)*((2*sqrt(a*b))/c) = 8
proof
((2*sqrt(b*c))/a)*((2*sqrt(a*c))/b)*((2*sqrt(a*b))/c) =(((2*sqrt(b*c))*(
2*sqrt(a*c)))/(a*b))*((2*sqrt(a*b))/c) by XCMPLX_1:76
.=((4*(sqrt(b*c)*sqrt(a*c)))/(a*b))*((2*sqrt(a*b))/c)
.=((4*sqrt((b*c)*(a*c)))/(a*b))*((2*sqrt(a*b))/c) by SQUARE_1:29
.=((4*sqrt(b*a*c^2))*(2*sqrt(a*b)))/((a*b)*c) by XCMPLX_1:76
.=(8*(sqrt(b*a*c^2)*sqrt(a*b)))/(a*b*c)
.=(8*sqrt((b*a*c^2)*(a*b)))/(a*b*c) by SQUARE_1:29
.=(8*sqrt((a*b*c)^2))/(a*b*c)
.=(8*(a*b*c))/(a*b*c) by SQUARE_1:22
.=8*((a*b*c)/(a*b*c)) by XCMPLX_1:74
.=8*1 by XCMPLX_1:60;
hence thesis;
end;
Lm19: a+b+c = 1 implies 1+1/a=2+(b+c)/a
proof
assume a+b+c =1;
then 1+1/a = 1+(a+(b+c))/a .=1+(a/a+(b+c)/a) by XCMPLX_1:62
.=1+a/a+(b+c)/a
.=1+1+(b+c)/a by XCMPLX_1:60;
hence thesis;
end;
Lm20: (1+sqrt(a*c)/b)*(sqrt(a*b)/c)=sqrt(a*b)/c+a/sqrt(b*c)
proof
A1: sqrt(b*c)>0 by SQUARE_1:25;
(1+sqrt(a*c)/b)*(sqrt(a*b)/c) =1*(sqrt(a*b)/c)+(sqrt(a*c)/b)*(sqrt(a*b)/ c)
.=sqrt(a*b)/c+(sqrt(a*c)*sqrt(a*b))/(b*c) by XCMPLX_1:76
.=sqrt(a*b)/c+(sqrt((a*c)*(a*b)))/(b*c) by SQUARE_1:29
.=sqrt(a*b)/c+(sqrt((a^2)*(c*b)))/(b*c)
.=sqrt(a*b)/c+(sqrt(a^2)*sqrt(c*b))/(b*c) by SQUARE_1:29
.=sqrt(a*b)/c+(sqrt(a^2)*sqrt(c*b))/(sqrt(b*c))^2 by SQUARE_1:def 2
.=sqrt(a*b)/c+(sqrt(a^2)/sqrt(b*c))*(sqrt(c*b)/sqrt(b*c)) by XCMPLX_1:76
.=sqrt(a*b)/c+(sqrt(a^2)/sqrt(b*c))*(1) by A1,XCMPLX_1:60
.=sqrt(a*b)/c+a/sqrt(b*c) by SQUARE_1:22;
hence thesis;
end;
Lm21: (sqrt(b*c)/a+c/sqrt(b*a))*(sqrt(a*b)/c) =b/sqrt(a*c)+1
proof
A1: sqrt(a*c)>0 by SQUARE_1:25;
A2: sqrt(a*b)>0 by SQUARE_1:25;
(sqrt(b*c)/a+c/sqrt(b*a))*(sqrt(a*b)/c) =(sqrt(b*c)/a)*(sqrt(a*b)/c)+(c/
sqrt(b*a))*(sqrt(a*b)/c)
.=((sqrt(b*c)*sqrt(a*b))/(a*c))+(c/sqrt(b*a))*(sqrt(a*b)/c) by XCMPLX_1:76
.=((sqrt((b*c)*(a*b)))/(a*c))+(c/sqrt(b*a))*(sqrt(a*b)/c) by SQUARE_1:29
.=((sqrt((a*c)*b^2))/(a*c))+(c/sqrt(b*a))*(sqrt(a*b)/c)
.=((sqrt(a*c)*sqrt(b^2))/(a*c))+(c/sqrt(b*a))*(sqrt(a*b)/c) by SQUARE_1:29
.=(sqrt(b^2)*sqrt(a*c))/(sqrt(a*c))^2+(c/sqrt(b*a))*(sqrt(a*b)/c) by
SQUARE_1:def 2
.=(sqrt(b^2)/sqrt(a*c))*(sqrt(a*c)/sqrt(a*c))+(c/sqrt(b*a))*(sqrt(a*b)/c
) by XCMPLX_1:76
.=(sqrt(b^2)/sqrt(a*c))*1+(c/sqrt(b*a))*(sqrt(a*b)/c) by A1,XCMPLX_1:60
.=b/sqrt(a*c)+(c/sqrt(b*a))*(sqrt(a*b)/c) by SQUARE_1:22
.=b/sqrt(a*c)+(c/c)*(sqrt(a*b)/sqrt(b*a)) by XCMPLX_1:85
.=b/sqrt(a*c)+1*(sqrt(a*b)/sqrt(b*a)) by XCMPLX_1:60
.=b/sqrt(a*c)+1 by A2,XCMPLX_1:60;
hence thesis;
end;
Lm22: (1+sqrt(b*c)/a)*(1+sqrt(a*c)/b)*(1+sqrt(a*b)/c) =2+sqrt(a*c)/b+b/sqrt(a*
c)+sqrt(a*b)/c+c/sqrt(b*a)+a/sqrt(b*c)+sqrt(b*c)/a
proof
A1: sqrt(b*a)>0 by SQUARE_1:25;
(1+sqrt(b*c)/a)*(1+sqrt(a*c)/b)*(1+sqrt(a*b)/c) =(1*1+1*(sqrt(a*c)/b)+(
sqrt(b*c)/a)*1+(sqrt(b*c)/a)*(sqrt(a*c)/b))* (1+sqrt(a*b)/c)
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(sqrt(b*c)*sqrt(a*c))/(a*b))* (1+sqrt(a*b)/
c) by XCMPLX_1:76
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(sqrt((b*c)*(a*c)))/(a*b) )* (1+sqrt(a*b)/c
) by SQUARE_1:29
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(sqrt(b*a*c^2))/(a*b) )* (1+sqrt(a*b)/c)
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(sqrt(b*a)*sqrt(c^2))/(a*b) )* (1+sqrt(a*b)
/c) by SQUARE_1:29
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(sqrt(b*a)*c)/(a*b) )* (1+sqrt(a*b)/c) by
SQUARE_1:22
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(sqrt(b*a)*c)/(sqrt(a*b))^2)* (1+sqrt(a*b)/
c) by SQUARE_1:def 2
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+((sqrt(b*a)/sqrt(b*a))*(c/sqrt(b*a))))* (1+
sqrt(a*b)/c) by XCMPLX_1:76
.=(1+sqrt(a*c)/b+sqrt(b*c)/a+(1*(c/sqrt(b*a))))* (1+sqrt(a*b)/c) by A1,
XCMPLX_1:60
.=1+sqrt(a*c)/b+(1+sqrt(a*c)/b)*(sqrt(a*b)/c)+sqrt(b*c)/a+c/sqrt(b*a) +(
sqrt(b*c)/a+c/sqrt(b*a))*(sqrt(a*b)/c)
.=1+sqrt(a*c)/b+(sqrt(a*b)/c+a/sqrt(b*c))+sqrt(b*c)/a+c/sqrt(b*a) +(sqrt
(b*c)/a+c/sqrt(b*a))*(sqrt(a*b)/c) by Lm20
.=1+sqrt(a*c)/b+sqrt(a*b)/c+a/sqrt(b*c)+sqrt(b*c)/a+c/sqrt(b*a) +(b/sqrt
(a*c)+1) by Lm21
.=2+sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/sqrt(b*a)+a/sqrt(b*c)+sqrt(b*c
)/a;
hence thesis;
end;
Lm23: sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/sqrt(b*a)+a/sqrt(b*c)+sqrt(b*c)/a
>=6
proof
sqrt(a*c)>0 by SQUARE_1:25;
then
A1: sqrt(a*c)/b+b/sqrt(a*c)>=2 by SERIES_3:3;
sqrt(b*c)>0 by SQUARE_1:25;
then
A2: a/sqrt(b*c)+sqrt(b*c)/a>=2 by SERIES_3:3;
sqrt(b*a)>0 by SQUARE_1:25;
then sqrt(a*b)/c+c/sqrt(b*a)>=2 by SERIES_3:3;
then sqrt(a*c)/b+b/sqrt(a*c)+(sqrt(a*b)/c+c/sqrt(b*a))>=2+2 by A1,XREAL_1:7;
then
sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/sqrt(b*a)+(a/sqrt(b*c)+sqrt(b*c) /
a) >=4+2 by A2,XREAL_1:7;
hence thesis;
end;
theorem
(a+b)*(1/a+1/b)>=4
proof
a/b+b/a>=2*sqrt((a/b)*(b/a)) by SIN_COS2:1;
then a/b+b/a>=2*sqrt((a*b)/(b*a)) by XCMPLX_1:76;
then a/b+b/a>=2*sqrt((a/b*b)/a) by XCMPLX_1:83;
then a/b+b/a>=2*sqrt(a/a) by XCMPLX_1:87;
then a/b+b/a>=2*1 by SQUARE_1:18,XCMPLX_1:60;
then (a/b+b/a)+2>=2+2 by XREAL_1:7;
then a/b+b/a+1+1>=4;
then a*(1/b)+b/a+1+1>=4 by XCMPLX_1:99;
then a*(1/b)+b*(1/a)+1+1>=4 by XCMPLX_1:99;
then a*(1/b)+b*(1/a)+a*(1/a)+1>=4 by XCMPLX_1:106;
then a*(1/b)+b*(1/a)+a*(1/a)+b*(1/b)>=4 by XCMPLX_1:106;
hence thesis;
end;
theorem
a|^4+b|^4>=a|^3*b+a*b|^3
proof
(a-b)^2>=0 by XREAL_1:63;
then ((a-b)*(a-b))*(a^2+a*b+b^2)>=0;
then (a-b)*((a-b)*(a^2+a*b+b^2))>=0;
then (a-b)*(a|^3-b|^3)>=0 by Lm1;
then a|^3*a-a|^3*b-b|^3*(a-b)>=0;
then a|^(3+1)-a|^3*b-b|^3*(a-b)>=0 by NEWTON:6;
then a|^4-a|^3*b-(b|^3*a-b|^3*b)>=0;
then a|^4-a|^3*b-(b|^3*a-b|^(3+1))>=0 by NEWTON:6;
then (a|^4+b|^4-a|^3*b-b|^3*a)+(a|^3*b+b|^3*a)>=0+(a|^3*b+b|^3*a) by
XREAL_1:7;
hence thesis;
end;
theorem Th3:
a<b implies 1<(b+c)/(a+c)
proof
assume a<b;
then a+c<b+c by XREAL_1:8;
hence thesis by XREAL_1:187;
end;
theorem Th4:
a<b implies a/b<sqrt(a/b)
proof
b^2>0;
then b|^2>0 by NEWTON:81;
then b|^2*b>0;
then
A1: b|^(2+1)>0 by NEWTON:6;
assume a<b;
then a-b<0 by XREAL_1:49;
then (a*b)*(a-b)<0;
then a^2*b-a*b^2+(a*b^2)<0+(a*b^2) by XREAL_1:8;
then (a^2*b)/(b|^(2+1))<(a*b^2)/(b|^(2+1)) by A1,XREAL_1:74;
then (a^2*b)/(b|^2*b)<(a*b^2)/(b|^(2+1)) by NEWTON:6;
then (a^2*b)/(b|^2*b)<(a*b^2)/(b|^2*b) by NEWTON:6;
then (a^2*b)/(b^2*b)<(a*b^2)/(b|^2*b) by NEWTON:81;
then (a^2*b)/(b^2*b)<(a*b^2)/(b^2*b) by NEWTON:81;
then a^2/b^2<(a*b^2)/(b*b^2) by XCMPLX_1:91;
then a^2/b^2<a/b by XCMPLX_1:91;
then (a/b)^2<a/b by XCMPLX_1:76;
then sqrt((a/b)^2)<sqrt(a/b) by SQUARE_1:27;
hence thesis by SQUARE_1:22;
end;
theorem Th5:
a<b implies sqrt(a/b)<(b+sqrt((a^2+b^2)/2))/(a+sqrt((a^2+b^2)/2))
proof
assume
A1: a<b;
then a/b<1 by XREAL_1:189;
then
A2: sqrt(a/b)<1 by SQUARE_1:18,27;
sqrt((a^2+b^2)/2)>0 by SQUARE_1:25;
then 1<(b+sqrt((a^2+b^2)/2))/(a+sqrt((a^2+b^2)/2)) by A1,Th3;
hence thesis by A2,XXREAL_0:2;
end;
theorem
a<b implies a/b<(b+sqrt((a^2+b^2)/2))/(a+sqrt((a^2+b^2)/2))
proof
assume
A1: a<b;
then
A2: sqrt(a/b)<(b+sqrt((a^2+b^2)/2))/(a+sqrt((a^2+b^2)/2)) by Th5;
a/b<sqrt(a/b) by A1,Th4;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th7:
2/((1/a)+(1/b))<=sqrt(a*b)
proof
A1: sqrt(a*b)>0 by SQUARE_1:25;
then (2*sqrt(a*b))/(a+b)<=1 by SIN_COS2:1,XREAL_1:183;
then ((2*sqrt(a*b))/(a+b))*sqrt(a*b)<=1*sqrt(a*b) by A1,XREAL_1:64;
then (2*sqrt(a*b))/((a+b)/sqrt(a*b))<=sqrt(a*b) by XCMPLX_1:82;
then ((2*sqrt(a*b))*sqrt(a*b))/(a+b)<=sqrt(a*b) by XCMPLX_1:77;
then (2*(sqrt(a*b))^2)/(a+b)<=sqrt(a*b);
then 2*(a*b)/(a+b)<=sqrt(a*b) by SQUARE_1:def 2;
hence thesis by Lm2;
end;
theorem Th8:
(a+b)/2<=sqrt((a^2+b^2)/2)
proof
a^2+b^2>=2*a*b by SERIES_3:6;
then (a^2+b^2)+(a^2+b^2)>=2*a*b+(a^2+b^2) by XREAL_1:7;
then sqrt(2*(a^2+b^2))>=sqrt((a+b)^2) by SQUARE_1:26;
then sqrt(2*(a^2+b^2))>=(a+b) by SQUARE_1:22;
then (sqrt(2*(a^2+b^2)))/sqrt(2*2)>=(a+b)/2 by SQUARE_1:20,XREAL_1:72;
then (sqrt(2*(a^2+b^2)))/(sqrt(2)*sqrt(2))>=(a+b)/2 by SQUARE_1:29;
then (sqrt(2)*sqrt(a^2+b^2))/(sqrt(2)*sqrt(2))>=(a+b)/2 by SQUARE_1:29;
then
A1: (sqrt(2)/sqrt(2)*sqrt(a^2+b^2))/sqrt(2)>=(a+b)/2 by XCMPLX_1:83;
sqrt(2)>0 by SQUARE_1:25;
then (1*sqrt(a^2+b^2))/sqrt(2)>=(a+b)/2 by A1,XCMPLX_1:60;
hence thesis by SQUARE_1:30;
end;
theorem
x+y<=sqrt(2*(x^2+y^2))
proof
x^2+y^2>=2*x*y by SERIES_3:6;
then
A1: x^2+y^2+(x^2+y^2)>=2*x*y+(x^2+y^2) by XREAL_1:6;
then
A2: 2*(x^2+y^2)>=(x+y)^2;
A3: (x+y)^2>=0 by XREAL_1:63;
then
A4: sqrt(2*(x^2+y^2))>=sqrt((x+y)^2) by A1,SQUARE_1:26;
per cases;
suppose
x+y>0;
hence thesis by A4,SQUARE_1:22;
end;
suppose
x+y=0;
hence thesis by A2,SQUARE_1:17,26;
end;
suppose
x+y<0;
hence thesis by A1,A3,SQUARE_1:def 2;
end;
end;
theorem Th10:
2/((1/a)+(1/b))<=(a+b)/2
proof
A1: (a+b)/2>=sqrt(a*b) by SERIES_3:2;
2/((1/a)+(1/b))<=sqrt(a*b) by Th7;
hence thesis by A1,XXREAL_0:2;
end;
theorem
sqrt(a*b)<=sqrt((a^2+b^2)/2)
proof
A1: (a+b)/2>=sqrt(a*b) by SERIES_3:2;
(a+b)/2<=sqrt((a^2+b^2)/2) by Th8;
hence thesis by A1,XXREAL_0:2;
end;
theorem
2/((1/a)+(1/b))<=sqrt((a^2+b^2)/2)
proof
A1: 2/((1/a)+(1/b))<=(a+b)/2 by Th10;
(a+b)/2<=sqrt((a^2+b^2)/2) by Th8;
hence thesis by A1,XXREAL_0:2;
end;
theorem
|.x.|<1 & |.y.|<1 implies |.(x+y)/(1+x*y).|<=1
proof
assume that
A1: |.x.|<1 and
A2: |.y.|<1;
per cases;
suppose
A3: 1+x*y<>0;
y^2<1 by A2,Lm7;
then
A4: y^2-y^2<1-y^2 by XREAL_1:14;
x^2<1 by A1,Lm7;
then x^2-x^2<1-x^2 by XREAL_1:14;
then 0<(1-x^2)*(1-y^2) by A4;
then 0+(x^2+y^2)<1-y^2-x^2+x^2*y^2+(x^2+y^2) by XREAL_1:8;
then
A5: x^2+y^2+2*x*y<1+x^2*y^2+2*x*y by XREAL_1:8;
(1+x*y)^2>0 by A3,SQUARE_1:12;
then (x+y)^2/(1+x*y)^2<(x*y+1)^2/(1+x*y)^2 by A5,XREAL_1:74;
then (x+y)^2/(1+x*y)^2<1 by A3,XCMPLX_1:60;
then ((x+y)/(1+x*y))^2<1 by XCMPLX_1:76;
hence thesis by Lm8;
end;
suppose
1+x*y=0;
then |.(x+y)/(1+x*y).|= |.0.| by XCMPLX_1:49
.=0 by ABSVALUE:2;
hence thesis;
end;
end;
theorem
|.x+y.|/(1+|.x+y.|)<=|.x.|/(1+|.x.|)+|.y.|/(1+|.y.|)
proof
per cases;
suppose
|.x+y.|=0;
hence thesis;
end;
suppose
A1: |.x+y.|>0;
1+|.y.|>=1 by XREAL_1:31;
then 1+|.y.|+|.x.|>=1+|.x.| by XREAL_1:6;
then
A2: |.x.|/(1+|.x.|+|.y.|)<=|.x.|/(1+|.x.|) by XREAL_1:118;
1+|.x.|>=1 by XREAL_1:31;
then 1+|.x.|+|.y.|>=1+|.y.| by XREAL_1:6;
then |.y.|/(1+|.x.|+|.y.|)<=|.y.|/(1+|.y.|) by XREAL_1:118;
then
A3: |.x.|/(1+|.x.|+|.y.|)+|.y.|/(1+|.x.|+|.y.|)<= |.x.|/(1+|.x.|)
+|.y.|/(1+|.y.|) by A2,XREAL_1:7;
1/(|.x.|+|.y.|)<=1/|.x+y.| by A1,COMPLEX1:56,XREAL_1:118;
then 1/(|.x.|+|.y.|)+1<=1/|.x+y.|+1 by XREAL_1:7;
then
A4: 1/(1/|.x+y.|+1)<=1/(1/(|.x.|+|.y.|)+1) by XREAL_1:118;
A5: 0<|.x.|+|.y.| by A1,COMPLEX1:56;
then
A6: 1/(1/(|.x.|+|.y.|)+1) =(1*(|.x.|+|.y.|))/((1/(|.x.|+|.y.|)+1)*(
|.x.|+|.y.|)) by XCMPLX_1:91
.=(|.x.|+|.y.|)/(1/(|.x.|+|.y.|)*(|.x.|+|.y.|)+(|.x.|+|.y.|))
.=(|.x.|+|.y.|)/(1+(|.x.|+|.y.|)) by A5,XCMPLX_1:87
.=|.x.|/(1+|.x.|+|.y.|)+|.y.|/(1+|.x.|+|.y.|) by XCMPLX_1:62;
|.x+y.|/(1+|.x+y.|) =(|.x+y.|/|.x+y.|)/((1+|.x+y.|)/|.x+y.|) by A1,
XCMPLX_1:55
.=1/((1+|.x+y.|)/|.x+y.|) by A1,XCMPLX_1:60
.=1/(1/|.x+y.|+|.x+y.|/|.x+y.|) by XCMPLX_1:62
.=1/(1/|.x+y.|+1) by A1,XCMPLX_1:60;
hence thesis by A4,A6,A3,XXREAL_0:2;
end;
end;
theorem
a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d)>1
proof
d+(a+b+c)>0+(a+b+c) by XREAL_1:8;
then
A1: b/(a+b+c+d)<b/(a+b+c) by XREAL_1:76;
(b+c+d)+a>0+(b+c+d) by XREAL_1:8;
then
A2: c/(b+c+d)>c/(a+b+c+d) by XREAL_1:76;
c+(a+b+d)>0+(a+b+d) by XREAL_1:8;
then a/(a+b+c+d)<a/(a+b+d) by XREAL_1:76;
then a/(a+b+c+d)+b/(a+b+c+d)<a/(a+b+d)+b/(a+b+c) by A1,XREAL_1:8;
then (a+b)/(a+b+c+d)<a/(a+b+d)+b/(a+b+c) by XCMPLX_1:62;
then (a+b)/(a+b+c+d)+c/(a+b+c+d)<(a/(a+b+d)+b/(a+b+c))+c/(b+c+d) by A2,
XREAL_1:8;
then
A3: (a+b+c)/(a+b+c+d)<(a/(a+b+d)+b/(a+b+c))+c/(b+c+d) by XCMPLX_1:62;
b+(a+c+d)>0+(a+c+d) by XREAL_1:8;
then d/(a+c+d)>d/(a+b+c+d) by XREAL_1:76;
then (a+b+c)/(a+b+c+d)+d/(a+b+c+d)<(a/(a+b+d)+b/(a+b+c))+c/(b+c+d)+d/(a+c+d
) by A3,XREAL_1:8;
then (a+b+c+d)/(a+b+c+d)<(a/(a+b+d)+b/(a+b+c))+c/(b+c+d)+d/(a+c+d) by
XCMPLX_1:62;
hence thesis by XCMPLX_1:60;
end;
theorem
a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d)<2
proof
A1: b/(a+b)>b/(a+b+c) by XREAL_1:29,76;
a/(a+b)>a/(a+b+d) by XREAL_1:29,76;
then a/(a+b)+b/(a+b)>a/(a+b+d)+b/(a+b+c) by A1,XREAL_1:8;
then (a+b)/(a+b)>a/(a+b+d)+b/(a+b+c) by XCMPLX_1:62;
then
A2: 1>a/(a+b+d)+b/(a+b+c) by XCMPLX_1:60;
a+(c+d)>c+d by XREAL_1:29;
then
A3: d/(c+d)>d/(a+c+d) by XREAL_1:76;
b+(c+d)>c+d by XREAL_1:29;
then c/(c+d)>c/(b+c+d) by XREAL_1:76;
then 1+c/(c+d)>a/(a+b+d)+b/(a+b+c)+c/(b+c+d) by A2,XREAL_1:8;
then (1+c/(c+d))+d/(c+d)>(a/(a+b+d)+b/(a+b+c)+c/(b+c+d))+d/(a+c+d) by A3,
XREAL_1:8;
then 1+(c/(c+d)+d/(c+d))>a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d);
then 1+(c+d)/(c+d)>a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d) by XCMPLX_1:62;
then 1+1>a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d) by XCMPLX_1:60;
hence thesis;
end;
theorem
a+b>c & b+c>a & a+c>b implies 1/(a+b-c)+1/(b+c-a)+1/(c+a-b)>=9/(a+b+c)
proof
assume that
A1: a+b>c and
A2: b+c>a and
A3: a+c>b;
A4: a+c-b>0 by A3,XREAL_1:50;
set f=c+a-b;
set e=b+c-a;
set d=a+b-c;
A5: b+c-a>0 by A2,XREAL_1:50;
A6: a+b-c>0 by A1,XREAL_1:50;
then
A7: d+e+f>=3*(3-root(d*e*f)) by A5,A4,SERIES_3:15;
1/d+1/e+1/f>=3*(3-root((1/d)*(1/e)*(1/f))) by A6,A5,A4,SERIES_3:15;
then
A8: 1/d+1/e+1/f>=3*(3-root((1/(d*e*f)))) by Lm3;
A9: 3-root(d*e*f)>=0 by A6,A5,A4,POWER:7;
3-root(1/(d*e*f))>=0 by A6,A5,A4,POWER:7;
then
(d+e+f)*(1/d+1/e+1/f)>=(3*(3-root(d*e*f)))*(3*(3-root((1/(d*e*f))))) by A7,A9
,A8,XREAL_1:66;
then (d+e+f)*(1/d+1/e+1/f)>=9*((3-root(d*e*f))*(3-root((1/(d*e*f)))));
then (d+e+f)*(1/d+1/e+1/f)>=9*(3-root((d*e*f)*(1/(d*e*f)))) by A6,A5,A4,
POWER:11;
then (d+e+f)*(1/d+1/e+1/f)>=9*(3-root((d*e*f)/((d*e*f)/1))) by XCMPLX_1:79;
then (d+e+f)*(1/d+1/e+1/f)>=9*(3-root(1)) by A6,A5,A4,XCMPLX_1:60;
then (d+e+f)*(1/d+1/e+1/f)>=9*1 by POWER:6;
hence thesis by XREAL_1:79;
end;
theorem
sqrt((a+b)*(c+d))>=sqrt(a*c)+sqrt(b*d)
proof
A1: sqrt((a+b)*(c+d))>0 by SQUARE_1:25;
A2: sqrt(b*d)>0 by SQUARE_1:25;
a*d+b*c>=2*sqrt((a*d)*(b*c)) by SIN_COS2:1;
then (a*d+b*c)+(a*c+b*d)>=2*sqrt((a*d)*(b*c))+(a*c+b*d) by XREAL_1:7;
then (a+b)*(c+d)>=2*sqrt((a*d)*(b*c))+a*c+b*d;
then (a+b)*(c+d)>=2*sqrt((a*d)*(b*c))+(sqrt(a*c))^2+b*d by SQUARE_1:def 2;
then (a+b)*(c+d)>=2*sqrt((a*d)*(b*c))+(sqrt(a*c))^2+(sqrt(b*d))^2 by
SQUARE_1:def 2;
then (sqrt((a+b)*(c+d)))^2>=2*sqrt((a*c)*(b*d))+(sqrt(a*c))^2+(sqrt(b*d))^2
by SQUARE_1:def 2;
then
A3: (sqrt((a+b)*(c+d)))^2>=(sqrt(a*c))^2+2*(sqrt(a*c)*sqrt(b*d))+(sqrt(b *d)
)^2 by SQUARE_1:29;
(sqrt(a*c)+sqrt(b*d))^2>=0 by XREAL_1:63;
then
A4: sqrt((sqrt((a+b)*(c+d)))^2)>=sqrt((sqrt(a*c)+sqrt(b*d))^2) by A3,
SQUARE_1:26;
sqrt(a*c)>0 by SQUARE_1:25;
then sqrt((sqrt((a+b)*(c+d)))^2)>=sqrt(a*c)+sqrt(b*d) by A4,A2,SQUARE_1:22;
hence thesis by A1,SQUARE_1:22;
end;
theorem
(a*b+c*d)*(a*c+b*d)>=4*a*b*c*d
proof
sqrt(a*d)>0 by SQUARE_1:25;
then (a+d)^2>=(2*sqrt(a*d))^2 by SIN_COS2:1,SQUARE_1:15;
then (a+d)^2>=2^2*(sqrt(a*d))^2;
then (a+d)^2>=2*2*(a*d) by SQUARE_1:def 2;
then
A1: (a+d)^2*(b*c)>=4*a*d*(b*c) by XREAL_1:64;
(a*b+c*d)*(a*c+b*d) =((sqrt(a*b))^2+c*d)*(a*c+b*d) by SQUARE_1:def 2
.=((sqrt(a*b))^2+(sqrt(c*d))^2)*(a*c+b*d) by SQUARE_1:def 2
.=((sqrt(a*b))^2+(sqrt(c*d))^2)*((sqrt(a*c))^2+b*d) by SQUARE_1:def 2
.=((sqrt(a*b))^2+(sqrt(c*d))^2)*((sqrt(a*c))^2+(sqrt(b*d))^2) by
SQUARE_1:def 2;
then (a*b+c*d)*(a*c+b*d)>=b*c*(a+d)^2 by Lm5;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th20:
a/b+b/c+c/a>=3
proof
a/b+b/c+c/a>=3*(3-root((a/b)*(b/c)*(c/a))) by SERIES_3:15;
then a/b+b/c+c/a>=3*(3-root(((a*b)/(b*c))*(c/a))) by XCMPLX_1:76;
then a/b+b/c+c/a>=3*(3-root((a/c)*(c/a))) by XCMPLX_1:91;
then a/b+b/c+c/a>=3*(3-root(((a*c)/(c*a)))) by XCMPLX_1:76;
then a/b+b/c+c/a>=3*(3-root(1)) by XCMPLX_1:60;
then a/b+b/c+c/a>=3*1 by POWER:6;
hence thesis;
end;
theorem
a*b+b*c+c*a=1 implies a+b+c>=sqrt 3
proof
assume
A1: a*b+b*c+c*a=1;
then a^2+b^2+c^2>=1 by SERIES_3:10;
then a^2+b^2+c^2+2>=1+2 by XREAL_1:6;
then sqrt((a+b+c)^2)>=sqrt(3) by A1,SQUARE_1:26;
hence thesis by SQUARE_1:22;
end;
theorem
(b+c-a)/a+(c+a-b)/b+(a+b-c)/c>=3
proof
A1: b/a+c/b+a/c>=3 by Th20;
a/b+b/c+c/a>=3 by Th20;
then (a/b+b/c+c/a)+(b/a+c/b+a/c)>=3+3 by A1,XREAL_1:7;
then
A2: (a/b+b/c+c/a+b/a+c/b+a/c)-3>=6-3 by XREAL_1:9;
(b+c-a)/a+(c+a-b)/b+(a+b-c)/c =(b+c)/a-a/a+(c+a-b)/b+(a+b-c)/c by
XCMPLX_1:120
.=(b+c)/a-1+(c+a-b)/b+(a+b-c)/c by XCMPLX_1:60
.=(b+c)/a-1+((c+a)/b-b/b)+(a+b-c)/c by XCMPLX_1:120
.=(b+c)/a-1+((c+a)/b-1)+(a+b-c)/c by XCMPLX_1:60
.=(b+c)/a-1+(c+a)/b-1+((a+b)/c-c/c) by XCMPLX_1:120
.=(b+c)/a-1+(c+a)/b-1+((a+b)/c-1) by XCMPLX_1:60
.=(b+c)/a+(c+a)/b+(a+b)/c-3
.=b/a+c/a+(c+a)/b+(a+b)/c-3 by XCMPLX_1:62
.=b/a+c/a+(c/b+a/b)+(a+b)/c-3 by XCMPLX_1:62
.=b/a+c/a+(c/b+a/b)+(a/c+b/c)-3 by XCMPLX_1:62
.=a/b+b/c+c/a+b/a+c/b+a/c-3;
hence thesis by A2;
end;
theorem
(a+1/a)*(b+1/b)>=(sqrt(a*b)+1/sqrt(a*b))^2
proof
A1: sqrt(a*b)>0 by SQUARE_1:25;
A2: (a+1/a)*(b+1/b)=a*b+a*(1/b)+(1/a)*b+(1/a)*(1/b)
.=a*b+(a*1)/b+(1/a)*b+(1/a)*(1/b) by XCMPLX_1:74
.=a*b+(a*1)/b+(b*1)/a+(1/a)*(1/b) by XCMPLX_1:74
.=a*b+(a*1)/b+(b*1)/a+(1*1)/(a*b) by XCMPLX_1:76
.=a*b+a/b+b/a+1/(a*b);
a/b+b/a>=2*sqrt((a/b)*(b/a)) by SIN_COS2:1;
then a/b+b/a>=2*sqrt((a*b)/(b*a)) by XCMPLX_1:76;
then a/b+b/a>=2*1 by SQUARE_1:18,XCMPLX_1:60;
then
A3: (a/b+b/a)+(a*b+1/(a*b))>=2+(a*b+1/(a*b)) by XREAL_1:6;
(sqrt(a*b)+1/sqrt(a*b))^2 =(sqrt(a*b))^2+2*sqrt(a*b)*(1/sqrt(a*b))+(1/
sqrt(a*b))^2
.=a*b+2*sqrt(a*b)*(1/sqrt(a*b))+(1/sqrt(a*b))^2 by SQUARE_1:def 2
.=a*b+2*sqrt(a*b)*(1/sqrt(a*b))+1^2/(sqrt(a*b))^2 by XCMPLX_1:76
.=a*b+2*(sqrt(a*b)*(1/sqrt(a*b)))+1/(a*b) by SQUARE_1:def 2
.=a*b+2*((sqrt(a*b)*1)/sqrt(a*b))+1/(a*b) by XCMPLX_1:74
.=a*b+2*(1)+1/(a*b) by A1,XCMPLX_1:60
.=a*b+2+1/(a*b);
hence thesis by A2,A3;
end;
theorem
(b*c)/a+(a*c)/b+(a*b)/c>=a+b+c
proof
A1: (a*c)/b+(a*b)/c = a*(c/b)+(a*b)/c by XCMPLX_1:74
.=a*(c/b)+a*(b/c) by XCMPLX_1:74
.=a*(c/b+b/c);
A2: (a*b)/c+(b*c)/a =b*(a/c)+(b*c)/a by XCMPLX_1:74
.=b*(a/c)+b*(c/a) by XCMPLX_1:74
.=b*(a/c+c/a);
A3: b*(a/c+c/a)>=b*2 by SERIES_3:3,XREAL_1:64;
A4: c*(b/a+a/b)>=c*2 by SERIES_3:3,XREAL_1:64;
a*(c/b+b/c)>=a*2 by SERIES_3:3,XREAL_1:64;
then a*(c/b+b/c)+b*(a/c+c/a)>=a*2+b*2 by A3,XREAL_1:7;
then
A5: a*(c/b+b/c)+b*(a/c+c/a)+c*(b/a+a/b)>=a*2+b*2+c*2 by A4,XREAL_1:7;
(b*c)/a+(a*c)/b = c*(b/a)+(a*c)/b by XCMPLX_1:74
.=c*(b/a)+c*(a/b) by XCMPLX_1:74
.=c*(b/a+a/b);
then (2*((b*c)/a+(a*c)/b+(a*b)/c))/2>=(2*(a+b+c))/2 by A1,A2,A5,XREAL_1:72;
hence thesis;
end;
theorem
x>y & y>z implies x^2*y+y^2*z+z^2*x>x*y^2+y*z^2+z*x^2
proof
assume that
A1: x>y and
A2: y>z;
A3: y-z>0 by A2,XREAL_1:50;
x>z by A1,A2,XXREAL_0:2;
then
A4: x-z>0 by XREAL_1:50;
x-y>0 by A1,XREAL_1:50;
then (x-y)*(y-z)*(x-z)>0 by A3,A4;
then (x^2*y+y^2*z+z^2*x)-(x*y^2+y*z^2+z*x^2)>0;
hence thesis by XREAL_1:47;
end;
theorem
a>b & b>c implies b/(a-b)>c/(a-c)
proof
assume that
A1: a>b and
A2: b>c;
A3: a-b>0 by A1,XREAL_1:50;
b*(-1)<c*(-1) by A2,XREAL_1:69;
then -b+a<-c+a by XREAL_1:8;
then
A4: c/(a-b)>c/(a-c) by A3,XREAL_1:76;
b/(a-b)>c/(a-b) by A2,A3,XREAL_1:74;
hence thesis by A4,XXREAL_0:2;
end;
theorem
b>a & c>d implies c/(c+a)>d/(d+b)
proof
assume that
A1: b>a and
A2: c>d;
b*c>a*d by A1,A2,XREAL_1:96;
then b*c+c*d>a*d+c*d by XREAL_1:8;
then c*(b+d)>d*(a+c);
hence thesis by XREAL_1:106;
end;
theorem
m*x+z*y<=sqrt(m^2+z^2)*sqrt(x^2+y^2)
proof
A1: z^2>=0 by XREAL_1:63;
A2: m^2>=0 by XREAL_1:63;
then
A3: sqrt(m^2+z^2)>=0 by A1,SQUARE_1:def 2;
A4: (m*x+z*y)^2>=0 by XREAL_1:63;
(m*y)^2+(z*x)^2>=2*(m*y)*(z*x) by SERIES_3:6;
then
A5: (m*y)^2+(z*x)^2+(m^2*x^2+z^2*y^2)>=2*m*x*y*z+(m^2*x^2+z^2*y^2) by XREAL_1:6
;
A6: y^2>=0 by XREAL_1:63;
A7: x^2>=0 by XREAL_1:63;
then
A8: sqrt(x^2+y^2)>=0 by A6,SQUARE_1:def 2;
(sqrt(m^2+z^2)*sqrt(x^2+y^2))^2 =(sqrt(m^2+z^2))^2*(sqrt(x^2+y^2))^2
.=(m^2+z^2)*(sqrt(x^2+y^2))^2 by A2,A1,SQUARE_1:def 2
.=(m^2+z^2)*(x^2+y^2) by A7,A6,SQUARE_1:def 2
.=m^2*x^2+(m*y)^2+(z*x)^2+z^2*y^2;
then sqrt((sqrt(m^2+z^2)*sqrt(x^2+y^2))^2)>=sqrt((m*x+z*y)^2) by A5,A4,
SQUARE_1:26;
then
A9: sqrt(m^2+z^2)*sqrt(x^2+y^2)>=sqrt((m*x+z*y)^2) by A3,A8,SQUARE_1:22;
per cases;
suppose
m*x+z*y>0;
hence thesis by A9,SQUARE_1:22;
end;
suppose
m*x+z*y=0;
hence thesis by A3,A8;
end;
suppose
m*x+z*y<0;
hence thesis by A3,A8;
end;
end;
theorem Th29:
(m*x+u*y+w*z)^2<=(m^2+u^2+w^2)*(x^2+y^2+z^2)
proof
m^2*z^2+w^2*x^2=(m*z)^2+(w*x)^2;
then
A1: m^2*z^2+w^2*x^2>=2*(m*z)*(w*x) by SERIES_3:6;
u^2*z^2+w^2*y^2=(u*z)^2+(w*y)^2;
then
A2: u^2*z^2+w^2*y^2>=2*(u*z)*(w*y) by SERIES_3:6;
(m*y)^2+(u*x)^2>=2*(m*y)*(u*x) by SERIES_3:6;
then m^2*y^2+u^2*x^2+(m^2*z^2+w^2*x^2)>=2*m*y*u*x+2*m*z*w*x by A1,XREAL_1:7;
then
m^2*y^2+u^2*x^2+m^2*z^2+w^2*x^2+(u^2*z^2+w^2*y^2)>=2*m*y*u*x+2*m*z*w *x+
2*u*z*w*y by A2,XREAL_1:7;
then
m^2*y^2+u^2*x^2+m^2*z^2+w^2*x^2+(u^2*z^2)+(w^2*y^2)+((m*x)^2+(u*y)^2+ (w
*z)^2)>=2*m*y*u*x+2*m*z*w*x+2*u*z*w*y+((m*x)^2+(u*y)^2+(w*z)^2) by XREAL_1:6;
hence thesis;
end;
theorem
(9*a*b*c)/(a^2+b^2+c^2)<=a+b+c
proof
A1: b^2*(a+c)>=b^2*(2*sqrt(a*c)) by SIN_COS2:1,XREAL_1:64;
A2: c^2*(a+b)>=c^2*(2*sqrt(a*b)) by SIN_COS2:1,XREAL_1:64;
A3: sqrt(a*b)>0 by SQUARE_1:25;
A4: sqrt(a*c)>0 by SQUARE_1:25;
sqrt(b*c)>0 by SQUARE_1:25;
then
2*a^2*sqrt(b*c)+2*b^2*sqrt(a*c)+2*c^2*sqrt(a*b)>= 3*(3-root((2*a^2*sqrt
(b*c)) *(2*b^2*sqrt(a*c))*(2*c^2*sqrt(a*b)))) by A4,A3,SERIES_3:15;
then
2*a^2*sqrt(b*c)+2*b^2*sqrt(a*c)+2*c^2*sqrt(a*b)>= 3*(3-root(2*a^2*sqrt(
b*c) *2*b^2*sqrt(a*c)*2*c^2*sqrt(a*b)));
then
2*a^2*sqrt(b*c)+2*b^2*sqrt(a*c)+2*c^2*sqrt(a*b)>= 3*(3-root((2*a*b*c)|^
3)) by Lm9;
then
A5: 2*a^2*sqrt(b*c)+2*b^2*sqrt(a*c)+2*c^2*sqrt(a*b)>= 3*(2*a*b*c) by POWER:4;
A6: a|^3+b|^3+c|^3>=3*a*b*c by SERIES_3:12;
a^2*(b+c)>=a^2*(2*sqrt(b*c)) by SIN_COS2:1,XREAL_1:64;
then a^2*(b+c)+b^2*(a+c)>=a^2*(2*sqrt(b*c))+b^2*(2*sqrt(a*c)) by A1,XREAL_1:7
;
then a^2*(b+c)+b^2*(a+c)+c^2*(a+b)>=2*a^2*sqrt(b*c)+2*b^2*sqrt(a*c)+ 2*c^2*
sqrt(a*b) by A2,XREAL_1:7;
then a*b^2+a*c^2+b*a^2+b*c^2+(c*a^2)+(c*b^2)>=6*a*b*c by A5,XXREAL_0:2;
then
A7: (a|^3+b|^3+c|^3)+(a*b^2+a*c^2+b*a^2+b*c^2+(c*a^2)+(c*b^2))>=3*a*b*c +6*
a*b*c by A6,XREAL_1:7;
(a^2+b^2+c^2)*(a+b+c) =a*a^2+a*b^2+a*c^2+b*a^2+b*b^2+b*c^2+(c*a^2)+(c*b
^2)+(c*c^2)
.=a*a|^2+a*b^2+a*c^2+b*a^2+b*b^2+b*c^2+(c*a^2)+(c*b^2)+(c*c^2) by NEWTON:81
.=a|^(2+1)+a*b^2+a*c^2+b*a^2+b*b^2+b*c^2+(c*a^2)+(c*b^2)+(c*c^2) by
NEWTON:6
.=a|^3+a*b^2+a*c^2+b*a^2+b*b|^2+b*c^2+(c*a^2)+(c*b^2)+(c*c^2) by NEWTON:81
.=a|^3+a*b^2+a*c^2+b*a^2+b|^(2+1)+b*c^2+(c*a^2)+(c*b^2)+(c*c^2) by NEWTON:6
.=a|^3+a*b^2+a*c^2+b*a^2+b|^3+b*c^2+(c*a^2)+(c*b^2)+(c*c|^2) by NEWTON:81
.=a|^3+a*b^2+a*c^2+b*a^2+b|^3+b*c^2+(c*a^2)+(c*b^2)+(c|^(2+1)) by NEWTON:6
.=a|^3+b|^3+c|^3+a*b^2+a*c^2+b*a^2+b*c^2+(c*a^2)+(c*b^2);
then ((a+b+c)*(a^2+b^2+c^2))/(a^2+b^2+c^2)>=(9*a*b*c)/(a^2+b^2+c^2) by A7,
XREAL_1:72;
then (a+b+c)/((a^2+b^2+c^2)/(a^2+b^2+c^2))>=(9*a*b*c)/(a^2+b^2+c^2) by
XCMPLX_1:77;
then (a+b+c)/1>=(9*a*b*c)/(a^2+b^2+c^2) by XCMPLX_1:60;
hence thesis;
end;
theorem
a+b+c<=sqrt((a^2+a*b+b^2)/3)+sqrt((b^2+b*c+c^2)/3)+sqrt((c^2+c*a+a^2)/ 3)
proof
A1: sqrt(3)>0 by SQUARE_1:25;
A2: sqrt(c^2+c*a+a^2)>=(1/2)*sqrt(3)*(c+a) by Lm11;
A3: sqrt(b^2+b*c+c^2)>=(1/2)*sqrt(3)*(b+c) by Lm11;
sqrt(a^2+a*b+b^2)>=(1/2)*sqrt(3)*(a+b) by Lm11;
then
sqrt(a^2+a*b+b^2)+sqrt(b^2+b*c+c^2)>=(1/2)*sqrt(3)*(a+b)+(1/2)*sqrt( 3)*
(b+c) by A3,XREAL_1:7;
then
sqrt(a^2+a*b+b^2)+sqrt(b^2+b*c+c^2)+sqrt(c^2+c*a+a^2)>=(1/2)*sqrt(3)*( a
+b)+ (1/2)*sqrt(3)*(b+c)+(1/2)*sqrt(3)*(c+a) by A2,XREAL_1:7;
then
(sqrt(a^2+a*b+b^2)+sqrt(b^2+b*c+c^2)+sqrt(c^2+c*a+a^2))/sqrt(3)>=((a+b +
c)* sqrt(3))/sqrt(3) by A1,XREAL_1:72;
then
(sqrt(a^2+a*b+b^2)+sqrt(b^2+b*c+c^2)+sqrt(c^2+c*a+a^2))/sqrt(3)>=(a+b+ c
)* (sqrt(3)/sqrt(3)) by XCMPLX_1:74;
then
(sqrt(a^2+a*b+b^2)+sqrt(b^2+b*c+c^2)+sqrt(c^2+c*a+a^2))/sqrt(3)>=(a+b+ c
)*1 by A1,XCMPLX_1:60;
then (sqrt(a^2+a*b+b^2)+sqrt(b^2+b*c+c^2))/sqrt(3)+sqrt(c^2+c*a+a^2)/sqrt(3
) >=a+b+c by XCMPLX_1:62;
then
sqrt(a^2+a*b+b^2)/sqrt(3)+sqrt(b^2+b*c+c^2)/sqrt(3)+sqrt(c^2+c*a+a^2 )/
sqrt(3)>=a+b+c by XCMPLX_1:62;
then
sqrt((a^2+a*b+b^2)/3)+sqrt(b^2+b*c+c^2)/sqrt(3)+sqrt(c^2+c*a+a^2)/ sqrt
(3)>=a+b+c by SQUARE_1:30;
then sqrt((a^2+a*b+b^2)/3)+sqrt((b^2+b*c+c^2)/3)+sqrt(c^2+c*a+a^2)/ sqrt(3)
>=a+b+c by SQUARE_1:30;
hence thesis by SQUARE_1:30;
end;
theorem
sqrt((a^2+a*b+b^2)/3)+sqrt((b^2+b*c+c^2)/3)+sqrt((c^2+c*a+a^2)/3) <=
sqrt((a^2+b^2)/2)+sqrt((b^2+c^2)/2)+sqrt((c^2+a^2)/2)
proof
A1: sqrt((b^2+b*c+c^2)/3)<=sqrt((b^2+c^2)/2) by Lm12;
A2: sqrt((c^2+c*a+a^2)/3)<=sqrt((c^2+a^2)/2) by Lm12;
sqrt((a^2+a*b+b^2)/3)<=sqrt((a^2+b^2)/2) by Lm12;
then
sqrt((a^2+a*b+b^2)/3)+sqrt((b^2+b*c+c^2)/3)<=sqrt((a^2+b^2)/2)+sqrt ((b
^2+c^2)/2) by A1,XREAL_1:7;
hence thesis by A2,XREAL_1:7;
end;
theorem
sqrt((a^2+b^2)/2)+sqrt((b^2+c^2)/2)+sqrt((c^2+a^2)/2) <=sqrt(3*(a^2+b
^2+c^2))
proof
A1: (sqrt((a^2+b^2)/2))^2=(a^2+b^2)/2 by SQUARE_1:def 2;
A2: (sqrt((b^2+c^2)/2))^2=(b^2+c^2)/ 2 by SQUARE_1:def 2;
A3: sqrt((c^2+a^2)/2)>0 by SQUARE_1:25;
A4: sqrt((b^2+c^2)/2)>0 by SQUARE_1:25;
A5: (sqrt((a^2+b^2)/2)+sqrt((b^2+c^2)/2)+sqrt((c^2+a^2)/2))^2>=0 by XREAL_1:63;
A6: sqrt((a^2+b^2)/2)>0 by SQUARE_1:25;
A7: (sqrt((c^2+a^2)/2))^2=(c^2+a^2)/2 by SQUARE_1:def 2;
(1*sqrt((a^2+b^2)/2)+1*sqrt((b^2+c^2)/2)+1*sqrt((c^2+a^2)/2))^2 <=(1^2+1
^2+1^2)*((sqrt((a^2+b^2)/2))^2+(sqrt((b^2+c^2)/2))^2+ (sqrt((c^2+a^2)/2))^2)
by Th29;
then
sqrt((sqrt((a^2+b^2)/2)+sqrt((b^2+c^2)/2)+sqrt((c^2+a^2)/2))^2)<= sqrt(
3*(a^2+b^2+c^2)) by A1,A2,A7,A5,SQUARE_1:26;
hence thesis by A6,A4,A3,SQUARE_1:22;
end;
theorem
sqrt(3*(a^2+b^2+c^2))<=(b*c)/a+(c*a)/b+(a*b)/c
proof
A1: ((b*c)/a)^2+((c*a)/b)^2>=2*c^2 by Lm13;
A2: ((c*a)/b)^2+((a*b)/c)^2>=2*a^2 by Lm13;
((b*c)/a)^2+((a*b)/c)^2>=2*b^2 by Lm13;
then (((c*a)/b)^2+((a*b)/c)^2)+(((b*c)/a)^2+((a*b)/c)^2)>=2*a^2+2*b^2 by A2,
XREAL_1:7;
then ((c*a)/b)^2+((a*b)/c)^2+((b*c)/a)^2+((a*b)/c)^2+(((b*c)/a)^2+((c*a)/b)
^2)>= 2*a^2+2*b^2+2*c^2 by A1,XREAL_1:7;
then ((((c*a)/b)^2+((a*b)/c)^2+((b*c)/a)^2)*2)/2>=((a^2+b^2+c^2)*2)/2 by
XREAL_1:72;
then
((c*a)/b)^2+((a*b)/c)^2+((b*c)/a)^2+2*(a^2+b^2+c^2)>=(a^2+b^2+c^2)+ 2*(a
^2+b^2+c^2) by XREAL_1:6;
then ((b*c)/a+(c*a)/b+(a*b)/c)^2>=3*(a^2+b^2+c^2) by Lm16;
then sqrt(((b*c)/a+(c*a)/b+(a*b)/c)^2)>=sqrt(3*(a^2+b^2+c^2)) by SQUARE_1:26;
hence thesis by SQUARE_1:22;
end;
theorem
a+b=1 implies (1/a^2-1)*(1/b^2-1)>=9
proof
assume
A1: a+b=1;
sqrt(a*b)>0 by SQUARE_1:25;
then 1^2>=(2*sqrt(a*b))^2 by A1,SIN_COS2:1,SQUARE_1:15;
then 1>=2*2*(sqrt(a*b))^2;
then 1>=4*(a*b) by SQUARE_1:def 2;
then 8/1<=8/(4*a*b) by XREAL_1:118;
then 8<=8/(4*(a*b));
then 8<=8/4/(a*b) by XCMPLX_1:78;
then
A2: 8+1<=2/(a*b)+1 by XREAL_1:7;
(1/a^2-1)*(1/b^2-1) =(1-1*a^2)/a^2*(1/b^2-1) by XCMPLX_1:126
.=(1-1*a^2)/a^2*((1-1*b^2)/b^2) by XCMPLX_1:126
.=((1-a)*(1+a)*((1-b)*(1+b)))/(a^2*b^2) by XCMPLX_1:76;
then (1/a^2-1)*(1/b^2-1) =((a*b)*((1+a)*(1+b)))/((a*b)*(a*b)) by A1
.=((a*b)/(a*b))*(((1+a)*(1+b))/(a*b)) by XCMPLX_1:76
.=1*(((1+a)*(1+b))/(a*b)) by XCMPLX_1:60
.=(1+(a+b)+a*b)/(a*b)
.=2/(a*b)+(a*b)/(a*b) by A1,XCMPLX_1:62
.=2/(a*b)+1 by XCMPLX_1:60;
hence thesis by A2;
end;
theorem
a+b=1 implies a*b+1/(a*b)>=17/4
proof
A1: sqrt(a*b)>0 by SQUARE_1:25;
assume a+b=1;
then 1^2>=(2*sqrt(a*b))^2 by A1,SIN_COS2:1,SQUARE_1:15;
then 1>=2*2*(sqrt(a*b))^2;
then 1>=4*(a*b) by SQUARE_1:def 2;
then
A2: 1/4>=((a*b)*4)/4 by XREAL_1:72;
then 1/4*(-1)<=a*b*(-1) by XREAL_1:65;
then -(1/4)+1<=-(a*b)+1 by XREAL_1:7;
then (3/4)^2<=(1-(a*b))^2 by SQUARE_1:15;
then (9/4^2)/(1/4)<=((1-(a*b))^2)/(1/4) by XREAL_1:72;
then
A3: 9/4+8/4<=((1-(a*b))^2)*4+2 by XREAL_1:7;
(1-a*b)^2>=0 by XREAL_1:63;
then (1-a*b)^2/(1/4)<=(1-a*b)^2/(a*b) by A2,XREAL_1:118;
then
A4: (1-a*b)^2*4+2<=(1-a*b)^2/(a*b)+2 by XREAL_1:7;
1/(a*b)+a*b =(1+(a*b)*(a*b))/(a*b) by XCMPLX_1:113
.=((1^2-2*1*(a*b)+(a*b)^2)+2*(a*b))/(a*b)
.=(1-a*b)^2/(a*b)+(2*(a*b))/(a*b) by XCMPLX_1:62
.=(1-a*b)^2/(a*b)+2*((a*b)/(a*b)) by XCMPLX_1:74
.=(1-a*b)^2/(a*b)+2*1 by XCMPLX_1:60
.=(1-a*b)^2/(a*b)+2;
hence thesis by A4,A3,XXREAL_0:2;
end;
theorem
a+b+c = 1 implies 1/a+1/b+1/c>=9
proof
assume
A1: a+b+c = 1;
A2: 3-root(a*b*c)>=0 by POWER:7;
1/a+1/b+1/c>=3*(3-root((1/a)*(1/b)*(1/c))) by SERIES_3:15;
then
A3: 1/a+1/b+1/c>=3*(3-root((1/(a*b*c)))) by Lm3;
A4: 3-root((1/(a*b*c)))>=0 by POWER:7;
a+b+c>=3*(3-root(a*b*c)) by SERIES_3:15;
then
(a+b+c)*(1/a+1/b+1/c)>=(3*(3-root(a*b*c)))*(3*(3-root((1/(a*b*c))))) by A2,A3
,A4,XREAL_1:66;
then (1/a+1/b+1/c)>=9*((3-root(a*b*c))*(3-root((1/(a*b*c))))) by A1;
then (1/a+1/b+1/c)>=9*(3-root((a*b*c)*(1/(a*b*c)))) by POWER:11;
then (1/a+1/b+1/c)>=9*(3-root((a*b*c)/((a*b*c)/1))) by XCMPLX_1:79;
then (1/a+1/b+1/c)>=9*(3-root(1)) by XCMPLX_1:60;
then (1/a+1/b+1/c)>=9*1 by POWER:6;
hence thesis;
end;
theorem
a+b+c = 1 implies (1/a-1)*(1/b-1)*(1/c-1)>=8
proof
A1: (a+c)/b>=(2*sqrt(a*c))/b by SIN_COS2:1,XREAL_1:72;
A2: (a+b)/c>=(2*sqrt(a*b))/c by SIN_COS2:1,XREAL_1:72;
A3: sqrt(a*b)>0 by SQUARE_1:25;
A4: sqrt(a*c)>0 by SQUARE_1:25;
assume
A5: a+b+c =1;
then
A6: (1/a-1)*(1/b-1)*(1/c-1) =((b+c)/a)*(1/b-1)*(1/c-1) by Lm17
.=((b+c)/a)*((a+c)/b)*(1/c-1) by A5,Lm17
.=((b+c)/a)*((a+c)/b)*((a+b)/c+c/c-1) by A5,XCMPLX_1:62
.=((b+c)/a)*((a+c)/b)*((a+b)/c+1-1) by XCMPLX_1:60
.=((b+c)/a)*((a+c)/b)*((a+b)/c);
A7: sqrt(b*c)>0 by SQUARE_1:25;
(b+c)/a>=(2*sqrt(b*c))/a by SIN_COS2:1,XREAL_1:72;
then ((b+c)/a)*((a+c)/b)>=((2*sqrt(b*c))/a)*((2*sqrt(a*c))/b) by A1,A7,A4,
XREAL_1:66;
then
(1/a-1)*(1/b-1)*(1/c-1)>=((2*sqrt(b*c))/a)*((2*sqrt(a*c))/b)* ((2*sqrt(
a*b))/c) by A6,A2,A7,A4,A3,XREAL_1:66;
hence thesis by Lm18;
end;
theorem
a+b+c = 1 implies (1+1/a)*(1+1/b)*(1+1/c)>=64
proof
A1: sqrt(b*c)>0 by SQUARE_1:25;
(a+b)/c>=(2*sqrt(a*b))/c by SIN_COS2:1,XREAL_1:72;
then 2+(a+b)/c>=2+(2*sqrt(a*b))/c by XREAL_1:6;
then
A2: 2+(a+b)/c>=2+2*(sqrt(a*b)/c) by XCMPLX_1:74;
A3: sqrt(a*b)>0 by SQUARE_1:25;
(a+c)/b>=(2*sqrt(a*c))/b by SIN_COS2:1,XREAL_1:72;
then 2+(a+c)/b>=2+(2*sqrt(a*c))/b by XREAL_1:6;
then
A4: 2+(a+c)/b>=2+2*(sqrt(a*c)/b) by XCMPLX_1:74;
A5: sqrt(a*c)>0 by SQUARE_1:25;
(b+c)/a>=(2*sqrt(b*c))/a by SIN_COS2:1,XREAL_1:72;
then 2+(b+c)/a>=2+(2*sqrt(b*c))/a by XREAL_1:6;
then 2+(b+c)/a>=2+2*(sqrt(b*c)/a) by XCMPLX_1:74;
then (2+(b+c)/a)*(2+(a+c)/b)>=(2*(1+sqrt(b*c)/a))*(2*(1+sqrt(a*c)/b)) by A4
,A1,A5,XREAL_1:66;
then
A6: (2+(b+c)/a)*(2+(a+c)/b)*(2+(a+b)/c)>=(2*(1+sqrt(b*c)/a))*(2*(1+sqrt(a*
c)/b)) *(2*(1+sqrt(a*b)/c)) by A2,A1,A5,A3,XREAL_1:66;
sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/sqrt(b*a)+a/sqrt(b*c)+sqrt(b*c)/a
>=6 by Lm23;
then 2+(sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/sqrt(b*a)+a/sqrt(b*c)+sqrt(b*
c)/a) >=6+2 by XREAL_1:6;
then
A7: 8*(2+sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/sqrt(b*a)+a/sqrt(b*c)+ sqrt(
b*c)/a)>=8*8 by XREAL_1:64;
assume
A8: a+b+c = 1;
then (1+1/a)*(1+1/b)*(1+1/c) =(2+(b+c)/a)*(1+1/b)*(1+1/c) by Lm19
.=(2+(b+c)/a)*(2+(a+c)/b)*(1+1/c) by A8,Lm19
.=(2+(b+c)/a)*(2+(a+c)/b)*(1+((a+b)/c+c/c)) by A8,XCMPLX_1:62
.=(2+(b+c)/a)*(2+(a+c)/b)*(1+(a+b)/c+1) by XCMPLX_1:60
.=(2+(b+c)/a)*(2+(a+c)/b)*(2+(a+b)/c);
then
(1+1/a)*(1+1/b)*(1+1/c)>=8*((1+sqrt(b*c)/a)*(1+sqrt(a*c)/b) *(1+sqrt(a*
b)/c)) by A6;
then (1+1/a)*(1+1/b)*(1+1/c)>=8* (2+sqrt(a*c)/b+b/sqrt(a*c)+sqrt(a*b)/c+c/
sqrt(b*a)+a/sqrt(b*c)+sqrt(b*c)/a) by Lm22;
hence thesis by A7,XXREAL_0:2;
end;
theorem
x+y+z=1 implies x^2+y^2+z^2>=1/3
proof
A1: (y^2+z^2)/2>=y*z by SERIES_3:7;
A2: (x^2+z^2)/2>=x*z by SERIES_3:7;
(x^2+y^2)/2>=x*y by SERIES_3:7;
then (x^2+y^2)/2+(y^2+z^2)/2>=y*z+x*y by A1,XREAL_1:7;
then (x^2+y^2)/2+(y^2+z^2)/2+(x^2+z^2)/2>=y*z+x*y+x*z by A2,XREAL_1:7;
then -((x^2+y^2)/2+(y^2+z^2)/2+(x^2+z^2)/2)<=-(y*z+x*y+x*z) by XREAL_1:24;
then (-((x^2+y^2)/2+(y^2+z^2)/2+(x^2+z^2)/2))*2<=(-(y*z+x*y+x*z))*2 by
XREAL_1:64;
then -((x^2+y^2)/2+(y^2+z^2)/2+(x^2+z^2)/2)*2+1<=-(y*z+x*y+x*z)*2+1 by
XREAL_1:6;
then
A3: 1-(x^2+y^2+z^2)*2<=1-(y*z+x*y+x*z)*2;
assume x+y+z=1;
then x^2+y^2+z^2+2*x*y+2*y*z+2*z*x=1^2 by Lm6;
then 1<=(x^2+y^2+z^2)+(x^2+y^2+z^2)*2 by A3,XREAL_1:20;
then 1/3<=((x^2+y^2+z^2)*3)/3 by XREAL_1:72;
hence thesis;
end;
theorem
x+y+z=1 implies x*y+y*z+z*x<=1/3
proof
x^2+y^2+z^2>=x*y+y*z+x*z by SERIES_3:10;
then
A1: (x^2+y^2+z^2)+2*(x*y+y*z+z*x)>=(x*y+y*z+x*z)+2*(x*y+y*z+z*x) by XREAL_1:7;
assume x+y+z=1;
then 1^2=x^2+y^2+z^2+2*x*y+2*y*z+2*z*x by Lm6;
then 1/3>=(3*(x*y+y*z+z*x))/3 by A1,XREAL_1:72;
hence thesis;
end;
theorem
a>b & b>c implies (a to_power (2*a))*(b to_power (2*b))*(c to_power (2
*c)) > (a to_power (b+c))*(b to_power (a+c))*(c to_power (a+b))
proof
assume that
A1: a>b and
A2: b>c;
A3: b/c>1 by A2,XREAL_1:187;
set e=(a to_power (b+c))*(b to_power (a+c))*(c to_power (a+b));
A4: b to_power (c+a)>0 by POWER:34;
b-c>0 by A2,XREAL_1:50;
then
A5: (b/c) to_power (b-c) > 1 by A3,POWER:35;
A6: a/b>1 by A1,XREAL_1:187;
a-b>0 by A1,XREAL_1:50;
then (a/b) to_power (a-b) > 1 by A6,POWER:35;
then
A7: ((a/b) to_power (a-b))*((b/c) to_power (b-c)) > 1 by A5,XREAL_1:161;
A8: c to_power (a+b)>0 by POWER:34;
A9: a>c by A1,A2,XXREAL_0:2;
then
A10: a/c>1 by XREAL_1:187;
set d=(a to_power (2*a))*(b to_power (2*b))*(c to_power (2*c));
A11: a to_power (b+c)>0 by POWER:34;
a-c>0 by A9,XREAL_1:50;
then (a/c) to_power (a-c) > 1 by A10,POWER:35;
then ((a/b) to_power (a-b))*((b/c) to_power (b-c)) *((a/c) to_power -(c-a))
>1 by A7,XREAL_1:161;
then
((a/b) to_power (a-b))*((b/c) to_power (b-c)) *((c/a) to_power (c-a)) >
1 by Lm4;
then (a to_power (a-b)/b to_power (a-b))*((b/c) to_power (b-c)) *((c/a)
to_power (c-a)) >1 by POWER:31;
then (a to_power (a-b)/b to_power (a-b))*(b to_power (b-c)/c to_power (b-c)
) *((c/a) to_power (c-a)) >1 by POWER:31;
then (a to_power (a-b)/b to_power (a-b))*(b to_power (b-c)/c to_power (b-c)
) *(c to_power (c-a)/a to_power (c-a)) >1 by POWER:31;
then
((a to_power (a-b))*(b to_power (b-c)))/((c to_power (b-c))*(b to_power
( a-b))) *(c to_power (c-a)/a to_power (c-a)) >1 by XCMPLX_1:76;
then
((a to_power (a-b))/(c to_power (b-c)))*((b to_power (b-c))/(b to_power
( a-b))) *(c to_power (c-a)/a to_power (c-a)) >1 by XCMPLX_1:76;
then ((a to_power (a-b))/(c to_power (b-c)))*(b to_power ((b-c)-(a-b))) *(c
to_power (c-a)/a to_power (c-a)) >1 by POWER:29;
then
((a to_power (a-b))/(c to_power (b-c)))*(c to_power (c-a)/a to_power (c
-a)) *(b to_power (2*b-a-c)) >1;
then
((a to_power (a-b))/a to_power (c-a))*(c to_power (c-a)/(c to_power ( b
-c))) *(b to_power (2*b-a-c)) >1 by XCMPLX_1:85;
then (a to_power ((a-b)-(c-a))) *(c to_power (c-a)/(c to_power (b-c))) *(b
to_power (2*b-a-c)) >1 by POWER:29;
then
(a to_power (2*a-b-c)) *(c to_power ((c-a)-(b-c))) *(b to_power (2*b-a-
c)) >1 by POWER:29;
then
(a to_power (2*a-(b+c))) *(c to_power (2*c-(a+b))) *(b to_power (2*b-(a
+c))) >1;
then (a to_power (2*a)/a to_power (b+c))*(c to_power (2*c-(a+b))) *(b
to_power (2*b-(a+c))) >1 by POWER:29;
then
(a to_power (2*a)/a to_power (b+c))*(c to_power (2*c)/c to_power (a+b )
) *(b to_power (2*b-(a+c))) >1 by POWER:29;
then ((a to_power (2*a))*((c to_power (2*c)))/((a to_power (b+c))* (c
to_power (a+b))))*(b to_power (2*b-(a+c))) >1 by XCMPLX_1:76;
then ((a to_power (2*a))*((c to_power (2*c)))/((a to_power (b+c))* (c
to_power (a+b))))* (b to_power (2*b)/b to_power (a+c)) >1 by POWER:29;
then ((a to_power (2*a))*(c to_power (2*c))*(b to_power (2*b)))/ ((a
to_power (b+c))* (c to_power (a+b))*(b to_power (a+c))) >1 by XCMPLX_1:76;
then (d/e)*e>1*e by A11,A4,A8,XREAL_1:68;
hence thesis by A11,A4,A8,XCMPLX_1:87;
end;
theorem
n>=1 implies a|^(n+1)+b|^(n+1)>=a|^n*b+a*b|^n
proof
assume
A1: n>=1;
per cases;
suppose
A2: a-b>0;
then a-b+b>0+b by XREAL_1:8;
then a|^n>b|^n by A1,PREPOWER:10;
then a|^n-b|^n>0 by XREAL_1:50;
then (a-b)*(a|^n-b|^n)>0 by A2;
then a*(a|^n)-a*(b|^n)-b*(a|^n)+b*(b|^n)>0;
then a|^(n+1)-a*(b|^n)-b*(a|^n)+b*(b|^n)>0 by NEWTON:6;
then a|^(n+1)-a*(b|^n)-b*(a|^n)+b|^(n+1)>0 by NEWTON:6;
then
(a|^(n+1)+b|^(n+1)-a*(b|^n)-b*(a|^n))+(a*(b|^n)+b*(a|^n))> 0+(a*(b|^n
)+b*(a|^n)) by XREAL_1:8;
hence thesis;
end;
suppose
A3: a-b=0;
then a|^n*b+a*b|^n =a|^(n+1)+(a|^n*a) by NEWTON:6
.=a|^(n+1)+a|^(n+1) by NEWTON:6
.=2*(a|^(n+1));
hence thesis by A3;
end;
suppose
A4: a-b<0;
then (a-b)+b<0+b by XREAL_1:8;
then a|^n<b|^n by A1,PREPOWER:10;
then a|^n-b|^n<0 by XREAL_1:49;
then (a-b)*(a|^n-b|^n)>0 by A4;
then a*(a|^n)-a*(b|^n)-b*(a|^n)+b*(b|^n)>0;
then a|^(n+1)-a*(b|^n)-b*(a|^n)+b*(b|^n)>0 by NEWTON:6;
then a|^(n+1)-a*(b|^n)-b*(a|^n)+b|^(n+1)>0 by NEWTON:6;
then
(a|^(n+1)+b|^(n+1)-a*(b|^n)-b*(a|^n))+(a*(b|^n)+b*(a|^n))> 0+(a*(b|^n
)+b*(a|^n)) by XREAL_1:8;
hence thesis;
end;
end;
theorem
a^2+b^2=c^2 & n>=3 implies a|^(n+2)+b|^(n+2)<c|^(n+2)
proof
assume that
A1: a^2+b^2=c^2 and
A2: n>=3;
A3: n>=1 by A2,XXREAL_0:2;
b^2>0;
then
A4: b|^2>0 by NEWTON:81;
c^2-b^2+b^2>0+b^2 by A1,XREAL_1:8;
then sqrt(c^2)>sqrt(b^2) by SQUARE_1:27;
then c>sqrt(b^2) by SQUARE_1:22;
then c>b by SQUARE_1:22;
then c|^n>b|^n by A3,PREPOWER:10;
then c|^n*b|^2>b|^n*b|^2 by A4,XREAL_1:68;
then
A5: c|^n*b|^2>b|^(n+2) by NEWTON:8;
a^2>0;
then
A6: a|^2>0 by NEWTON:81;
c^2-a^2+a^2>0+a^2 by A1,XREAL_1:8;
then sqrt(c^2)>sqrt(a^2) by SQUARE_1:27;
then c>sqrt(a^2) by SQUARE_1:22;
then c>a by SQUARE_1:22;
then c|^n>a|^n by A3,PREPOWER:10;
then c|^n*a|^2>a|^n*a|^2 by A6,XREAL_1:68;
then c|^n*a|^2>a|^(n+2) by NEWTON:8;
then c|^n*a|^2+c|^n*b|^2>a|^(n+2)+b|^(n+2) by A5,XREAL_1:8;
then c|^n*(a|^2+b|^2)>a|^(n+2)+b|^(n+2);
then c|^n*(a^2+b|^2)>a|^(n+2)+b|^(n+2) by NEWTON:81;
then c|^n*c^2>a|^(n+2)+b|^(n+2) by A1,NEWTON:81;
then c|^n*c|^2>a|^(n+2)+b|^(n+2) by NEWTON:81;
hence thesis by NEWTON:8;
end;
theorem
n>=1 implies (1+1/(n+1))|^n<(1+1/n)|^(n+1)
proof
assume
A1: n>=1;
n+1>n+0 by XREAL_1:8;
then 1/(n+1)<1/n by A1,XREAL_1:76;
then 1/(n+1)+1<1/n+1 by XREAL_1:8;
then
A2: (1+1/(n+1))|^n<(1+1/n)|^n by A1,PREPOWER:10;
A3: (1+1/n)|^n>0 by PREPOWER:6;
(1+1/n)|^(n+1)-(1+1/n)|^n =(1+1/n)|^n*(1+1/n)-(1+1/n)|^n by NEWTON:6
.=(1+1/n)|^n*(1/n);
then (1+1/n)|^(n+1)-(1+1/n)|^n+(1+1/n)|^n>0+(1+1/n)|^n by A1,A3,XREAL_1:8;
hence thesis by A2,XXREAL_0:2;
end;
theorem
n>=1 & k>=1 implies (a|^k+b|^k)*(a|^n+b|^n)<=2*(a|^(k+n)+b|^(k+n))
proof
assume that
A1: n>=1 and
A2: k>=1;
A3: (a|^k+b|^k)*(a|^n+b|^n)-2*(a|^(k+n)+b|^(k+n)) =a|^k*a|^n+a|^k*b|^n+b|^k*
a|^n+b|^k*b|^n-2*a|^(k+n)-2*(b|^(k+n))
.=a|^(k+n)+a|^k*b|^n+b|^k*a|^n+b|^k*b|^n-2*a|^(k+n)-2*(b|^(k+n)) by
NEWTON:8
.=a|^(k+n)+a|^k*b|^n+b|^k*a|^n+b|^(k+n)-2*a|^(k+n)-2*(b|^(k+n)) by NEWTON:8
.=a|^k*b|^n+b|^k*a|^n-a|^(k+n)-(b|^(k+n))
.=a|^k*b|^n+b|^k*a|^n-a|^k*a|^n-(b|^(k+n)) by NEWTON:8
.=a|^k*b|^n+b|^k*a|^n-a|^k*a|^n-b|^k*b|^n by NEWTON:8
.=(a|^n-b|^n)*(b|^k-a|^k);
per cases;
suppose
a-b>0;
then
A4: a-b+b>0+b by XREAL_1:8;
then a|^k>b|^k by A2,PREPOWER:10;
then
A5: b|^k-a|^k<0 by XREAL_1:49;
a|^n>b|^n by A1,A4,PREPOWER:10;
then a|^n-b|^n>0 by XREAL_1:50;
hence thesis by A3,A5,XREAL_1:48;
end;
suppose
a-b=0;
then a|^n=b|^n;
hence thesis by A3;
end;
suppose
a-b<0;
then
A6: a-b+b<0+b by XREAL_1:8;
then a|^k<b|^k by A2,PREPOWER:10;
then
A7: b|^k-a|^k>0 by XREAL_1:50;
a|^n<b|^n by A1,A6,PREPOWER:10;
then a|^n-b|^n<0 by XREAL_1:49;
hence thesis by A3,A7,XREAL_1:48;
end;
end;
theorem
(for n holds s.n=1/sqrt(n+1)) implies for n holds (Partial_Sums s).n<2
*sqrt(n+1)
proof
defpred X[Nat] means (Partial_Sums s).$1<2*sqrt($1+1);
assume
A1: for n holds s.n=1/sqrt(n+1);
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: sqrt(n+2)>0 by SQUARE_1:25;
4*n^2+12*n+8<4*n^2+12*n+9 by XREAL_1:8;
then sqrt(4*((n+2)*(n+1)))<sqrt(((2*n)+3)^2) by SQUARE_1:27;
then 2*sqrt((n+2)*(n+1))<sqrt(((2*n)+3)^2) by SQUARE_1:20,29;
then 2*sqrt((n+2)*(n+1))<2*n+3 by SQUARE_1:22;
then 2*sqrt((n+2)*(n+1))+1<2*n+3+1 by XREAL_1:8;
then 2*(sqrt(n+2)*sqrt(n+1))+1<2*(n+2) by SQUARE_1:29;
then 2*(sqrt(n+2)*sqrt(n+1))+1<2*sqrt((n+2)^2) by SQUARE_1:22;
then
(2*(sqrt(n+2)*sqrt(n+1))+1)/sqrt(n+2)<(2*sqrt((n+2)*(n+2)))/sqrt(n+2)
by A3,XREAL_1:74;
then
(2*(sqrt(n+2)*sqrt(n+1))+1)/sqrt(n+2)<(2*(sqrt(n+2)*sqrt(n+2)))/sqrt(
n +2) by SQUARE_1:29;
then
(2*(sqrt(n+2)*sqrt(n+1))+1)/sqrt(n+2)<(2*sqrt(n+2))*sqrt(n+2)/sqrt(n+ 2 );
then (2*(sqrt(n+2)*sqrt(n+1))+1)/sqrt(n+2)<2*sqrt(n+2) by A3,XCMPLX_1:89;
then (2*sqrt(n+1))*sqrt(n+2)/sqrt(n+2)+1/sqrt(n+2)<2*sqrt(n+2) by
XCMPLX_1:62;
then
A4: (2*sqrt(n+1))+1/sqrt(n+2)<2*sqrt(n+2) by A3,XCMPLX_1:89;
assume (Partial_Sums s).n<2*sqrt(n+1);
then (Partial_Sums s).n+1/sqrt(n+2)<2*sqrt(n+1)+1/sqrt(n+2) by XREAL_1:8;
then (Partial_Sums s).n+1/sqrt((n+1)+1)<2*sqrt(n+2) by A4,XXREAL_0:2;
then (Partial_Sums s).n+s.(n+1)<2*sqrt(n+2) by A1;
hence thesis by SERIES_1:def 1;
end;
(Partial_Sums s).0 = s.0 by SERIES_1:def 1
.=1/sqrt(0+1) by A1
.=1;
then
A5: X[0];
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th48:
(for n holds s.n=1/((n+1)^2)) implies for n holds (Partial_Sums
s).n<=2-1/(n+1)
proof
defpred X[Nat] means (Partial_Sums s).$1<=2-1/($1+1);
assume
A1: for n holds s.n=1/((n+1)^2);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume (Partial_Sums s).n<=2-1/(n+1);
then
A3: (Partial_Sums s).n+1/((n+2)^2)<=2-1/(n+1)+1/((n+2)^2) by XREAL_1:7;
n^2+3*n+3>n^2+3*n+2 by XREAL_1:8;
then (n^2+3*n+3)/((n+1)*((n+2)^2))>((n+2)*(n+1))/(((n+2)^2)*(n+1)) by
XREAL_1:74;
then (n^2+3*n+3)/((n+1)*((n+2)^2))>(n+2)/((n+2)*(n+2))by XCMPLX_1:91;
then (n^2+3*n+3)/((n+1)*((n+2)^2))>((n+2)/(n+2))/(n+2) by XCMPLX_1:78;
then (n^2+3*n+3)/((n+1)*((n+2)^2))>1/(n+2) by XCMPLX_1:60;
then (-1)*((n^2+3*n+3)/((n+1)*((n+2)^2)))<(-1)*(1/(n+2)) by XREAL_1:69;
then
A4: -(n^2+3*n+3)/((n+1)*((n+2)^2))+2<-1/(n+2)+2 by XREAL_1:8;
(Partial_Sums s).(n+1) =(Partial_Sums s).n+s.(n+1) by SERIES_1:def 1
.=(Partial_Sums s).n+1/((n+1+1)^2) by A1;
then (Partial_Sums s).(n+1)<=2-(1/(n+1)-1/((n+2)^2)) by A3;
then (Partial_Sums s).(n+1)<=2-(1*((n+2)^2)-1*(n+1))/((n+1)*((n+2)^2)) by
XCMPLX_1:130;
hence thesis by A4,XXREAL_0:2;
end;
(Partial_Sums s).0=s.0 by SERIES_1:def 1
.=1/((0+1)^2) by A1
.=1;
then
A5: X[0];
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem
(for n holds s.n=1/((n+1)^2)) implies (Partial_Sums s).n<2
proof
assume for n holds s.n=1/((n+1)^2);
then
A1: (Partial_Sums s).n<=2-1/(n+1) by Th48;
-(1/(n+1))+2<0+2 by XREAL_1:8;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th50:
(for n holds s.n<1) implies for n holds Partial_Sums(s).n<n+1
proof
defpred X[Nat] means Partial_Sums(s).$1<$1+1;
assume
A1: for n holds s.n<1;
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: Partial_Sums(s).(n+1) = Partial_Sums(s).n+s.(n+1) by SERIES_1:def 1;
assume Partial_Sums(s).n<n+1;
hence thesis by A1,A3,XREAL_1:8;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1;
then
A4: X[0] by A1;
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
(for n holds s.n>0 & s.n<1) implies for n holds Partial_Product(s).n>=
Partial_Sums(s).n-n
proof
defpred X[Nat] means Partial_Product(s).$1>=Partial_Sums(s).$1-$1;
assume
A1: for n holds s.n>0 & s.n<1;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: Partial_Product(s).n>=Partial_Sums(s).n-n;
A4: s.(n+1)<1 by A1;
Partial_Sums(s).n-(n+1)<0 by A1,Th50,XREAL_1:49;
then s.(n+1)*(Partial_Sums(s).n-n-1)>1*(Partial_Sums(s).n-n-1) by A4,
XREAL_1:69;
then
A5: s.(n+1)*Partial_Sums(s).n-s.(n+1)*n-s.(n+1)+s.(n+1)> Partial_Sums(s).
n-n-1+s.(n+1) by XREAL_1:8;
s.(n+1)>0 by A1;
then
Partial_Product(s).n*s.(n+1)>=(Partial_Sums(s).n-n)*s.(n+1) by A3,XREAL_1:64;
then Partial_Product(s).n*s.(n+1)>Partial_Sums(s).n+s.(n+1)-(n+1) by A5,
XXREAL_0:2;
then Partial_Product(s).(n+1)>Partial_Sums(s).n+s.(n+1)-(n+1) by
SERIES_3:def 1;
hence thesis by SERIES_1:def 1;
end;
Partial_Sums(s).0-0 = s.0 by SERIES_1:def 1;
then
A6: X[0] by SERIES_3:def 1;
for n holds X[n] from NAT_1:sch 2(A6,A2);
hence thesis;
end;
theorem Th52:
(for n being Nat holds s.n>0 & s1.n=1/s.n)
implies for n holds Partial_Sums(s1).n>0
proof
defpred X[Nat] means Partial_Sums(s1).$1>0;
assume
A1: for n being Nat holds s.n>0 & s1.n=1/s.n;
then
A2: s1.0=1/s.0;
A3: for n st X[n] holds X[n+1]
proof
let n;
assume
A4: Partial_Sums(s1).n>0;
A5: Partial_Sums(s1).(n+1)=Partial_Sums(s1).n+s1.(n+1) by SERIES_1:def 1;
A6: s.(n+1)>0 by A1;
s1.(n+1)=1/s.(n+1) by A1;
hence thesis by A4,A5,A6;
end;
s.0>0 by A1;
then
A7: X[0] by A2,SERIES_1:def 1;
for n holds X[n] from NAT_1:sch 2(A7,A3);
hence thesis;
end;
theorem
(for n being Nat holds s.n>0 & s1.n=1/s.n) implies
for n holds Partial_Sums(s).n*Partial_Sums(s1).n>=(n+1)^2
proof
defpred X[Nat] means Partial_Sums(s).$1*Partial_Sums(s1).$1>=($1+
1)^2;
assume
A1: for n being Nat holds s.n>0 & s1.n=1/s.n;
then
A2: s.0>0;
A3: for n st X[n] holds X[n+1]
proof
let n;
set x=Partial_Sums(s).n;
set y=Partial_Sums(s1).n;
assume
A4: Partial_Sums(s).n*Partial_Sums(s1).n>=(n+1)^2;
then
A5: x*y+(x/s.(n+1)+y*s.(n+1)+1)>=(n+1)^2+(x/s.(n+1)+y*s.(n+1)+1) by XREAL_1:7;
sqrt(x*y)>=sqrt((n+1)^2) by A4,SQUARE_1:26;
then sqrt(x*y)>=n+1 by SQUARE_1:22;
then
A6: 2*sqrt(x*y)>=2*(n+1) by XREAL_1:64;
A7: s.(n+1)>0 by A1;
A8: x>0 by A1,SERIES_3:33;
y>0 by A1,Th52;
then x/s.(n+1)+y*s.(n+1)>=2*sqrt((y*s.(n+1))*(x/s.(n+1))) by A7,A8,
SIN_COS2:1;
then x/s.(n+1)+y*s.(n+1)>=2*sqrt(x/((1*s.(n+1))/(y*s.(n+1)))) by
XCMPLX_1:81;
then x/s.(n+1)+y*s.(n+1)>=2*sqrt(x/(1/y)) by A7,XCMPLX_1:91;
then x/s.(n+1)+y*s.(n+1)>=2*sqrt(y*(x/1)) by XCMPLX_1:81;
then x/s.(n+1)+y*s.(n+1)>=2*n+2 by A6,XXREAL_0:2;
then
A9: (x/s.(n+1)+y*s.(n+1))+(n^2+2*n+2)>=(2*n+2)+(n^2+2*n+2) by XREAL_1:7;
Partial_Sums(s).(n+1)*Partial_Sums(s1).(n+1) =(x+s.(n+1))*Partial_Sums
(s1).(n+1) by SERIES_1:def 1
.=(x+s.(n+1))*(y+s1.(n+1)) by SERIES_1:def 1
.=x*y+x*(s1.(n+1))+(s.(n+1))*y+(s.(n+1))*(s1.(n+1))
.=x*y+x*(1/s.(n+1))+(s.(n+1))*y+(s.(n+1))*(s1.(n+1)) by A1
.=x*y+x*(1/s.(n+1))+(s.(n+1))*y+(s.(n+1))*(1/s.(n+1)) by A1
.=x*y+x*(1/s.(n+1))+(s.(n+1))*y+((s.(n+1))*1)/s.(n+1) by XCMPLX_1:74
.=x*y+x*(1/s.(n+1))+(s.(n+1))*y+1 by A7,XCMPLX_1:60
.=x*y+x/(s.(n+1)/1)+(s.(n+1))*y+1 by XCMPLX_1:79
.=x*y+x/s.(n+1)+(s.(n+1))*y+1;
hence thesis by A9,A5,XXREAL_0:2;
end;
Partial_Sums(s).0*Partial_Sums(s1).0 =s.0*Partial_Sums(s1).0 by
SERIES_1:def 1
.=s.0*s1.0 by SERIES_1:def 1
.=s.0*(1/s.0) by A1
.=s.0/(s.0/1) by XCMPLX_1:79
.=1 by A2,XCMPLX_1:60;
then
A10: X[0];
for n holds X[n] from NAT_1:sch 2(A10,A3);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n=sqrt(n) & s.0=0) implies for n st n>=1 holds
Partial_Sums(s).n<1/6*(4*n+3)*sqrt(n)
proof
defpred X[Nat] means Partial_Sums(s).$1<1/6*(4*$1+3)*sqrt($1);
assume
A1: for n st n>=1 holds s.n=sqrt(n) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
A3: n>=1 and
A4: Partial_Sums(s).n<1/6*(4*n+3)*sqrt(n);
n+1>=1+1 by A3,XREAL_1:7;
then n+1>=1 by XXREAL_0:2;
then
A5: s.(n+1)=sqrt(n+1) by A1;
0+(16*n^2+8*n)<1+(16*n^2+8*n) by XREAL_1:8;
then (16*n+8)*n<1*(16*n^2+8*n+1);
then (4*(4*n+1)+4)/((4*n+1)^2)<1/n by A3,XREAL_1:106;
then (4*(4*n+1))/((4*n+1)*(4*n+1))+4/((4*n+1)^2)<1/n by XCMPLX_1:62;
then 4/(4*n+1)+4/((4*n+1)^2)<1/n by XCMPLX_1:91;
then 1+(4/(4*n+1)+4/((4*n+1)^2))<1+1/n by XREAL_1:8;
then 1+4/(4*n+1)+4/((4*n+1)^2)<1+1/n;
then 1+2*2/(4*n+1)+(2/(4*n+1))^2<1+1/n by XCMPLX_1:76;
then 1+2*(2/(4*n+1))+(2/(4*n+1))^2<1+1/n by XCMPLX_1:74;
then (2/(4*n+1)+1)^2<(1+n*1)/n by A3,XCMPLX_1:113;
then sqrt((2/(4*n+1)+1)^2)<sqrt((1+n)/n) by SQUARE_1:27;
then 2/(4*n+1)+1<sqrt((1+n)/n) by SQUARE_1:22;
then (2+(4*n+1)*1)/(4*n+1)<sqrt((1+n)/n) by XCMPLX_1:113;
then
A6: (4*n+3)/(4*n+1)<sqrt(1+n)/sqrt(n) by SQUARE_1:30;
sqrt(n)>0 by A3,SQUARE_1:25;
then (1/6)*((4*n+3)*(sqrt(n)))<(1/6)*((sqrt(1+n))*(4*n+1)) by A6,XREAL_1:68
,102;
then Partial_Sums(s).n<(1/6)*sqrt(1+n)*((4*n)+7)-sqrt(1+n) by A4,XXREAL_0:2
;
then
A7: Partial_Sums(s).n+sqrt(1+n)<(1/6)*sqrt(1+n)*((4*n)+7)-sqrt(1+n)+sqrt(
1+n) by XREAL_1:8;
thus thesis by A5,A7,SERIES_1:def 1;
end;
Partial_Sums(s).(1+0) =Partial_Sums(s).0 + s.(1+0) by SERIES_1:def 1
.=s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=1 by A1,SQUARE_1:18;
then
A8: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A8,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n=sqrt(n) & s.0=0) implies for n st n>=1 holds
Partial_Sums(s).n>(2/3)*n*sqrt(n)
proof
defpred X[Nat] means Partial_Sums(s).$1>(2/3)*$1*sqrt($1);
assume
A1: for n st n>=1 holds s.n=sqrt(n) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
A3: n>=1 and
A4: Partial_Sums(s).n>(2/3)*n*sqrt(n);
2*n>=2*1 by A3,XREAL_1:64;
then 2*n>1 by XXREAL_0:2;
then
A5: 2*n-1>0 by XREAL_1:50;
3*n>=3*1 by A3,XREAL_1:64;
then 3*n>1 by XXREAL_0:2;
then 1-3*n<0 by XREAL_1:49;
then 1+(n-4*n)+(4*n^2-4*n^2)+4*n|^3<0+4*n|^3 by XREAL_1:8;
then (4*(n|^(2+1))-4*n^2+n)+(4*n^2-4*n+1)<4*n|^3;
then (4*(n|^2*n)-4*(n*n)+n)+(4*n^2-4*n+1)<4*n|^3 by NEWTON:6;
then (4*n|^2-4*n+1)*n+(4*n^2-4*n+1)*1<4*n|^3;
then (4*n^2-4*n+1)*n+(4*n^2-4*n+1)*1<4*n|^3 by NEWTON:81;
then (4*n^2-4*n+1)*(n+1)<4*n|^(2+1);
then (4*n^2-4*n+1)*(n+1)<4*(n|^2*n) by NEWTON:6;
then (4*n^2-4*n+1)*(n+1)<4*n|^2*n;
then (2*n-1)^2*(n+1)<4*n^2*n by NEWTON:81;
then (n+1)/n<(2*n)^2/(2*n-1)^2 by A3,A5,XREAL_1:106;
then (n+1)/n<((2*n)/(2*n-1))^2 by XCMPLX_1:76;
then sqrt((n+1)/n)<sqrt(((2*n)/(2*n-1))^2) by SQUARE_1:27;
then sqrt((n+1)/n)<(2*n)/(2*n-1) by A5,SQUARE_1:22;
then
A6: sqrt(n+1)/sqrt(n)<(2*n)/(2*n-1) by SQUARE_1:30;
sqrt(n)>0 by A3,SQUARE_1:25;
then (1/3)*(sqrt(n+1)*(2*n-1))<(1/3)*((2*n)*sqrt(n)) by A5,A6,XREAL_1:68
,102;
then Partial_Sums(s).n>((2/3)*(n+1))*sqrt(n+1)-sqrt(n+1) by A4,XXREAL_0:2;
then
A7: Partial_Sums(s).n+sqrt(n+1)>((2/3)*(n+1))*sqrt(n+1)-sqrt(n+1)+ sqrt(n
+1 ) by XREAL_1:8;
n+1>=1+1 by A3,XREAL_1:7;
then n+1>=1 by XXREAL_0:2;
then Partial_Sums(s).n+s.(n+1)>((2/3)*(n+1))*sqrt(n+1) by A1,A7;
hence thesis by SERIES_1:def 1;
end;
Partial_Sums(s).(1+0) =Partial_Sums(s).0 + s.(1+0) by SERIES_1:def 1
.=s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=1 by A1,SQUARE_1:18;
then
A8: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A8,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n=1+1/(2*n+1) & s.0=1) implies for n st n>=1
holds Partial_Product(s).n>(1/2)*sqrt(2*n+3)
proof
defpred X[Nat] means Partial_Product(s).$1>(1/2)*sqrt(2*$1+3);
A1: (1/2)*sqrt(2*1+3)=sqrt(5)/2;
assume
A2: for n st n>=1 holds s.n=1+1/(2*n+1) & s.0=1;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
A4: n>=1 and
A5: Partial_Product(s).n>(1/2)*sqrt(2*n+3);
n+1>=1+1 by A4,XREAL_1:7;
then
A6: n+1>=1 by XXREAL_0:2;
A7: sqrt(2*n+3)>0 by SQUARE_1:25;
1/(2*n+3)+(2*n+5)>0+(2*n+5) by XREAL_1:8;
then 1/(2*n+3)+2+(2*n+3)>2*n+5;
then 1^2/(sqrt(2*n+3))^2+2+(2*n+3)>2*n+5 by SQUARE_1:def 2;
then (1/(sqrt(2*n+3)))^2+2+(2*n+3)>2*n+5 by XCMPLX_1:76;
then (1/sqrt(2*n+3))^2+2*1+(sqrt(2*n+3))^2>2*n+5 by SQUARE_1:def 2;
then
(1/sqrt(2*n+3))^2+2*(sqrt(2*n+3)*(1/sqrt(2*n+3)))+(sqrt(2*n+3))^2>2*n
+5 by A7,XCMPLX_1:106;
then sqrt((1/sqrt(2*n+3)+sqrt(2*n+3))^2)>sqrt(2*n+5) by SQUARE_1:27;
then sqrt(2*n+3)+1/sqrt(2*n+3)>sqrt(2*n+5) by A7,SQUARE_1:22;
then
A8: (1/2)*(sqrt(2*n+3)+1/sqrt(2*n+3))>(1/2)*sqrt(2*n+5) by XREAL_1:68;
Partial_Product(s).n*(1+1/(2*n+3))>((1/2)*sqrt(2*n+3))*(1+1/(2*n+3))
by A5,XREAL_1:68;
then
Partial_Product(s).n*(1+1/(2*n+3))>((1/2)*sqrt(2*n+3))*1+ ((1/2)*sqrt
(2*n+3))*(1/(2*n+3));
then
Partial_Product(s).n*(1+1/(2*n+3))>(1/2)*sqrt(2*n+3)+ ((1/2)*sqrt(2*n
+3))/(2*n+3) by XCMPLX_1:74;
then
Partial_Product(s).n*(1+1/(2*n+3))>(1/2)*sqrt(2*n+3)+ (1/2)*(sqrt(2*n
+3)/(2*n+3)) by XCMPLX_1:74;
then
Partial_Product(s).n*(1+1/(2*n+3))>(1/2)*sqrt(2*n+3)+ (1/2)*(sqrt(2*n
+3)/sqrt((2*n+3)^2)) by SQUARE_1:22;
then
Partial_Product(s).n*(1+1/(2*n+3))>(1/2)*sqrt(2*n+3)+ (1/2)*((sqrt(2*
n+3)*1)/(sqrt(2*n+3)*sqrt(2*n+3))) by SQUARE_1:29;
then
Partial_Product(s).n*(1+1/(2*n+3))>(1/2)*sqrt(2*n+3)+ (1/2)*((sqrt(2*
n+3)/sqrt(2*n+3))*(1/sqrt(2*n+3))) by XCMPLX_1:76;
then Partial_Product(s).n*(1+1/(2*n+3))>(1/2)*sqrt(2*n+3)+ (1/2)*(1*(1/
sqrt(2*n+3))) by A7,XCMPLX_1:60;
then Partial_Product(s).n*(1+1/(2*(n+1)+1))>(1/2)*sqrt(2*n+5) by A8,
XXREAL_0:2;
then Partial_Product(s).n*s.(n+1)>(1/2)*sqrt(2*n+5) by A2,A6;
hence thesis by SERIES_3:def 1;
end;
sqrt(16/9)>sqrt(5/4) by SQUARE_1:27;
then sqrt(4^2)/sqrt(3^2)>sqrt(5/4) by SQUARE_1:30;
then 4/sqrt(3^2)>sqrt(5/4) by SQUARE_1:22;
then 4/3>sqrt(5/4) by SQUARE_1:22;
then
A9: 4/3>sqrt(5)/sqrt(2^2) by SQUARE_1:30;
Partial_Product(s).(1+0) =Partial_Product(s).0 * s.(1+0) by SERIES_3:def 1
.=s.0 * s.1 by SERIES_3:def 1
.=1*s.1 by A2
.=1+1/(2*1+1) by A2
.=4/3;
then
A10: X[1] by A1,A9,SQUARE_1:22;
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A10,A3);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n=sqrt(n*(n+1)) & s.0=0) implies for n st n>=1
holds Partial_Sums(s).n>(n*(n+1))/2
proof
defpred X[Nat] means Partial_Sums(s).$1>($1*($1+1))/2;
assume
A1: for n st n>=1 holds s.n=sqrt(n*(n+1)) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
A3: n>=1 and
A4: Partial_Sums(s).n>(n*(n+1))/2;
n+1>=1+1 by A3,XREAL_1:7;
then n+1>=1 by XXREAL_0:2;
then
A5: s.(n+1)=sqrt((n+1)*(n+1+1)) by A1;
n+2>n+1 by XREAL_1:8;
then (n+2)*(n+1)>(n+1)^2 by XREAL_1:68;
then sqrt((n+2)*(n+1))>sqrt((n+1)^2) by SQUARE_1:27;
then
A6: sqrt((n+2)*(n+1))>n+1 by SQUARE_1:22;
Partial_Sums(s).n+(sqrt((n+1)*(n+2))-((n+1)*(n+2))/2)>(n*(n+1))/2 +(
sqrt((n+1)*(n+2))-((n+1)*(n+2))/2) by A4,XREAL_1:8;
then
Partial_Sums(s).n+sqrt((n+1)*(n+2))-((n+1)*(n+2))/2> sqrt((n+1)*(n+2)
)-(n+1);
then Partial_Sums(s).n+sqrt((n+1)*(n+2))-((n+1)*(n+2))/2>0 by A6,XREAL_1:50
;
then
A7: Partial_Sums(s).n+sqrt((n+1)*(n+2))-((n+1)*(n+2))/2+((n+1)*(n+2))/2>0
+((n+1)*(n+2))/2 by XREAL_1:8;
thus thesis by A5,A7,SERIES_1:def 1;
end;
A8: Partial_Sums(s).1 = Partial_Sums(s).(0+1)
.=Partial_Sums(s).0+s.1 by SERIES_1:def 1
.=s.0+s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=sqrt(1*(1+1)) by A1
.=sqrt 2;
then (Partial_Sums(s).1)^2 = 2 by SQUARE_1:def 2;
then sqrt((Partial_Sums(s).1)^2)>sqrt(((1*(1+1))/2)^2) by SQUARE_1:27;
then
A9: sqrt((Partial_Sums(s).1)^2)>((1*(1+1))/2);
Partial_Sums(s).1>0 by A8,SQUARE_1:25;
then
A10: X[1] by A9,SQUARE_1:22;
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A10,A2);
hence thesis;
end;