:: 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-2021 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;


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;

theorem :: SERIES_5:1
  (a+b)*(1/a+1/b)>=4;

theorem :: SERIES_5:2
  a|^4+b|^4>=a|^3*b+a*b|^3;

theorem :: SERIES_5:3
  a<b implies 1<(b+c)/(a+c);

theorem :: SERIES_5:4
  a<b implies a/b<sqrt(a/b);

theorem :: SERIES_5:5
  a<b implies sqrt(a/b)<(b+sqrt((a^2+b^2)/2))/(a+sqrt((a^2+b^2)/2));

theorem :: SERIES_5:6
  a<b implies a/b<(b+sqrt((a^2+b^2)/2))/(a+sqrt((a^2+b^2)/2));

theorem :: SERIES_5:7
  2/((1/a)+(1/b))<=sqrt(a*b);

theorem :: SERIES_5:8
  (a+b)/2<=sqrt((a^2+b^2)/2);

theorem :: SERIES_5:9
  x+y<=sqrt(2*(x^2+y^2));

theorem :: SERIES_5:10
  2/((1/a)+(1/b))<=(a+b)/2;

theorem :: SERIES_5:11
  sqrt(a*b)<=sqrt((a^2+b^2)/2);

theorem :: SERIES_5:12
  2/((1/a)+(1/b))<=sqrt((a^2+b^2)/2);

theorem :: SERIES_5:13
  |.x.|<1 & |.y.|<1 implies |.(x+y)/(1+x*y).|<=1;

theorem :: SERIES_5:14
  |.x+y.|/(1+|.x+y.|)<=|.x.|/(1+|.x.|)+|.y.|/(1+|.y.|);

theorem :: SERIES_5:15
  a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d)>1;

theorem :: SERIES_5:16
  a/(a+b+d)+b/(a+b+c)+c/(b+c+d)+d/(a+c+d)<2;

theorem :: SERIES_5:17
  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);

theorem :: SERIES_5:18
  sqrt((a+b)*(c+d))>=sqrt(a*c)+sqrt(b*d);

theorem :: SERIES_5:19
  (a*b+c*d)*(a*c+b*d)>=4*a*b*c*d;

theorem :: SERIES_5:20
  a/b+b/c+c/a>=3;

theorem :: SERIES_5:21
  a*b+b*c+c*a=1 implies a+b+c>=sqrt 3;

theorem :: SERIES_5:22
  (b+c-a)/a+(c+a-b)/b+(a+b-c)/c>=3;

theorem :: SERIES_5:23
  (a+1/a)*(b+1/b)>=(sqrt(a*b)+1/sqrt(a*b))^2;

theorem :: SERIES_5:24
  (b*c)/a+(a*c)/b+(a*b)/c>=a+b+c;

theorem :: SERIES_5:25
  x>y & y>z implies x^2*y+y^2*z+z^2*x>x*y^2+y*z^2+z*x^2;

theorem :: SERIES_5:26
  a>b & b>c implies b/(a-b)>c/(a-c);

theorem :: SERIES_5:27
  b>a & c>d implies c/(c+a)>d/(d+b);

theorem :: SERIES_5:28
  m*x+z*y<=sqrt(m^2+z^2)*sqrt(x^2+y^2);

theorem :: SERIES_5:29
  (m*x+u*y+w*z)^2<=(m^2+u^2+w^2)*(x^2+y^2+z^2);

theorem :: SERIES_5:30
  (9*a*b*c)/(a^2+b^2+c^2)<=a+b+c;

theorem :: SERIES_5:31
  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);

theorem :: SERIES_5:32
  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);

theorem :: SERIES_5:33
  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));

theorem :: SERIES_5:34
  sqrt(3*(a^2+b^2+c^2))<=(b*c)/a+(c*a)/b+(a*b)/c;

theorem :: SERIES_5:35
  a+b=1 implies (1/a^2-1)*(1/b^2-1)>=9;

theorem :: SERIES_5:36
  a+b=1 implies a*b+1/(a*b)>=17/4;

theorem :: SERIES_5:37
  a+b+c = 1 implies 1/a+1/b+1/c>=9;

theorem :: SERIES_5:38
  a+b+c = 1 implies (1/a-1)*(1/b-1)*(1/c-1)>=8;

theorem :: SERIES_5:39
  a+b+c = 1 implies (1+1/a)*(1+1/b)*(1+1/c)>=64;

theorem :: SERIES_5:40
  x+y+z=1 implies x^2+y^2+z^2>=1/3;

theorem :: SERIES_5:41
  x+y+z=1 implies x*y+y*z+z*x<=1/3;

theorem :: SERIES_5:42
  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));

theorem :: SERIES_5:43
  n>=1 implies a|^(n+1)+b|^(n+1)>=a|^n*b+a*b|^n;

theorem :: SERIES_5:44
  a^2+b^2=c^2 & n>=3 implies a|^(n+2)+b|^(n+2)<c|^(n+2);

theorem :: SERIES_5:45
  n>=1 implies (1+1/(n+1))|^n<(1+1/n)|^(n+1);

theorem :: SERIES_5:46
  n>=1 & k>=1 implies (a|^k+b|^k)*(a|^n+b|^n)<=2*(a|^(k+n)+b|^(k+n));

theorem :: SERIES_5:47
  (for n holds s.n=1/sqrt(n+1)) implies for n holds (Partial_Sums s).n<2
  *sqrt(n+1);

theorem :: SERIES_5:48
  (for n holds s.n=1/((n+1)^2)) implies for n holds (Partial_Sums
  s).n<=2-1/(n+1);

theorem :: SERIES_5:49
  (for n holds s.n=1/((n+1)^2)) implies (Partial_Sums s).n<2;

theorem :: SERIES_5:50
  (for n holds s.n<1) implies for n holds Partial_Sums(s).n<n+1;

theorem :: SERIES_5:51
  (for n holds s.n>0 & s.n<1) implies for n holds Partial_Product(s).n>=
  Partial_Sums(s).n-n;

theorem :: SERIES_5:52
  (for n being Nat holds s.n>0 & s1.n=1/s.n)
  implies for n holds Partial_Sums(s1).n>0;

theorem :: SERIES_5:53
  (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;

theorem :: SERIES_5:54
  (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);

theorem :: SERIES_5:55
  (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);

theorem :: SERIES_5:56
  (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);

theorem :: SERIES_5:57
  (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;