DOE MACSYMA Version 10. (c1) Batching the file triang Batching done. (d1) triang (c2) (c3) /* */ showproof: true $ (c4) /* 1.1 */ trineq(3*csum(a*b)<=csum(a)^2); 2 To prove: (c + b + a) >= 3 (b c + a c + a b) Expanding and collecting terms of the same sign gives: 2 2 2 c + b + a >= b c + a c + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 2 2 2 2 z + (y + x) z + y + x y + x z + (3 y + 3 x) z + y + 3 x y + x ------------------------------ >= ------------------------------------ 2 4 Multiplying both sides by 4 gives: 2 2 2 2 z + 2 y z + 2 x z + 2 y + 2 x y + 2 x >= 2 2 2 z + 3 y z + 3 x z + y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 z + y + x >= y z + x z + x y Expressing in terms of symmetric polynomials gives: {2, 0, 0} >= {1, 1, 0} This result follows from the majorization theorem. (d4) true (c5) trineq(csum(a)^2<4*csum(a*b)); 2 To prove: 4 (b c + a c + a b) > (c + b + a) Expanding and collecting terms of the same sign gives: 2 2 2 2 b c + 2 a c + 2 a b > c + b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 2 2 2 2 z + (3 y + 3 x) z + y + 3 x y + x z + (y + x) z + y + x y + x ------------------------------------ > ------------------------------ 2 2 Multiplying both sides by 2 gives: 2 2 2 2 2 2 z + 3 y z + 3 x z + y + 3 x y + x > z + y z + x z + y + x y + x Expanding and collecting terms of the same sign gives: 2 y z + 2 x z + 2 x y > 0 This is true because a sum of positive terms must be positive. (d5) true (c6) /* 1.2 */ trineq(csum(a^2)>=(36/35)*(s^2+a*b*c/s)); 2 a b c 36 (s + -----) 2 2 2 s To prove: c + b + a >= --------------- 35 Multiplying both sides by 35 s gives: 2 2 2 3 35 c s + 35 b s + 35 a s >= 36 s + 36 a b c Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 2 (35 c + (35 b + 35 a) c + (35 b + 35 a ) c + 35 b + 35 a b + 35 a b 3 3 2 2 2 3 + 35 a )/2 >= (9 c + (27 b + 27 a) c + (27 b + 126 a b + 27 a ) c + 9 b 2 2 3 + 27 a b + 27 a b + 9 a )/2 Multiplying both sides by 2 gives: 3 2 2 2 2 3 2 2 35 c + 35 b c + 35 a c + 35 b c + 35 a c + 35 b + 35 a b + 35 a b 3 3 2 2 2 2 3 + 35 a >= 9 c + 27 b c + 27 a c + 27 b c + 126 a b c + 27 a c + 9 b 2 2 3 + 27 a b + 27 a b + 9 a Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 26 c + 8 b c + 8 a c + 8 b c + 8 a c + 26 b + 8 a b + 8 a b + 26 a >= 126 a b c Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 (34 z + (59 y + 59 x) z + (59 y + 48 x y + 59 x ) z + 34 y + 59 x y 2 3 + 59 x y + 34 x )/4 >= 2 2 2 2 2 (63 y + 63 x) z + (63 y + 126 x y + 63 x ) z + 63 x y + 63 x y ------------------------------------------------------------------ 4 Multiplying both sides by 4 gives: 3 2 2 2 2 3 2 34 z + 59 y z + 59 x z + 59 y z + 48 x y z + 59 x z + 34 y + 59 x y 2 3 2 2 2 2 + 59 x y + 34 x >= 63 y z + 63 x z + 63 y z + 126 x y z + 63 x z 2 2 + 63 x y + 63 x y Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 34 z + 34 y + 34 x >= 4 y z + 4 x z + 4 y z + 78 x y z + 4 x z + 4 x y 2 + 4 x y Dividing both sides by 2 gives: 3 3 3 2 2 2 2 2 17 z + 17 y + 17 x >= 2 y z + 2 x z + 2 y z + 39 x y z + 2 x z + 2 x y 2 + 2 x y Expressing in terms of symmetric polynomials gives: 17 {3, 0, 0} >= 4 {2, 1, 0} + 13 {1, 1, 1} This follows from the following majorizations: 4 {3, 0, 0} >= 4 {2, 1, 0} 13 {3, 0, 0} >= 13 {1, 1, 1} (d6) true (c7) /* 1.3 */ trineq(8*cprod(s-a)<=a*b*c); To prove: a b c >= 8 (s - a) (s - b) (s - c) Expanding and collecting terms of the same sign gives: 2 2 2 3 8 c s + 8 b s + 8 a s + 9 a b c >= 8 s + 8 b c s + 8 a c s + 8 a b s Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 2 2 c + (6 b + 6 a) c + (6 b + 21 a b + 6 a ) c + 2 b + 6 a b + 6 a b 3 3 2 2 2 3 2 + 2 a >= c + (7 b + 7 a) c + (7 b + 18 a b + 7 a ) c + b + 7 a b 2 3 + 7 a b + a Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 c + 3 a b c + b + a >= b c + a c + b c + a c + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 z + (3 y + 3 x) z + (3 y + 3 x y + 3 x ) z + y + 3 x y + 3 x y + x ------------------------------------------------------------------------- >= 4 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 2 z + 6 y z + 6 x z + 6 y z + 6 x y z + 6 x z + 2 y + 6 x y + 6 x y 3 3 2 2 2 2 3 2 + 2 x >= 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y 2 3 + 5 x y + 2 x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 y z + x z + y z + x z + x y + x y >= 6 x y z Expressing in terms of symmetric polynomials gives: {2, 1, 0} >= {1, 1, 1} This result follows from the majorization theorem. (d7) true (c8) /* 1.4 */ trineq(8*a*b*c<=cprod(a+b)); To prove: (b + a) (c + a) (c + b) >= 8 a b c Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 b c + a c + b c + a c + a b + a b >= 6 a b c Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 2 2 2 2 2 3 (3 y + 3 x) z + (3 y + 6 x y + 3 x ) z + 3 x y + 3 x y + 2 x )/8 >= ---------------------------------------------------------- 4 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y + 5 x y 3 2 2 2 2 2 2 + 2 x >= 6 y z + 6 x z + 6 y z + 12 x y z + 6 x z + 6 x y + 6 x y Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 2 z + 2 y + 2 x >= y z + x z + y z + x z + x y + x y Expressing in terms of symmetric polynomials gives: {3, 0, 0} >= {2, 1, 0} This result follows from the majorization theorem. (d8) true (c9) /* 1.5 */ trineq(3*cprod(a+b)<=8*csum(a^3)); 3 3 3 To prove: 8 (c + b + a ) >= 3 (b + a) (c + a) (c + b) Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 2 z + (3 y + 3 x) z + (3 y + 3 x ) z + 2 y + 3 x y + 3 x y + 2 x >= 3 2 2 2 3 2 (6 z + (21 y + 21 x) z + (21 y + 48 x y + 21 x ) z + 6 y + 21 x y 2 3 + 21 x y + 6 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 16 z + 24 y z + 24 x z + 24 y z + 24 x z + 16 y + 24 x y + 24 x y 3 3 2 2 2 2 3 + 16 x >= 6 z + 21 y z + 21 x z + 21 y z + 48 x y z + 21 x z + 6 y 2 2 3 + 21 x y + 21 x y + 6 x Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 10 z + 3 y z + 3 x z + 3 y z + 3 x z + 10 y + 3 x y + 3 x y + 10 x >= 48 x y z Expressing in terms of symmetric polynomials gives: 5 {3, 0, 0} + 3 {2, 1, 0} >= 8 {1, 1, 1} This follows from the following majorizations: 3 {2, 1, 0} >= 3 {1, 1, 1} 5 {3, 0, 0} >= 5 {1, 1, 1} (d9) true (c10) /* 1.6 */ trineq(2*csum(a)*csum(a^2)>=3*(csum(a^3)+3*a*b*c)); 2 2 2 3 3 3 To prove: 2 (c + b + a) (c + b + a ) >= 3 (c + 3 a b c + b + a ) Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 3 3 3 2 b c + 2 a c + 2 b c + 2 a c + 2 a b + 2 a b >= c + 9 a b c + b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/4 >= 3 2 2 2 3 2 2 3 z + (6 y + 6 x) z + (6 y + 9 x y + 6 x ) z + y + 6 x y + 6 x y + x ------------------------------------------------------------------------- 4 Multiplying both sides by 4 gives: 3 2 2 2 2 3 2 2 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y + 5 x y 3 3 2 2 2 2 3 2 + 2 x >= z + 6 y z + 6 x z + 6 y z + 9 x y z + 6 x z + y + 6 x y 2 3 + 6 x y + x Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 z + 3 x y z + y + x >= y z + x z + y z + x z + x y + x y Expressing in terms of symmetric polynomials gives: {3, 0, 0} + {1, 1, 1} >= 2 {2, 1, 0} This follows from the following majorizations: {3, 0, 0} + {1, 1, 1} >= 2 {2, 1, 0} (d10) true (c11) /* 1.7 */ trineq(a*b*c a b c Expanding and collecting terms of the same sign gives: 2 2 2 3 3 3 c s + b s + a s > c + a b c + b + a Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 2 3 c + (b + a) c + (b + a ) c + b + a b + a b + a 3 3 3 ----------------------------------------------------- > c + a b c + b + a 2 Multiplying both sides by 2 gives: 3 2 2 2 2 3 2 2 3 c + b c + a c + b c + a c + b + a b + a b + a > 3 3 3 2 c + 2 a b c + 2 b + 2 a Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 3 3 3 b c + a c + b c + a c + a b + a b > c + 2 a b c + b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 3 2 2 2 3 2 + 2 x )/8 > (2 z + (5 y + 5 x) z + (5 y + 4 x y + 5 x ) z + 2 y + 5 x y 2 3 + 5 x y + 2 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y + 5 x y 3 3 2 2 2 2 3 2 + 2 x > 2 z + 5 y z + 5 x z + 5 y z + 4 x y z + 5 x z + 2 y + 5 x y 2 3 + 5 x y + 2 x Expanding and collecting terms of the same sign gives: 8 x y z > 0 This is true because a sum of positive terms must be positive. (d11) true (c12) trineq(csum(a^2*(s-a))<=3*a*b*c/2); 3 a b c 2 2 2 To prove: ------- >= c (s - c) + b (s - b) + a (s - a) 2 Expanding and collecting terms of the same sign gives: 3 3 a b c 3 3 2 2 2 c + ------- + b + a >= c s + b s + a s 2 Multiplying both sides by 2 gives: 3 3 3 2 2 2 2 c + 3 a b c + 2 b + 2 a >= 2 c s + 2 b s + 2 a s Let s = (c+b+a)/2 . We get: 3 3 3 3 2 2 2 3 2 2 c + 3 a b c + 2 b + 2 a >= c + (b + a) c + (b + a ) c + b + a b 2 3 + a b + a Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 c + 3 a b c + b + a >= b c + a c + b c + a c + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 z + (3 y + 3 x) z + (3 y + 3 x y + 3 x ) z + y + 3 x y + 3 x y + x ------------------------------------------------------------------------- >= 4 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 2 z + 6 y z + 6 x z + 6 y z + 6 x y z + 6 x z + 2 y + 6 x y + 6 x y 3 3 2 2 2 2 3 2 + 2 x >= 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y 2 3 + 5 x y + 2 x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 y z + x z + y z + x z + x y + x y >= 6 x y z Expressing in terms of symmetric polynomials gives: {2, 1, 0} >= {1, 1, 1} This result follows from the majorization theorem. (d12) true (c13) /* 1.8 */ trineq(csum(a*b*(a+b))>=48*cprod(s-a)); To prove: b c (c + b) + a c (c + a) + a b (b + a) >= 48 (s - a) (s - b) (s - c) Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 48 c s + 48 b s + 48 a s + b c + a c + b c + 48 a b c + a c + a b 2 3 + a b >= 48 s + 48 b c s + 48 a c s + 48 a b s Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 12 c + (37 b + 37 a) c + (37 b + 120 a b + 37 a ) c + 12 b + 37 a b 2 3 3 2 2 2 + 37 a b + 12 a >= 6 c + (42 b + 42 a) c + (42 b + 108 a b + 42 a ) c 3 2 2 3 + 6 b + 42 a b + 42 a b + 6 a Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 6 c + 12 a b c + 6 b + 6 a >= 5 b c + 5 a c + 5 b c + 5 a c + 5 a b 2 + 5 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 (6 z + (15 y + 15 x) z + (15 y + 12 x y + 15 x ) z + 6 y + 15 x y 2 3 3 2 2 2 + 15 x y + 6 x )/4 >= (10 z + (25 y + 25 x) z + (25 y + 60 x y + 25 x ) z 3 2 2 3 + 10 y + 25 x y + 25 x y + 10 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 12 z + 30 y z + 30 x z + 30 y z + 24 x y z + 30 x z + 12 y + 30 x y 2 3 3 2 2 2 2 + 30 x y + 12 x >= 10 z + 25 y z + 25 x z + 25 y z + 60 x y z + 25 x z 3 2 2 3 + 10 y + 25 x y + 25 x y + 10 x Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 2 z + 5 y z + 5 x z + 5 y z + 5 x z + 2 y + 5 x y + 5 x y + 2 x >= 36 x y z Expressing in terms of symmetric polynomials gives: {3, 0, 0} + 5 {2, 1, 0} >= 6 {1, 1, 1} This follows from the following majorizations: 5 {2, 1, 0} >= 5 {1, 1, 1} {3, 0, 0} >= {1, 1, 1} (d13) true (c14) /* 1.9 */ trineq(csum(a^3*(s-a))<=a*b*c*s); 3 3 3 To prove: a b c s >= c (s - c) + b (s - b) + a (s - a) Expanding and collecting terms of the same sign gives: 4 4 4 3 3 3 a b c s + c + b + a >= c s + b s + a s Let s = (c+b+a)/2 . We get: 4 2 2 2 4 4 2 c + a b c + (a b + a b) c + 2 b + 2 a --------------------------------------------- >= 2 4 3 3 3 4 3 3 4 c + (b + a) c + (b + a ) c + b + a b + a b + a ----------------------------------------------------- 2 Multiplying both sides by 2 gives: 4 2 2 2 4 4 2 c + a b c + a b c + a b c + 2 b + 2 a >= 4 3 3 3 3 4 3 3 4 c + b c + a c + b c + a c + b + a b + a b + a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 c + a b c + a b c + a b c + b + a >= 3 3 3 3 3 3 b c + a c + b c + a c + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (z + (3 y + 3 x) z + (5 y + 4 x y + 5 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 4 x y + 4 x y + 3 x ) z + y + 3 x y + 5 x y + 3 x y + x ) 4 3 2 2 2 /8 >= (z + (3 y + 3 x) z + (3 y + 6 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 6 x y + 6 x y + 3 x ) z + y + 3 x y + 3 x y + 3 x y + x )/8 Multiplying both sides by 8 gives: 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 5 y z + 4 x y z + 5 x z + 3 y z + 4 x y z 2 3 4 3 2 2 3 4 + 4 x y z + 3 x z + y + 3 x y + 5 x y + 3 x y + x >= 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 3 y z + 6 x y z + 3 x z + 3 y z + 6 x y z 2 3 4 3 2 2 3 4 + 6 x y z + 3 x z + y + 3 x y + 3 x y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 2 2 y z + 2 x z + 2 x y >= 2 x y z + 2 x y z + 2 x y z Dividing both sides by 2 gives: 2 2 2 2 2 2 2 2 2 y z + x z + x y >= x y z + x y z + x y z Expressing in terms of symmetric polynomials gives: {2, 2, 0} >= {2, 1, 1} This result follows from the majorization theorem. (d14) true (c15) /* 1.10 */ trineq(csum(a^5*(s-a))<=(1/2)*a*b*c*csum(a^3)); 3 3 3 a b c (c + b + a ) 5 5 5 To prove: -------------------- >= c (s - c) + b (s - b) + a (s - a) 2 Expanding and collecting terms of the same sign gives: 4 4 4 6 a b c a b c a b c 6 6 5 5 5 c + ------ + ------ + ------ + b + a >= c s + b s + a s 2 2 2 Multiplying both sides by 2 gives: 6 4 4 4 6 6 5 5 5 2 c + a b c + a b c + a b c + 2 b + 2 a >= 2 c s + 2 b s + 2 a s Let s = (c+b+a)/2 . We get: 6 4 4 4 6 6 2 c + a b c + (a b + a b) c + 2 b + 2 a >= 6 5 5 5 6 5 5 6 c + (b + a) c + (b + a ) c + b + a b + a b + a Expanding and collecting terms of the same sign gives: 6 4 4 4 6 6 c + a b c + a b c + a b c + b + a >= 5 5 5 5 5 5 b c + a c + b c + a c + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 6 5 2 2 4 (z + (4 y + 4 x) z + (10 y + 5 x y + 10 x ) z 3 2 2 3 3 + (13 y + 7 x y + 7 x y + 13 x ) z 4 3 2 2 3 4 2 + (10 y + 7 x y + 9 x y + 7 x y + 10 x ) z 5 4 2 3 3 2 4 5 6 5 + (4 y + 5 x y + 7 x y + 7 x y + 5 x y + 4 x ) z + y + 4 x y 2 4 3 3 4 2 5 6 + 10 x y + 13 x y + 10 x y + 4 x y + x )/32 >= 6 5 2 2 4 (2 z + (8 y + 8 x) z + (15 y + 20 x y + 15 x ) z 3 2 2 3 3 + (20 y + 20 x y + 20 x y + 20 x ) z 4 3 3 4 2 + (15 y + 20 x y + 20 x y + 15 x ) z 5 4 2 3 3 2 4 5 6 5 + (8 y + 20 x y + 20 x y + 20 x y + 20 x y + 8 x ) z + 2 y + 8 x y 2 4 3 3 4 2 5 6 + 15 x y + 20 x y + 15 x y + 8 x y + 2 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 2 z + 8 y z + 8 x z + 20 y z + 10 x y z + 20 x z + 26 y z 2 3 2 3 3 3 4 2 3 2 2 2 2 + 14 x y z + 14 x y z + 26 x z + 20 y z + 14 x y z + 18 x y z 3 2 4 2 5 4 2 3 3 2 + 14 x y z + 20 x z + 8 y z + 10 x y z + 14 x y z + 14 x y z 4 5 6 5 2 4 3 3 4 2 5 + 10 x y z + 8 x z + 2 y + 8 x y + 20 x y + 26 x y + 20 x y + 8 x y 6 6 5 5 2 4 4 2 4 3 3 + 2 x >= 2 z + 8 y z + 8 x z + 15 y z + 20 x y z + 15 x z + 20 y z 2 3 2 3 3 3 4 2 3 2 3 2 + 20 x y z + 20 x y z + 20 x z + 15 y z + 20 x y z + 20 x y z 4 2 5 4 2 3 3 2 4 5 + 15 x z + 8 y z + 20 x y z + 20 x y z + 20 x y z + 20 x y z + 8 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 8 x y + 15 x y + 20 x y + 15 x y + 8 x y + 2 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 2 2 2 4 2 5 y z + 5 x z + 6 y z + 6 x z + 5 y z + 18 x y z + 5 x z 2 4 3 3 4 2 4 2 3 2 3 3 2 + 5 x y + 6 x y + 5 x y >= 10 x y z + 6 x y z + 6 x y z + 6 x y z 3 2 4 2 3 3 2 4 + 6 x y z + 10 x y z + 6 x y z + 6 x y z + 10 x y z Expressing in terms of symmetric polynomials gives: 5 {4, 2, 0} + 3 {3, 3, 0} + 3 {2, 2, 2} >= 5 {4, 1, 1} + 6 {3, 2, 1} This follows from the following majorizations: 3 {3, 3, 0} + 3 {2, 2, 2} >= 6 {3, 2, 1} 5 {4, 2, 0} >= 5 {4, 1, 1} (d15) true (c16) /* 1.11 */ /* trineq(csum(a^2*b*(a-b))>=0); */ /* 1.12 */ trineq(64*s^3*cprod(s-a)<=27*a^2*b^2*c^2); 2 2 2 3 To prove: 27 a b c >= 64 s (s - a) (s - b) (s - c) Expanding and collecting terms of the same sign gives: 5 5 5 3 2 2 2 64 c s + 64 b s + 64 a s + 64 a b c s + 27 a b c >= 6 4 4 4 64 s + 64 b c s + 64 a c s + 64 a b s Let s = (c+b+a)/2 . We get: 6 5 2 2 4 2 c + (12 b + 12 a) c + (30 b + 68 a b + 30 a ) c 3 2 2 3 3 + (40 b + 144 a b + 144 a b + 40 a ) c 4 3 2 2 3 4 2 + (30 b + 144 a b + 255 a b + 144 a b + 30 a ) c 5 4 2 3 3 2 4 5 6 + (12 b + 68 a b + 144 a b + 144 a b + 68 a b + 12 a ) c + 2 b 5 2 4 3 3 4 2 5 6 + 12 a b + 30 a b + 40 a b + 30 a b + 12 a b + 2 a >= 6 5 2 2 4 c + (10 b + 10 a) c + (31 b + 66 a b + 31 a ) c 3 2 2 3 3 + (44 b + 148 a b + 148 a b + 44 a ) c 4 3 2 2 3 4 2 + (31 b + 148 a b + 234 a b + 148 a b + 31 a ) c 5 4 2 3 3 2 4 5 6 5 + (10 b + 66 a b + 148 a b + 148 a b + 66 a b + 10 a ) c + b + 10 a b 2 4 3 3 4 2 5 6 + 31 a b + 44 a b + 31 a b + 10 a b + a Expanding and collecting terms of the same sign gives: 6 5 5 4 2 2 2 5 4 4 c + 2 b c + 2 a c + 2 a b c + 21 a b c + 2 b c + 2 a b c + 2 a b c 5 6 5 5 6 + 2 a c + b + 2 a b + 2 a b + a >= 2 4 2 4 3 3 2 3 2 3 3 3 4 2 3 2 b c + a c + 4 b c + 4 a b c + 4 a b c + 4 a c + b c + 4 a b c 3 2 4 2 2 3 3 2 2 4 3 3 4 2 + 4 a b c + a c + 4 a b c + 4 a b c + a b + 4 a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 6 5 2 2 4 (3 z + (13 y + 13 x) z + (38 y + 51 x y + 38 x ) z 3 2 2 3 3 + (57 y + 97 x y + 97 x y + 57 x ) z 4 3 2 2 3 4 2 + (38 y + 97 x y + 123 x y + 97 x y + 38 x ) z 5 4 2 3 3 2 4 5 6 5 + (13 y + 51 x y + 97 x y + 97 x y + 51 x y + 13 x ) z + 3 y + 13 x y 2 4 3 3 4 2 5 6 + 38 x y + 57 x y + 38 x y + 13 x y + 3 x )/32 >= 6 5 2 2 4 (6 z + (26 y + 26 x) z + (49 y + 112 x y + 49 x ) z 3 2 2 3 3 + (60 y + 224 x y + 224 x y + 60 x ) z 4 3 2 2 3 4 2 + (49 y + 224 x y + 360 x y + 224 x y + 49 x ) z 5 4 2 3 3 2 4 5 6 + (26 y + 112 x y + 224 x y + 224 x y + 112 x y + 26 x ) z + 6 y 5 2 4 3 3 4 2 5 6 + 26 x y + 49 x y + 60 x y + 49 x y + 26 x y + 6 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 6 z + 26 y z + 26 x z + 76 y z + 102 x y z + 76 x z + 114 y z 2 3 2 3 3 3 4 2 3 2 + 194 x y z + 194 x y z + 114 x z + 76 y z + 194 x y z 2 2 2 3 2 4 2 5 4 2 3 + 246 x y z + 194 x y z + 76 x z + 26 y z + 102 x y z + 194 x y z 3 2 4 5 6 5 2 4 3 3 + 194 x y z + 102 x y z + 26 x z + 6 y + 26 x y + 76 x y + 114 x y 4 2 5 6 6 5 5 2 4 + 76 x y + 26 x y + 6 x >= 6 z + 26 y z + 26 x z + 49 y z 4 2 4 3 3 2 3 2 3 3 3 + 112 x y z + 49 x z + 60 y z + 224 x y z + 224 x y z + 60 x z 4 2 3 2 2 2 2 3 2 4 2 5 + 49 y z + 224 x y z + 360 x y z + 224 x y z + 49 x z + 26 y z 4 2 3 3 2 4 5 6 + 112 x y z + 224 x y z + 224 x y z + 112 x y z + 26 x z + 6 y 5 2 4 3 3 4 2 5 6 + 26 x y + 49 x y + 60 x y + 49 x y + 26 x y + 6 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 27 y z + 27 x z + 54 y z + 54 x z + 27 y z + 27 x z + 27 x y 3 3 4 2 4 2 3 2 3 3 2 + 54 x y + 27 x y >= 10 x y z + 30 x y z + 30 x y z + 30 x y z 2 2 2 3 2 4 2 3 3 2 4 + 114 x y z + 30 x y z + 10 x y z + 30 x y z + 30 x y z + 10 x y z Expressing in terms of symmetric polynomials gives: 27 {4, 2, 0} + 27 {3, 3, 0} >= 5 {4, 1, 1} + 30 {3, 2, 1} + 19 {2, 2, 2} This follows from the following majorizations: 5 {4, 2, 0} >= 5 {4, 1, 1} 22 {4, 2, 0} >= 22 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} 19 {3, 3, 0} >= 19 {2, 2, 2} (d16) true (c17) /* 1.14 */ trineq(2*s/(a*b*c)<=csum(1/a^2)); 1 1 1 2 s To prove: -- + -- + -- >= ----- 2 2 2 a b c c b a 2 2 2 Multiplying both sides by a b c gives: 2 2 2 2 2 2 b c + a c + a b >= 2 a b c s Let s = (c+b+a)/2 . We get: 2 2 2 2 2 2 2 2 (b + a ) c + a b >= a b c + (a b + a b) c Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (z + (2 y + 2 x) z + (3 y + 8 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (2 y + 8 x y + 8 x y + 2 x ) z + y + 2 x y + 3 x y + 2 x y + x ) 3 2 2 2 3 2 2 3 /16 >= ((y + x) z + (2 y + 4 x y + 2 x ) z + (y + 4 x y + 4 x y + x ) z 3 2 2 3 + x y + 2 x y + x y)/8 Multiplying both sides by 16 gives: 4 3 3 2 2 2 2 2 3 2 z + 2 y z + 2 x z + 3 y z + 8 x y z + 3 x z + 2 y z + 8 x y z 2 3 4 3 2 2 3 4 + 8 x y z + 2 x z + y + 2 x y + 3 x y + 2 x y + x >= 3 3 2 2 2 2 2 3 2 2 2 y z + 2 x z + 4 y z + 8 x y z + 4 x z + 2 y z + 8 x y z + 8 x y z 3 3 2 2 3 + 2 x z + 2 x y + 4 x y + 2 x y Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 z + y + x >= y z + x z + x y Expressing in terms of symmetric polynomials gives: {4, 0, 0} >= {2, 2, 0} This result follows from the majorization theorem. (d17) true (c18) /* 1.15 */ trineq(csum(1/(s-a))>=9/s); 1 1 1 9 To prove: ----- + ----- + ----- >= - s - c s - b s - a s Expanding and collecting terms of the same sign gives: 2 7 c s ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 2 7 b s + ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 2 7 a s + ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 9 a b c + ------------------------------------------------------------ >= 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 3 6 s ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 8 b c s + ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 8 a c s + ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s 8 a b s + ------------------------------------------------------------ 4 3 3 3 2 2 2 s - c s - b s - a s + b c s + a c s + a b s - a b c s Multiplying both sides by s (s - a) (s - b) (s - c) gives: 2 2 2 3 7 c s + 7 b s + 7 a s + 9 a b c >= 6 s + 8 b c s + 8 a c s + 8 a b s Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 (7 c + (21 b + 21 a) c + (21 b + 78 a b + 21 a ) c + 7 b + 21 a b 2 3 3 2 2 2 + 21 a b + 7 a )/4 >= (3 c + (25 b + 25 a) c + (25 b + 66 a b + 25 a ) c 3 2 2 3 + 3 b + 25 a b + 25 a b + 3 a )/4 Multiplying both sides by 4 gives: 3 2 2 2 2 3 2 7 c + 21 b c + 21 a c + 21 b c + 78 a b c + 21 a c + 7 b + 21 a b 2 3 3 2 2 2 2 + 21 a b + 7 a >= 3 c + 25 b c + 25 a c + 25 b c + 66 a b c + 25 a c 3 2 2 3 + 3 b + 25 a b + 25 a b + 3 a Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 4 c + 12 a b c + 4 b + 4 a >= 4 b c + 4 a c + 4 b c + 4 a c + 4 a b 2 + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 z + (3 y + 3 x) z + (3 y + 3 x y + 3 x ) z + y + 3 x y + 3 x y + x >= 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/2 Multiplying both sides by 2 gives: 3 2 2 2 2 3 2 2 2 z + 6 y z + 6 x z + 6 y z + 6 x y z + 6 x z + 2 y + 6 x y + 6 x y 3 3 2 2 2 2 3 2 + 2 x >= 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y 2 3 + 5 x y + 2 x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 y z + x z + y z + x z + x y + x y >= 6 x y z Expressing in terms of symmetric polynomials gives: {2, 1, 0} >= {1, 1, 1} This result follows from the majorization theorem. (d18) true (c19) /* 1.16 */ trineq(3/2<=csum(a/(b+c))); a b c 3 To prove: ----- + ----- + ----- >= - c + b c + a b + a 2 Expanding and collecting terms of the same sign gives: 3 2 c ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 3 2 b + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 3 2 a + ------------------------------------------------------------- >= 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 b c ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 a c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 b c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 a c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 a b + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 a b + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b Multiplying both sides by 2 (b + a) (c + a) (c + b) gives: 3 3 3 2 2 2 2 2 2 2 c + 2 b + 2 a >= b c + a c + b c + a c + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 2 z + (3 y + 3 x) z + (3 y + 3 x ) z + 2 y + 3 x y + 3 x y + 2 x ----------------------------------------------------------------------- >= 4 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 3 4 z + 6 y z + 6 x z + 6 y z + 6 x z + 4 y + 6 x y + 6 x y + 4 x >= 3 2 2 2 2 3 2 2 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y + 5 x y 3 + 2 x Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 2 z + y z + x z + y z + x z + 2 y + x y + x y + 2 x >= 12 x y z Expressing in terms of symmetric polynomials gives: {3, 0, 0} + {2, 1, 0} >= 2 {1, 1, 1} This follows from the following majorizations: {2, 1, 0} >= {1, 1, 1} {3, 0, 0} >= {1, 1, 1} (d19) true (c20) trineq(csum(a/(b+c))<2); a b c To prove: 2 > ----- + ----- + ----- c + b c + a b + a Expanding and collecting terms of the same sign gives: 2 b c ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 2 a c + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 2 b c + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b a b c + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 2 a c + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 2 a b + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 2 a b + ------------------------------------------------- > 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 3 c ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 3 b + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b 3 a + ------------------------------------------------- 2 2 2 2 2 2 b c + a c + b c + 2 a b c + a c + a b + a b Multiplying both sides by (b + a) (c + a) (c + b) gives: 2 2 2 2 2 2 3 3 3 b c + a c + b c + a b c + a c + a b + a b > c + b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 z + (3 y + 3 x) z + (3 y + 7 x y + 3 x ) z + y + 3 x y + 3 x y + x ------------------------------------------------------------------------- > 4 3 2 2 2 3 2 2 3 2 z + (3 y + 3 x) z + (3 y + 3 x ) z + 2 y + 3 x y + 3 x y + 2 x ----------------------------------------------------------------------- 8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 2 z + 6 y z + 6 x z + 6 y z + 14 x y z + 6 x z + 2 y + 6 x y + 6 x y 3 3 2 2 2 2 3 2 2 + 2 x > 2 z + 3 y z + 3 x z + 3 y z + 3 x z + 2 y + 3 x y + 3 x y 3 + 2 x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 3 y z + 3 x z + 3 y z + 14 x y z + 3 x z + 3 x y + 3 x y > 0 This is true because a sum of positive terms must be positive. (d20) true (c21) /* 1.17 */ trineq(15/4<=csum((s+a)/(b+c))); s + c s + b s + a 15 To prove: ----- + ----- + ----- >= -- b + a c + a c + b 4 Expanding and collecting terms of the same sign gives: 2 4 c s ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 12 b c s + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 12 a c s + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 4 b s + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 12 a b s + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 4 a s + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 3 4 c + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 3 4 b + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 3 4 a + ------------------------------------------------------------- >= 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 11 b c ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 11 a c + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 11 b c + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 18 a b c + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 11 a c + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 11 a b + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b 2 11 a b + ------------------------------------------------------------- 2 2 2 2 2 2 4 b c + 4 a c + 4 b c + 8 a b c + 4 a c + 4 a b + 4 a b Multiplying both sides by 4 (b + a) (c + a) (c + b) gives: 2 2 2 3 3 4 c s + 12 b c s + 12 a c s + 4 b s + 12 a b s + 4 a s + 4 c + 4 b 3 2 2 2 2 2 2 + 4 a >= 11 b c + 11 a c + 11 b c + 18 a b c + 11 a c + 11 a b + 11 a b Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 2 6 c + (8 b + 8 a) c + (8 b + 18 a b + 8 a ) c + 6 b + 8 a b + 8 a b 3 2 2 2 2 2 + 6 a >= (11 b + 11 a) c + (11 b + 18 a b + 11 a ) c + 11 a b + 11 a b Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 6 c + 6 b + 6 a >= 3 b c + 3 a c + 3 b c + 3 a c + 3 a b + 3 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 6 z + (9 y + 9 x) z + (9 y + 9 x ) z + 6 y + 9 x y + 9 x y + 6 x ----------------------------------------------------------------------- >= 4 3 2 2 2 3 2 (6 z + (15 y + 15 x) z + (15 y + 36 x y + 15 x ) z + 6 y + 15 x y 2 3 + 15 x y + 6 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 12 z + 18 y z + 18 x z + 18 y z + 18 x z + 12 y + 18 x y + 18 x y 3 3 2 2 2 2 3 + 12 x >= 6 z + 15 y z + 15 x z + 15 y z + 36 x y z + 15 x z + 6 y 2 2 3 + 15 x y + 15 x y + 6 x Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 6 z + 3 y z + 3 x z + 3 y z + 3 x z + 6 y + 3 x y + 3 x y + 6 x >= 36 x y z Dividing both sides by 3 gives: 3 2 2 2 2 3 2 2 3 2 z + y z + x z + y z + x z + 2 y + x y + x y + 2 x >= 12 x y z Expressing in terms of symmetric polynomials gives: {3, 0, 0} + {2, 1, 0} >= 2 {1, 1, 1} This follows from the following majorizations: {2, 1, 0} >= {1, 1, 1} {3, 0, 0} >= {1, 1, 1} (d21) true (c22) trineq(csum((s+a)/(b+c))<9/2); 9 s + c s + b s + a To prove: - > ----- + ----- + ----- 2 b + a c + a c + b Expanding and collecting terms of the same sign gives: 2 7 b c ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 7 a c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 7 b c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 12 a b c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 7 a c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 7 a b + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 7 a b + ------------------------------------------------------------- > 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 2 c s ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 6 b c s + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 6 a c s + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 2 b s + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 6 a b s + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 2 2 a s + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 3 2 c + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 3 2 b + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b 3 2 a + ------------------------------------------------------------- 2 2 2 2 2 2 2 b c + 2 a c + 2 b c + 4 a b c + 2 a c + 2 a b + 2 a b Multiplying both sides by 2 (b + a) (c + a) (c + b) gives: 2 2 2 2 2 2 7 b c + 7 a c + 7 b c + 12 a b c + 7 a c + 7 a b + 7 a b > 2 2 2 3 3 3 2 c s + 6 b c s + 6 a c s + 2 b s + 6 a b s + 2 a s + 2 c + 2 b + 2 a Let s = (c+b+a)/2 . We get: 2 2 2 2 2 (7 b + 7 a) c + (7 b + 12 a b + 7 a ) c + 7 a b + 7 a b > 3 2 2 2 3 2 2 3 3 c + (4 b + 4 a) c + (4 b + 9 a b + 4 a ) c + 3 b + 4 a b + 4 a b + 3 a Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 3 b c + 3 a c + 3 b c + 3 a b c + 3 a c + 3 a b + 3 a b > 3 3 3 3 c + 3 b + 3 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 (3 z + (9 y + 9 x) z + (9 y + 21 x y + 9 x ) z + 3 y + 9 x y + 9 x y 3 + 3 x )/4 > 3 2 2 2 3 2 2 3 6 z + (9 y + 9 x) z + (9 y + 9 x ) z + 6 y + 9 x y + 9 x y + 6 x ----------------------------------------------------------------------- 8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 6 z + 18 y z + 18 x z + 18 y z + 42 x y z + 18 x z + 6 y + 18 x y 2 3 3 2 2 2 2 3 2 + 18 x y + 6 x > 6 z + 9 y z + 9 x z + 9 y z + 9 x z + 6 y + 9 x y 2 3 + 9 x y + 6 x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 9 y z + 9 x z + 9 y z + 42 x y z + 9 x z + 9 x y + 9 x y > 0 This is true because a sum of positive terms must be positive. (d22) true (c23) /* 1.19 */ trineq(1/3<=csum(a^2)/csum(a)^2); 2 2 2 c + b + a 1 To prove: ------------ >= - 2 3 (c + b + a) Expanding and collecting terms of the same sign gives: 2 2 c ------------------------------------------ 2 2 2 3 c + 6 b c + 6 a c + 3 b + 6 a b + 3 a 2 2 b + ------------------------------------------ 2 2 2 3 c + 6 b c + 6 a c + 3 b + 6 a b + 3 a 2 2 a + ------------------------------------------ >= 2 2 2 3 c + 6 b c + 6 a c + 3 b + 6 a b + 3 a 2 b c ------------------------------------------ 2 2 2 3 c + 6 b c + 6 a c + 3 b + 6 a b + 3 a 2 a c + ------------------------------------------ 2 2 2 3 c + 6 b c + 6 a c + 3 b + 6 a b + 3 a 2 a b + ------------------------------------------ 2 2 2 3 c + 6 b c + 6 a c + 3 b + 6 a b + 3 a 2 Multiplying both sides by 3 (c + b + a) gives: 2 2 2 2 c + 2 b + 2 a >= 2 b c + 2 a c + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 2 2 2 2 z + (3 y + 3 x) z + y + 3 x y + x z + (y + x) z + y + x y + x >= ------------------------------------ 2 Multiplying both sides by 2 gives: 2 2 2 2 z + 2 y z + 2 x z + 2 y + 2 x y + 2 x >= 2 2 2 z + 3 y z + 3 x z + y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 z + y + x >= y z + x z + x y Expressing in terms of symmetric polynomials gives: {2, 0, 0} >= {1, 1, 0} This result follows from the majorization theorem. (d23) true (c24) trineq(csum(a^2)/csum(a)^2<1/2); 2 2 2 1 c + b + a To prove: - > ------------ 2 2 (c + b + a) Expanding and collecting terms of the same sign gives: 2 b c ------------------------------------------ 2 2 2 2 c + 4 b c + 4 a c + 2 b + 4 a b + 2 a 2 a c + ------------------------------------------ 2 2 2 2 c + 4 b c + 4 a c + 2 b + 4 a b + 2 a 2 a b + ------------------------------------------ > 2 2 2 2 c + 4 b c + 4 a c + 2 b + 4 a b + 2 a 2 c ------------------------------------------ 2 2 2 2 c + 4 b c + 4 a c + 2 b + 4 a b + 2 a 2 b + ------------------------------------------ 2 2 2 2 c + 4 b c + 4 a c + 2 b + 4 a b + 2 a 2 a + ------------------------------------------ 2 2 2 2 c + 4 b c + 4 a c + 2 b + 4 a b + 2 a 2 Multiplying both sides by 2 (c + b + a) gives: 2 2 2 2 b c + 2 a c + 2 a b > c + b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 2 2 2 2 z + (3 y + 3 x) z + y + 3 x y + x z + (y + x) z + y + x y + x ------------------------------------ > ------------------------------ 2 2 Multiplying both sides by 2 gives: 2 2 2 2 2 2 z + 3 y z + 3 x z + y + 3 x y + x > z + y z + x z + y + x y + x Expanding and collecting terms of the same sign gives: 2 y z + 2 x z + 2 x y > 0 This is true because a sum of positive terms must be positive. (d24) true (c25) /* 1.22 */ trineq(csum(a^2)*csum(b^3*c^3)<2*csum(a^5)*csum(a^3)); 3 3 3 5 5 5 To prove: 2 (c + b + a ) (c + b + a ) > 2 2 2 3 3 3 3 3 3 (c + b + a ) (b c + a c + a b ) Expanding and collecting terms of the same sign gives: 8 3 5 3 5 5 3 5 3 8 3 5 5 3 8 2 c + b c + a c + b c + a c + 2 b + a b + a b + 2 a > 2 3 3 3 2 3 3 3 2 a b c + a b c + a b c Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 8 7 2 2 6 (6 z + (24 y + 24 x) z + (69 y + 30 x y + 69 x ) z 3 2 2 3 5 + (125 y + 51 x y + 51 x y + 125 x ) z 4 3 2 2 3 4 4 + (150 y + 55 x y + 90 x y + 55 x y + 150 x ) z 5 4 2 3 3 2 4 5 3 + (125 y + 55 x y + 100 x y + 100 x y + 55 x y + 125 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (69 y + 51 x y + 90 x y + 100 x y + 90 x y + 51 x y + 69 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (24 y + 30 x y + 51 x y + 55 x y + 55 x y + 51 x y + 30 x y 7 8 7 2 6 3 5 4 4 5 3 + 24 x ) z + 6 y + 24 x y + 69 x y + 125 x y + 150 x y + 125 x y 6 2 7 8 2 2 6 + 69 x y + 24 x y + 6 x )/256 > ((y + 2 x y + x ) z 3 2 2 3 5 + (5 y + 15 x y + 15 x y + 5 x ) z 4 3 2 2 3 4 4 + (8 y + 35 x y + 54 x y + 35 x y + 8 x ) z 5 4 2 3 3 2 4 5 3 + (5 y + 35 x y + 80 x y + 80 x y + 35 x y + 5 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (y + 15 x y + 54 x y + 80 x y + 54 x y + 15 x y + x ) z 6 2 5 3 4 4 3 5 2 6 2 6 + (2 x y + 15 x y + 35 x y + 35 x y + 15 x y + 2 x y) z + x y 3 5 4 4 5 3 6 2 + 5 x y + 8 x y + 5 x y + x y )/256 Multiplying both sides by 256 gives: 8 7 7 2 6 6 2 6 3 5 6 z + 24 y z + 24 x z + 69 y z + 30 x y z + 69 x z + 125 y z 2 5 2 5 3 5 4 4 3 4 2 2 4 + 51 x y z + 51 x y z + 125 x z + 150 y z + 55 x y z + 90 x y z 3 4 4 4 5 3 4 3 2 3 3 + 55 x y z + 150 x z + 125 y z + 55 x y z + 100 x y z 3 2 3 4 3 5 3 6 2 5 2 2 4 2 + 100 x y z + 55 x y z + 125 x z + 69 y z + 51 x y z + 90 x y z 3 3 2 4 2 2 5 2 6 2 7 6 + 100 x y z + 90 x y z + 51 x y z + 69 x z + 24 y z + 30 x y z 2 5 3 4 4 3 5 2 6 7 + 51 x y z + 55 x y z + 55 x y z + 51 x y z + 30 x y z + 24 x z 8 7 2 6 3 5 4 4 5 3 6 2 + 6 y + 24 x y + 69 x y + 125 x y + 150 x y + 125 x y + 69 x y 7 8 2 6 6 2 6 3 5 2 5 + 24 x y + 6 x > y z + 2 x y z + x z + 5 y z + 15 x y z 2 5 3 5 4 4 3 4 2 2 4 3 4 + 15 x y z + 5 x z + 8 y z + 35 x y z + 54 x y z + 35 x y z 4 4 5 3 4 3 2 3 3 3 2 3 4 3 + 8 x z + 5 y z + 35 x y z + 80 x y z + 80 x y z + 35 x y z 5 3 6 2 5 2 2 4 2 3 3 2 4 2 2 + 5 x z + y z + 15 x y z + 54 x y z + 80 x y z + 54 x y z 5 2 6 2 6 2 5 3 4 4 3 + 15 x y z + x z + 2 x y z + 15 x y z + 35 x y z + 35 x y z 5 2 6 2 6 3 5 4 4 5 3 6 2 + 15 x y z + 2 x y z + x y + 5 x y + 8 x y + 5 x y + x y Expanding and collecting terms of the same sign gives: 8 7 7 2 6 6 2 6 3 5 6 z + 24 y z + 24 x z + 68 y z + 28 x y z + 68 x z + 120 y z 2 5 2 5 3 5 4 4 3 4 2 2 4 + 36 x y z + 36 x y z + 120 x z + 142 y z + 20 x y z + 36 x y z 3 4 4 4 5 3 4 3 2 3 3 3 2 3 + 20 x y z + 142 x z + 120 y z + 20 x y z + 20 x y z + 20 x y z 4 3 5 3 6 2 5 2 2 4 2 3 3 2 + 20 x y z + 120 x z + 68 y z + 36 x y z + 36 x y z + 20 x y z 4 2 2 5 2 6 2 7 6 2 5 + 36 x y z + 36 x y z + 68 x z + 24 y z + 28 x y z + 36 x y z 3 4 4 3 5 2 6 7 8 7 + 20 x y z + 20 x y z + 36 x y z + 28 x y z + 24 x z + 6 y + 24 x y 2 6 3 5 4 4 5 3 6 2 7 8 + 68 x y + 120 x y + 142 x y + 120 x y + 68 x y + 24 x y + 6 x > 0 This is true because a sum of positive terms must be positive. (d25) true (c26) /* 1.23 */ trineq(csum(a)^3<=5*csum(a*b*(a+b))-3*a*b*c); 3 To prove: 5 (b c (c + b) + a c (c + a) + a b (b + a)) - 3 a b c >= (c + b + a) Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 3 3 3 2 b c + 2 a c + 2 b c + 2 a c + 2 a b + 2 a b >= c + 9 a b c + b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/4 >= 3 2 2 2 3 2 2 3 z + (6 y + 6 x) z + (6 y + 9 x y + 6 x ) z + y + 6 x y + 6 x y + x ------------------------------------------------------------------------- 4 Multiplying both sides by 4 gives: 3 2 2 2 2 3 2 2 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y + 5 x y 3 3 2 2 2 2 3 2 + 2 x >= z + 6 y z + 6 x z + 6 y z + 9 x y z + 6 x z + y + 6 x y 2 3 + 6 x y + x Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 z + 3 x y z + y + x >= y z + x z + y z + x z + x y + x y Expressing in terms of symmetric polynomials gives: {3, 0, 0} + {1, 1, 1} >= 2 {2, 1, 0} This follows from the following majorizations: {3, 0, 0} + {1, 1, 1} >= 2 {2, 1, 0} (d26) true (c27) print("Summary:") $ Summary: (c28) print("Proved",triangtrue,"inequalities out of",triangcount,".") $ Proved 23 inequalities out of 23 . (d29) BATCH DONE (c30)