DOE MACSYMA Version 10. (c1) Batching the file triang Batching done. (d1) triang (c2) (c3) /* */ showproof: true $ (c4) /* 2.1 */ trineq(csum(sin(A))<=3*sqrt(3)/2); 3 sqrt(3) To prove: --------- >= sin(C) + sin(B) + sin(A) 2 Removing the trigonometric expressions gives: 3 sqrt(3) 2 K c + 2 K b + 2 K a --------- >= --------------------- 2 a b c Multiplying both sides by 2 a b c gives: 3 sqrt(3) a b c >= 4 K c + 4 K b + 4 K a Since 4 c + 4 b + 4 a is positive, and since 3 sqrt(3) a b c is positive, we can square both sides to get: 2 2 2 2 2 2 4 27 a b c >= (16 c + (32 b + 32 a) c + 16 b + 32 a b + 16 a ) s 3 2 2 2 3 + (- 16 c + (- 48 b - 48 a) c + (- 48 b - 96 a b - 48 a ) c - 16 b 2 2 3 3 3 - 48 a b - 48 a b - 16 a ) s + ((16 b + 16 a) c 2 2 2 3 2 2 3 + (32 b + 80 a b + 32 a ) c + (16 b + 80 a b + 80 a b + 16 a ) c 3 2 2 3 2 3 2 2 2 + 16 a b + 32 a b + 16 a b) s + (- 16 a b c + (- 32 a b - 32 a b) c 3 2 2 3 + (- 16 a b - 32 a b - 16 a b) c) s Expanding and collecting terms of the same sign gives: 3 3 2 3 2 3 2 3 3 2 3 16 c s + 48 b c s + 48 a c s + 48 b c s + 96 a b c s + 48 a c s 3 3 2 3 2 3 3 3 3 2 2 + 16 b s + 48 a b s + 48 a b s + 16 a s + 16 a b c s + 32 a b c s 2 2 3 2 2 3 2 2 2 + 32 a b c s + 16 a b c s + 32 a b c s + 16 a b c s + 27 a b c >= 2 4 4 4 2 4 4 2 4 3 2 16 c s + 32 b c s + 32 a c s + 16 b s + 32 a b s + 16 a s + 16 b c s 3 2 2 2 2 2 2 2 2 2 3 2 + 16 a c s + 32 b c s + 80 a b c s + 32 a c s + 16 b c s 2 2 2 2 3 2 3 2 2 2 2 + 80 a b c s + 80 a b c s + 16 a c s + 16 a b s + 32 a b s 3 2 + 16 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} (d4) true (c5) /* 2.3 */ trineq(csum(sin(A)^2)<=9/4); 9 2 2 2 To prove: - >= sin (C) + sin (B) + sin (A) 4 Removing the trigonometric expressions gives: 2 2 2 2 2 2 9 4 K c + 4 K b + 4 K a - >= --------------------------- 4 2 2 2 a b c 2 2 2 Multiplying both sides by 4 a b c gives: 2 2 2 2 2 2 2 2 2 9 a b c >= 16 K c + 16 K b + 16 K a Replacing K^2 by F^2 gives: 2 2 2 2 2 2 2 2 2 9 a b c >= 16 F c + 16 F b + 16 F a Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 2 6 2 2 4 4 2 2 4 2 6 2 4 4 2 9 a b c >= - c + (b + a ) c + (b + 6 a b + a ) c - b + a b + a b 6 - a Expanding and collecting terms of the same sign gives: 6 2 2 2 6 6 2 4 2 4 4 2 4 2 2 4 4 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: 6 5 2 2 4 (z + (3 y + 3 x) z + (9 y + 3 x y + 9 x ) z 3 2 2 3 3 + (13 y + 9 x y + 9 x y + 13 x ) z 4 3 2 2 3 4 2 + (9 y + 9 x y + 15 x y + 9 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (3 y + 3 x y + 9 x y + 9 x y + 3 x y + 3 x ) z + y + 3 x y 2 4 3 3 4 2 5 6 + 9 x y + 13 x y + 9 x y + 3 x y + x )/32 >= 6 5 2 2 4 (2 z + (6 y + 6 x) z + (9 y + 20 x y + 9 x ) z 3 2 2 3 3 + (8 y + 28 x y + 28 x y + 8 x ) z 4 3 2 2 3 4 2 + (9 y + 28 x y + 36 x y + 28 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (6 y + 20 x y + 28 x y + 28 x y + 20 x y + 6 x ) z + 2 y + 6 x y 2 4 3 3 4 2 5 6 + 9 x y + 8 x y + 9 x y + 6 x y + 2 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 18 y z + 6 x y z + 18 x z + 26 y z + 18 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 18 x y z + 26 x z + 18 y z + 18 x y z + 30 x y z + 18 x y z 4 2 5 4 2 3 3 2 4 5 + 18 x z + 6 y z + 6 x y z + 18 x y z + 18 x y z + 6 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 18 x y + 26 x y + 18 x y + 6 x y + 2 x >= 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 9 y z + 20 x y z + 9 x z + 8 y z + 28 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 28 x y z + 8 x z + 9 y z + 28 x y z + 36 x y z + 28 x y z 4 2 5 4 2 3 3 2 4 5 + 9 x z + 6 y z + 20 x y z + 28 x y z + 28 x y z + 20 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 9 x y + 8 x y + 9 x y + 6 x y + 2 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 9 y z + 9 x z + 18 y z + 18 x z + 9 y z + 9 x z + 9 x y 3 3 4 2 4 2 3 2 3 3 2 + 18 x y + 9 x y >= 14 x y z + 10 x y z + 10 x y z + 10 x y z 2 2 2 3 2 4 2 3 3 2 4 + 6 x y z + 10 x y z + 14 x y z + 10 x y z + 10 x y z + 14 x y z Expressing in terms of symmetric polynomials gives: 9 {4, 2, 0} + 9 {3, 3, 0} >= 7 {4, 1, 1} + 10 {3, 2, 1} + {2, 2, 2} This follows from the following majorizations: 7 {4, 2, 0} >= 7 {4, 1, 1} 2 {4, 2, 0} >= 2 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} {3, 3, 0} >= {2, 2, 2} (d5) true (c6) /* 2.4 */ trineq(csum(sin(A))>=csum(sin(2*A))); To prove: sin(C) + sin(B) + sin(A) >= sin(2 C) + sin(2 B) + sin(2 A) Expanding the trigonometric expressions gives: sin(C) + sin(B) + sin(A) >= 2 sin(C) cos(C) + 2 sin(B) cos(B) + 2 sin(A) cos(A) Removing the trigonometric expressions gives: 2 K c + 2 K b + 2 K a --------------------- >= a b c 4 2 2 2 4 2 2 4 2 K c + (- 4 K b - 4 K a ) c + 2 K b - 4 K a b + 2 K a - ------------------------------------------------------------- 2 2 2 a b c 2 2 2 Multiplying both sides by a b c gives: 2 2 2 2 K a b c + 2 K a b c + 2 K a b c >= 4 2 2 2 2 4 2 2 4 - 2 K c + 4 K b c + 4 K a c - 2 K b + 4 K a b - 2 K a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 2 K c + 2 K a b c + 2 K a b c + 2 K a b c + 2 K b + 2 K a >= 2 2 2 2 2 2 4 K b c + 4 K a c + 4 K a b Dividing both sides by 2 K gives: 4 2 2 2 4 4 2 2 2 2 2 2 c + a b c + a b c + a b c + b + 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: 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 + (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 )/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 + 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 Expanding and collecting terms of the same sign gives: 3 3 2 2 2 2 3 3 3 2 2 3 y z + x z + 2 y z + 2 x z + y z + x z + x y + 2 x y + x y >= 2 2 2 4 x y z + 4 x y z + 4 x y z Dividing both sides by z + y + x gives: 2 2 2 2 2 2 y z + x z + y z - 2 x y z + x z + x y + x y >= 4 x y z 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. (d6) true (c7) /* 2.7 */ trineq(cprod(sin(A))<=3*sqrt(3)/8); 3 sqrt(3) To prove: --------- >= sin(A) sin(B) sin(C) 8 Removing the trigonometric expressions gives: 3 3 sqrt(3) 8 K --------- >= -------- 8 2 2 2 a b c 2 2 2 Multiplying both sides by 8 a b c gives: 2 2 2 3 3 sqrt(3) a b c >= 64 K Replacing K^2 by F^2 gives: 2 2 2 2 3 sqrt(3) a b c >= 64 F K 2 Since 64 F is positive, and since 2 2 2 3 sqrt(3) a b c is positive, we can square both sides to get: 4 4 4 4 4 4 4 4 3 27 a b c >= 4096 F s + (- 4096 F c - 4096 F b - 4096 F a) s 4 4 4 2 4 + ((4096 F b + 4096 F a) c + 4096 F a b) s - 4096 F a b c s Expanding and collecting terms of the same sign gives: 4 3 4 3 4 3 4 4 4 4 4096 F c s + 4096 F b s + 4096 F a s + 4096 F a b c s + 27 a b c >= 4 4 4 2 4 2 4 2 4096 F s + 4096 F b c s + 4096 F a c s + 4096 F a b s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 12 11 2 2 10 3 3 9 2 c + (8 b + 8 a) c + (4 b + 32 a b + 4 a ) c + (- 24 b - 24 a ) c 4 3 2 2 3 4 8 + (- 34 b - 120 a b - 76 a b - 120 a b - 34 a ) c 5 4 2 3 3 2 4 5 7 + (16 b - 80 a b - 128 a b - 128 a b - 80 a b + 16 a ) c 6 5 2 4 3 3 4 2 5 6 6 + (56 b + 160 a b + 72 a b + 64 a b + 72 a b + 160 a b + 56 a ) c 7 6 2 5 3 4 4 3 5 2 6 + (16 b + 160 a b + 256 a b + 208 a b + 208 a b + 256 a b + 160 a b 7 5 8 7 2 6 3 5 4 4 + 16 a ) c + (- 34 b - 80 a b + 72 a b + 208 a b + 207 a b 5 3 6 2 7 8 4 + 208 a b + 72 a b - 80 a b - 34 a ) c 9 8 2 7 3 6 4 5 5 4 + (- 24 b - 120 a b - 128 a b + 64 a b + 208 a b + 208 a b 6 3 7 2 8 9 3 + 64 a b - 128 a b - 120 a b - 24 a ) c 10 2 8 3 7 4 6 5 5 6 4 7 3 + (4 b - 76 a b - 128 a b + 72 a b + 256 a b + 72 a b - 128 a b 8 2 10 2 11 10 3 8 4 7 5 6 - 76 a b + 4 a ) c + (8 b + 32 a b - 120 a b - 80 a b + 160 a b 6 5 7 4 8 3 10 11 12 11 + 160 a b - 80 a b - 120 a b + 32 a b + 8 a ) c + 2 b + 8 a b 2 10 3 9 4 8 5 7 6 6 7 5 8 4 + 4 a b - 24 a b - 34 a b + 16 a b + 56 a b + 16 a b - 34 a b 9 3 10 2 11 12 - 24 a b + 4 a b + 8 a b + 2 a >= 12 11 2 2 10 3 3 9 c + (8 b + 8 a) c + (10 b + 32 a b + 10 a ) c + (- 24 b - 24 a ) c 4 3 2 2 3 4 8 + (- 49 b - 120 a b - 94 a b - 120 a b - 49 a ) c 5 4 2 3 3 2 4 5 7 + (16 b - 80 a b - 128 a b - 128 a b - 80 a b + 16 a ) c 6 5 2 4 3 3 4 2 5 6 6 + (76 b + 160 a b + 84 a b + 64 a b + 84 a b + 160 a b + 76 a ) c 7 6 2 5 3 4 4 3 5 2 6 + (16 b + 160 a b + 256 a b + 208 a b + 208 a b + 256 a b + 160 a b 7 5 8 7 2 6 3 5 4 4 + 16 a ) c + (- 49 b - 80 a b + 84 a b + 208 a b + 186 a b 5 3 6 2 7 8 4 + 208 a b + 84 a b - 80 a b - 49 a ) c 9 8 2 7 3 6 4 5 5 4 + (- 24 b - 120 a b - 128 a b + 64 a b + 208 a b + 208 a b 6 3 7 2 8 9 3 + 64 a b - 128 a b - 120 a b - 24 a ) c 10 2 8 3 7 4 6 5 5 6 4 7 3 + (10 b - 94 a b - 128 a b + 84 a b + 256 a b + 84 a b - 128 a b 8 2 10 2 11 10 3 8 4 7 5 6 - 94 a b + 10 a ) c + (8 b + 32 a b - 120 a b - 80 a b + 160 a b 6 5 7 4 8 3 10 11 12 11 + 160 a b - 80 a b - 120 a b + 32 a b + 8 a ) c + b + 8 a b 2 10 3 9 4 8 5 7 6 6 7 5 8 4 + 10 a b - 24 a b - 49 a b + 16 a b + 76 a b + 16 a b - 49 a b 9 3 10 2 11 12 - 24 a b + 10 a b + 8 a b + a Expanding and collecting terms of the same sign gives: 12 4 8 2 2 8 4 8 8 4 4 4 4 8 4 c + 15 b c + 18 a b c + 15 a c + 15 b c + 21 a b c + 15 a c 2 8 2 8 2 2 12 4 8 8 4 12 + 18 a b c + 18 a b c + b + 15 a b + 15 a b + a >= 2 10 2 10 6 6 2 4 6 4 2 6 6 6 6 b c + 6 a c + 20 b c + 12 a b c + 12 a b c + 20 a c 2 6 4 6 2 4 10 2 4 6 2 6 4 2 10 2 + 12 a b c + 12 a b c + 6 b c + 12 a b c + 12 a b c + 6 a c 2 10 6 6 10 2 + 6 a b + 20 a b + 6 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 12 11 2 2 10 (32 z + (192 y + 192 x) z + (612 y + 1032 x y + 612 x ) z 3 2 2 3 9 + (1300 y + 2940 x y + 2940 x y + 1300 x ) z 4 3 2 2 3 4 8 + (2133 y + 5664 x y + 7542 x y + 5664 x y + 2133 x ) z 5 4 2 3 3 2 4 5 7 + (2844 y + 8508 x y + 13224 x y + 13224 x y + 8508 x y + 2844 x ) z 6 5 2 4 3 3 4 2 5 + (3150 y + 10416 x y + 18186 x y + 19152 x y + 18186 x y + 10416 x y 6 6 7 6 2 5 3 4 + 3150 x ) z + (2844 y + 10416 x y + 20160 x y + 20244 x y 4 3 5 2 6 7 5 + 20244 x y + 20160 x y + 10416 x y + 2844 x ) z 8 7 2 6 3 5 4 4 5 3 + (2133 y + 8508 x y + 18186 x y + 20244 x y + 17346 x y + 20244 x y 6 2 7 8 4 + 18186 x y + 8508 x y + 2133 x ) z 9 8 2 7 3 6 4 5 5 4 + (1300 y + 5664 x y + 13224 x y + 19152 x y + 20244 x y + 20244 x y 6 3 7 2 8 9 3 + 19152 x y + 13224 x y + 5664 x y + 1300 x ) z 10 9 2 8 3 7 4 6 5 5 + (612 y + 2940 x y + 7542 x y + 13224 x y + 18186 x y + 20160 x y 6 4 7 3 8 2 9 10 2 + 18186 x y + 13224 x y + 7542 x y + 2940 x y + 612 x ) z 11 10 2 9 3 8 4 7 5 6 + (192 y + 1032 x y + 2940 x y + 5664 x y + 8508 x y + 10416 x y 6 5 7 4 8 3 9 2 10 11 + 10416 x y + 8508 x y + 5664 x y + 2940 x y + 1032 x y + 192 x ) z 12 11 2 10 3 9 4 8 5 7 + 32 y + 192 x y + 612 x y + 1300 x y + 2133 x y + 2844 x y 6 6 7 5 8 4 9 3 10 2 11 + 3150 x y + 2844 x y + 2133 x y + 1300 x y + 612 x y + 192 x y 12 12 11 + 32 x )/4096 >= (16 z + (96 y + 96 x) z 2 2 10 3 2 2 3 + (306 y + 516 x y + 306 x ) z + (650 y + 1470 x y + 1470 x y + 650 x ) 9 4 3 2 2 3 4 8 z + (1053 y + 2778 x y + 3690 x y + 2778 x y + 1053 x ) z 5 4 2 3 3 2 4 5 7 + (1368 y + 3984 x y + 6072 x y + 6072 x y + 3984 x y + 1368 x ) z 6 5 2 4 3 3 4 2 5 + (1494 y + 4668 x y + 7662 x y + 9680 x y + 7662 x y + 4668 x y 6 6 7 6 2 5 3 4 4 3 + 1494 x ) z + (1368 y + 4668 x y + 8136 x y + 12756 x y + 12756 x y 5 2 6 7 5 + 8136 x y + 4668 x y + 1368 x ) z 8 7 2 6 3 5 4 4 5 3 + (1053 y + 3984 x y + 7662 x y + 12756 x y + 16290 x y + 12756 x y 6 2 7 8 4 + 7662 x y + 3984 x y + 1053 x ) z 9 8 2 7 3 6 4 5 5 4 + (650 y + 2778 x y + 6072 x y + 9680 x y + 12756 x y + 12756 x y 6 3 7 2 8 9 3 + 9680 x y + 6072 x y + 2778 x y + 650 x ) z 10 9 2 8 3 7 4 6 5 5 + (306 y + 1470 x y + 3690 x y + 6072 x y + 7662 x y + 8136 x y 6 4 7 3 8 2 9 10 2 + 7662 x y + 6072 x y + 3690 x y + 1470 x y + 306 x ) z 11 10 2 9 3 8 4 7 5 6 + (96 y + 516 x y + 1470 x y + 2778 x y + 3984 x y + 4668 x y 6 5 7 4 8 3 9 2 10 11 + 4668 x y + 3984 x y + 2778 x y + 1470 x y + 516 x y + 96 x ) z 12 11 2 10 3 9 4 8 5 7 + 16 y + 96 x y + 306 x y + 650 x y + 1053 x y + 1368 x y 6 6 7 5 8 4 9 3 10 2 11 + 1494 x y + 1368 x y + 1053 x y + 650 x y + 306 x y + 96 x y 12 + 16 x )/2048 Multiplying both sides by 4096 gives: 12 11 11 2 10 10 2 10 32 z + 192 y z + 192 x z + 612 y z + 1032 x y z + 612 x z 3 9 2 9 2 9 3 9 4 8 + 1300 y z + 2940 x y z + 2940 x y z + 1300 x z + 2133 y z 3 8 2 2 8 3 8 4 8 5 7 + 5664 x y z + 7542 x y z + 5664 x y z + 2133 x z + 2844 y z 4 7 2 3 7 3 2 7 4 7 5 7 + 8508 x y z + 13224 x y z + 13224 x y z + 8508 x y z + 2844 x z 6 6 5 6 2 4 6 3 3 6 + 3150 y z + 10416 x y z + 18186 x y z + 19152 x y z 4 2 6 5 6 6 6 7 5 6 5 + 18186 x y z + 10416 x y z + 3150 x z + 2844 y z + 10416 x y z 2 5 5 3 4 5 4 3 5 5 2 5 + 20160 x y z + 20244 x y z + 20244 x y z + 20160 x y z 6 5 7 5 8 4 7 4 2 6 4 + 10416 x y z + 2844 x z + 2133 y z + 8508 x y z + 18186 x y z 3 5 4 4 4 4 5 3 4 6 2 4 + 20244 x y z + 17346 x y z + 20244 x y z + 18186 x y z 7 4 8 4 9 3 8 3 2 7 3 + 8508 x y z + 2133 x z + 1300 y z + 5664 x y z + 13224 x y z 3 6 3 4 5 3 5 4 3 6 3 3 + 19152 x y z + 20244 x y z + 20244 x y z + 19152 x y z 7 2 3 8 3 9 3 10 2 9 2 + 13224 x y z + 5664 x y z + 1300 x z + 612 y z + 2940 x y z 2 8 2 3 7 2 4 6 2 5 5 2 + 7542 x y z + 13224 x y z + 18186 x y z + 20160 x y z 6 4 2 7 3 2 8 2 2 9 2 10 2 + 18186 x y z + 13224 x y z + 7542 x y z + 2940 x y z + 612 x z 11 10 2 9 3 8 4 7 + 192 y z + 1032 x y z + 2940 x y z + 5664 x y z + 8508 x y z 5 6 6 5 7 4 8 3 9 2 + 10416 x y z + 10416 x y z + 8508 x y z + 5664 x y z + 2940 x y z 10 11 12 11 2 10 3 9 + 1032 x y z + 192 x z + 32 y + 192 x y + 612 x y + 1300 x y 4 8 5 7 6 6 7 5 8 4 9 3 + 2133 x y + 2844 x y + 3150 x y + 2844 x y + 2133 x y + 1300 x y 10 2 11 12 12 11 11 + 612 x y + 192 x y + 32 x >= 32 z + 192 y z + 192 x z 2 10 10 2 10 3 9 2 9 + 612 y z + 1032 x y z + 612 x z + 1300 y z + 2940 x y z 2 9 3 9 4 8 3 8 2 2 8 + 2940 x y z + 1300 x z + 2106 y z + 5556 x y z + 7380 x y z 3 8 4 8 5 7 4 7 2 3 7 + 5556 x y z + 2106 x z + 2736 y z + 7968 x y z + 12144 x y z 3 2 7 4 7 5 7 6 6 5 6 + 12144 x y z + 7968 x y z + 2736 x z + 2988 y z + 9336 x y z 2 4 6 3 3 6 4 2 6 5 6 6 6 + 15324 x y z + 19360 x y z + 15324 x y z + 9336 x y z + 2988 x z 7 5 6 5 2 5 5 3 4 5 4 3 5 + 2736 y z + 9336 x y z + 16272 x y z + 25512 x y z + 25512 x y z 5 2 5 6 5 7 5 8 4 7 4 + 16272 x y z + 9336 x y z + 2736 x z + 2106 y z + 7968 x y z 2 6 4 3 5 4 4 4 4 5 3 4 + 15324 x y z + 25512 x y z + 32580 x y z + 25512 x y z 6 2 4 7 4 8 4 9 3 8 3 + 15324 x y z + 7968 x y z + 2106 x z + 1300 y z + 5556 x y z 2 7 3 3 6 3 4 5 3 5 4 3 + 12144 x y z + 19360 x y z + 25512 x y z + 25512 x y z 6 3 3 7 2 3 8 3 9 3 10 2 + 19360 x y z + 12144 x y z + 5556 x y z + 1300 x z + 612 y z 9 2 2 8 2 3 7 2 4 6 2 + 2940 x y z + 7380 x y z + 12144 x y z + 15324 x y z 5 5 2 6 4 2 7 3 2 8 2 2 + 16272 x y z + 15324 x y z + 12144 x y z + 7380 x y z 9 2 10 2 11 10 2 9 + 2940 x y z + 612 x z + 192 y z + 1032 x y z + 2940 x y z 3 8 4 7 5 6 6 5 7 4 + 5556 x y z + 7968 x y z + 9336 x y z + 9336 x y z + 7968 x y z 8 3 9 2 10 11 12 11 + 5556 x y z + 2940 x y z + 1032 x y z + 192 x z + 32 y + 192 x y 2 10 3 9 4 8 5 7 6 6 7 5 + 612 x y + 1300 x y + 2106 x y + 2736 x y + 2988 x y + 2736 x y 8 4 9 3 10 2 11 12 + 2106 x y + 1300 x y + 612 x y + 192 x y + 32 x Expanding and collecting terms of the same sign gives: 4 8 3 8 2 2 8 3 8 4 8 5 7 27 y z + 108 x y z + 162 x y z + 108 x y z + 27 x z + 108 y z 4 7 2 3 7 3 2 7 4 7 5 7 + 540 x y z + 1080 x y z + 1080 x y z + 540 x y z + 108 x z 6 6 5 6 2 4 6 4 2 6 5 6 + 162 y z + 1080 x y z + 2862 x y z + 2862 x y z + 1080 x y z 6 6 7 5 6 5 2 5 5 5 2 5 + 162 x z + 108 y z + 1080 x y z + 3888 x y z + 3888 x y z 6 5 7 5 8 4 7 4 2 6 4 + 1080 x y z + 108 x z + 27 y z + 540 x y z + 2862 x y z 6 2 4 7 4 8 4 8 3 2 7 3 + 2862 x y z + 540 x y z + 27 x z + 108 x y z + 1080 x y z 7 2 3 8 3 2 8 2 3 7 2 4 6 2 + 1080 x y z + 108 x y z + 162 x y z + 1080 x y z + 2862 x y z 5 5 2 6 4 2 7 3 2 8 2 2 3 8 + 3888 x y z + 2862 x y z + 1080 x y z + 162 x y z + 108 x y z 4 7 5 6 6 5 7 4 8 3 + 540 x y z + 1080 x y z + 1080 x y z + 540 x y z + 108 x y z 4 8 5 7 6 6 7 5 8 4 + 27 x y + 108 x y + 162 x y + 108 x y + 27 x y >= 3 3 6 3 4 5 4 3 5 3 5 4 4 4 4 208 x y z + 5268 x y z + 5268 x y z + 5268 x y z + 15234 x y z 5 3 4 3 6 3 4 5 3 5 4 3 6 3 3 + 5268 x y z + 208 x y z + 5268 x y z + 5268 x y z + 208 x y z Expressing in terms of symmetric polynomials gives: 27 {8, 4, 0} + 108 {8, 3, 1} + 81 {8, 2, 2} + 108 {7, 5, 0} + 540 {7, 4, 1} + 1080 {7, 3, 2} + 81 {6, 6, 0} + 1080 {6, 5, 1} + 2862 {6, 4, 2} + 1944 {5, 5, 2} >= 104 {6, 3, 3} + 5268 {5, 4, 3} + 2539 {4, 4, 4} This follows from the following majorizations: left side: [1944 {5, 5, 2}, 2862 {6, 4, 2}, 1080 {6, 5, 1}, 81 {6, 6, 0}, 1080 {7, 3, 2}, 540 {7, 4, 1}, 108 {7, 5, 0}, 81 {8, 2, 2}, 108 {8, 3, 1}, 27 {8, 4, 0}] right side: [2539 {4, 4, 4}, 5268 {5, 4, 3}, 104 {6, 3, 3}] (d7) notsure (c8) /* 2.16 */ trineq(1 1 Removing the trigonometric expressions gives: 3 2 2 2 3 2 2 3 c + (- b - a) c + (- b - a ) c + b - a b - a b + a - --------------------------------------------------------- > 1 2 a b c Multiplying both sides by 2 a b c 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 > 2 a b c 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. (d8) true (c9) trineq(csum(cos(A))<=3/2); 3 To prove: - >= cos(C) + cos(B) + cos(A) 2 Removing the trigonometric expressions gives: 3 2 2 2 3 2 2 3 3 c + (- b - a) c + (- b - a ) c + b - a b - a b + a - >= - --------------------------------------------------------- 2 2 a b c Multiplying both sides by 2 a b c gives: 3 2 2 2 2 3 2 2 3 3 a b c >= - c + b c + a c + b c + a c - b + a b + 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. (d9) true (c10) /* 2.21 */ trineq(3/4<=csum(cos(A)^2)); 2 2 2 3 To prove: cos (C) + cos (B) + cos (A) >= - 4 Removing the trigonometric expressions gives: 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 c + (- b - a ) c + (- b + 6 a b - a ) c + b - a b - a b + a 3 ------------------------------------------------------------------------ >= - 2 2 2 4 4 a b c 2 2 2 Multiplying both sides by 4 a b c gives: 6 2 4 2 4 4 2 2 2 2 4 2 6 2 4 4 2 6 c - b c - a c - b c + 6 a b c - a c + b - a b - a b + a >= 2 2 2 3 a b c Expanding and collecting terms of the same sign gives: 6 2 2 2 6 6 2 4 2 4 4 2 4 2 2 4 4 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: 6 5 2 2 4 (z + (3 y + 3 x) z + (9 y + 3 x y + 9 x ) z 3 2 2 3 3 + (13 y + 9 x y + 9 x y + 13 x ) z 4 3 2 2 3 4 2 + (9 y + 9 x y + 15 x y + 9 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (3 y + 3 x y + 9 x y + 9 x y + 3 x y + 3 x ) z + y + 3 x y 2 4 3 3 4 2 5 6 + 9 x y + 13 x y + 9 x y + 3 x y + x )/32 >= 6 5 2 2 4 (2 z + (6 y + 6 x) z + (9 y + 20 x y + 9 x ) z 3 2 2 3 3 + (8 y + 28 x y + 28 x y + 8 x ) z 4 3 2 2 3 4 2 + (9 y + 28 x y + 36 x y + 28 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (6 y + 20 x y + 28 x y + 28 x y + 20 x y + 6 x ) z + 2 y + 6 x y 2 4 3 3 4 2 5 6 + 9 x y + 8 x y + 9 x y + 6 x y + 2 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 18 y z + 6 x y z + 18 x z + 26 y z + 18 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 18 x y z + 26 x z + 18 y z + 18 x y z + 30 x y z + 18 x y z 4 2 5 4 2 3 3 2 4 5 + 18 x z + 6 y z + 6 x y z + 18 x y z + 18 x y z + 6 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 18 x y + 26 x y + 18 x y + 6 x y + 2 x >= 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 9 y z + 20 x y z + 9 x z + 8 y z + 28 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 28 x y z + 8 x z + 9 y z + 28 x y z + 36 x y z + 28 x y z 4 2 5 4 2 3 3 2 4 5 + 9 x z + 6 y z + 20 x y z + 28 x y z + 28 x y z + 20 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 9 x y + 8 x y + 9 x y + 6 x y + 2 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 9 y z + 9 x z + 18 y z + 18 x z + 9 y z + 9 x z + 9 x y 3 3 4 2 4 2 3 2 3 3 2 + 18 x y + 9 x y >= 14 x y z + 10 x y z + 10 x y z + 10 x y z 2 2 2 3 2 4 2 3 3 2 4 + 6 x y z + 10 x y z + 14 x y z + 10 x y z + 10 x y z + 14 x y z Expressing in terms of symmetric polynomials gives: 9 {4, 2, 0} + 9 {3, 3, 0} >= 7 {4, 1, 1} + 10 {3, 2, 1} + {2, 2, 2} This follows from the following majorizations: 7 {4, 2, 0} >= 7 {4, 1, 1} 2 {4, 2, 0} >= 2 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} {3, 3, 0} >= {2, 2, 2} (d10) true (c11) trineq(csum(cos(A)^2)<3); 2 2 2 To prove: 3 > cos (C) + cos (B) + cos (A) Removing the trigonometric expressions gives: 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 c + (- b - a ) c + (- b + 6 a b - a ) c + b - a b - a b + a 3 > ------------------------------------------------------------------------ 2 2 2 4 a b c 2 2 2 Multiplying both sides by 4 a b c gives: 2 2 2 6 2 4 2 4 4 2 2 2 2 4 2 6 2 4 12 a b c > c - b c - a c - b c + 6 a b c - a c + b - a b 4 2 6 - a b + a Expanding and collecting terms of the same sign gives: 2 4 2 4 4 2 2 2 2 4 2 2 4 4 2 6 6 6 b c + a c + b c + 6 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: 6 5 2 2 4 (2 z + (6 y + 6 x) z + (15 y + 32 x y + 15 x ) z 3 2 2 3 3 + (20 y + 64 x y + 64 x y + 20 x ) z 4 3 2 2 3 4 2 + (15 y + 64 x y + 96 x y + 64 x y + 15 x ) z 5 4 2 3 3 2 4 5 6 5 + (6 y + 32 x y + 64 x y + 64 x y + 32 x y + 6 x ) z + 2 y + 6 x y 2 4 3 3 4 2 5 6 + 15 x y + 20 x y + 15 x y + 6 x y + 2 x )/64 > 6 5 2 2 4 3 3 3 (2 z + (6 y + 6 x) z + (15 y + 15 x ) z + (20 y + 20 x ) z 4 4 2 5 5 6 5 2 4 3 3 + (15 y + 15 x ) z + (6 y + 6 x ) z + 2 y + 6 x y + 15 x y + 20 x y 4 2 5 6 + 15 x y + 6 x y + 2 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 2 z + 6 y z + 6 x z + 15 y z + 32 x y z + 15 x z + 20 y z 2 3 2 3 3 3 4 2 3 2 2 2 2 + 64 x y z + 64 x y z + 20 x z + 15 y z + 64 x y z + 96 x y z 3 2 4 2 5 4 2 3 3 2 + 64 x y z + 15 x z + 6 y z + 32 x y z + 64 x y z + 64 x y z 4 5 6 5 2 4 3 3 4 2 5 + 32 x y z + 6 x z + 2 y + 6 x y + 15 x y + 20 x y + 15 x y + 6 x y 6 6 5 5 2 4 2 4 3 3 3 3 + 2 x > 2 z + 6 y z + 6 x z + 15 y z + 15 x z + 20 y z + 20 x z 4 2 4 2 5 5 6 5 2 4 3 3 + 15 y z + 15 x z + 6 y z + 6 x z + 2 y + 6 x y + 15 x y + 20 x y 4 2 5 6 + 15 x y + 6 x y + 2 x Expanding and collecting terms of the same sign gives: 4 2 3 2 3 3 2 2 2 2 3 2 32 x y z + 64 x y z + 64 x y z + 64 x y z + 96 x y z + 64 x y z 4 2 3 3 2 4 + 32 x y z + 64 x y z + 64 x y z + 32 x y z > 0 This is true because a sum of positive terms must be positive. (d11) true (c12) /* 2.22 */ trineq(csum(cos(A)*cos(B))<=3/4); 3 To prove: - >= cos(B) cos(C) + cos(A) cos(C) + cos(A) cos(B) 4 Removing the trigonometric expressions gives: 3 5 4 3 3 3 5 4 4 5 - >= - ((b + a) c - a b c + (- 2 b - 2 a ) c + (b - a b - a b + a ) c 4 5 3 3 5 2 2 2 + a b - 2 a b + a b)/(4 a b c ) 2 2 2 Multiplying both sides by 4 a b c gives: 2 2 2 5 5 4 3 3 3 3 5 4 3 a b c >= - b c - a c + a b c + 2 b c + 2 a c - b c + a b c 4 5 5 3 3 5 + a b c - a c - a b + 2 a b - a b Expanding and collecting terms of the same sign gives: 5 5 2 2 2 5 5 5 5 b c + a c + 3 a b c + b c + a c + a b + a b >= 4 3 3 3 3 4 4 3 3 a b c + 2 b c + 2 a c + a b c + a b c + 2 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 + (9 y + 13 x y + 9 x ) z 3 2 2 3 3 + (13 y + 19 x y + 19 x y + 13 x ) z 4 3 2 2 3 4 2 + (9 y + 19 x y + 15 x y + 19 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (4 y + 13 x y + 19 x y + 19 x y + 13 x y + 4 x ) z + y + 4 x y 2 4 3 3 4 2 5 6 + 9 x y + 13 x y + 9 x y + 4 x y + x )/32 >= 6 5 2 2 4 (2 z + (8 y + 8 x) z + (11 y + 28 x y + 11 x ) z 3 2 2 3 3 + (12 y + 44 x y + 44 x y + 12 x ) z 4 3 2 2 3 4 2 + (11 y + 44 x y + 72 x y + 44 x y + 11 x ) z 5 4 2 3 3 2 4 5 6 5 + (8 y + 28 x y + 44 x y + 44 x y + 28 x y + 8 x ) z + 2 y + 8 x y 2 4 3 3 4 2 5 6 + 11 x y + 12 x y + 11 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 + 18 y z + 26 x y z + 18 x z + 26 y z 2 3 2 3 3 3 4 2 3 2 2 2 2 + 38 x y z + 38 x y z + 26 x z + 18 y z + 38 x y z + 30 x y z 3 2 4 2 5 4 2 3 3 2 + 38 x y z + 18 x z + 8 y z + 26 x y z + 38 x y z + 38 x y z 4 5 6 5 2 4 3 3 4 2 5 + 26 x y z + 8 x z + 2 y + 8 x y + 18 x y + 26 x y + 18 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 + 11 y z + 28 x y z + 11 x z + 12 y z 2 3 2 3 3 3 4 2 3 2 2 2 2 + 44 x y z + 44 x y z + 12 x z + 11 y z + 44 x y z + 72 x y z 3 2 4 2 5 4 2 3 3 2 + 44 x y z + 11 x z + 8 y z + 28 x y z + 44 x y z + 44 x y z 4 5 6 5 2 4 3 3 4 2 5 + 28 x y z + 8 x z + 2 y + 8 x y + 11 x y + 12 x y + 11 x y + 8 x y 6 + 2 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 7 y z + 7 x z + 14 y z + 14 x z + 7 y z + 7 x z + 7 x y 3 3 4 2 4 2 3 2 3 3 2 + 14 x y + 7 x y >= 2 x y z + 6 x y z + 6 x y z + 6 x y z 2 2 2 3 2 4 2 3 3 2 4 + 42 x y z + 6 x y z + 2 x y z + 6 x y z + 6 x y z + 2 x y z Expressing in terms of symmetric polynomials gives: 7 {4, 2, 0} + 7 {3, 3, 0} >= {4, 1, 1} + 6 {3, 2, 1} + 7 {2, 2, 2} This follows from the following majorizations: {4, 2, 0} >= {4, 1, 1} 6 {4, 2, 0} >= 6 {3, 2, 1} 7 {3, 3, 0} >= 7 {2, 2, 2} (d12) true (c13) /* 2.23 */ trineq(cprod(cos(A))<=1/8); 1 To prove: - >= cos(A) cos(B) cos(C) 8 Removing the trigonometric expressions gives: 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 1 c + (- b - a ) c + (- b + 2 a b - a ) c + b - a b - a b + a - >= - ------------------------------------------------------------------------ 8 2 2 2 8 a b c 2 2 2 Multiplying both sides by 8 a b c gives: 2 2 2 6 2 4 2 4 4 2 2 2 2 4 2 6 2 4 a b c >= - c + b c + a c + b c - 2 a b c + a c - b + a b 4 2 6 + a b - a Expanding and collecting terms of the same sign gives: 6 2 2 2 6 6 2 4 2 4 4 2 4 2 2 4 4 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: 6 5 2 2 4 (z + (3 y + 3 x) z + (9 y + 3 x y + 9 x ) z 3 2 2 3 3 + (13 y + 9 x y + 9 x y + 13 x ) z 4 3 2 2 3 4 2 + (9 y + 9 x y + 15 x y + 9 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (3 y + 3 x y + 9 x y + 9 x y + 3 x y + 3 x ) z + y + 3 x y 2 4 3 3 4 2 5 6 + 9 x y + 13 x y + 9 x y + 3 x y + x )/32 >= 6 5 2 2 4 (2 z + (6 y + 6 x) z + (9 y + 20 x y + 9 x ) z 3 2 2 3 3 + (8 y + 28 x y + 28 x y + 8 x ) z 4 3 2 2 3 4 2 + (9 y + 28 x y + 36 x y + 28 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (6 y + 20 x y + 28 x y + 28 x y + 20 x y + 6 x ) z + 2 y + 6 x y 2 4 3 3 4 2 5 6 + 9 x y + 8 x y + 9 x y + 6 x y + 2 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 18 y z + 6 x y z + 18 x z + 26 y z + 18 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 18 x y z + 26 x z + 18 y z + 18 x y z + 30 x y z + 18 x y z 4 2 5 4 2 3 3 2 4 5 + 18 x z + 6 y z + 6 x y z + 18 x y z + 18 x y z + 6 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 18 x y + 26 x y + 18 x y + 6 x y + 2 x >= 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 9 y z + 20 x y z + 9 x z + 8 y z + 28 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 28 x y z + 8 x z + 9 y z + 28 x y z + 36 x y z + 28 x y z 4 2 5 4 2 3 3 2 4 5 + 9 x z + 6 y z + 20 x y z + 28 x y z + 28 x y z + 20 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 9 x y + 8 x y + 9 x y + 6 x y + 2 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 9 y z + 9 x z + 18 y z + 18 x z + 9 y z + 9 x z + 9 x y 3 3 4 2 4 2 3 2 3 3 2 + 18 x y + 9 x y >= 14 x y z + 10 x y z + 10 x y z + 10 x y z 2 2 2 3 2 4 2 3 3 2 4 + 6 x y z + 10 x y z + 14 x y z + 10 x y z + 10 x y z + 14 x y z Expressing in terms of symmetric polynomials gives: 9 {4, 2, 0} + 9 {3, 3, 0} >= 7 {4, 1, 1} + 10 {3, 2, 1} + {2, 2, 2} This follows from the following majorizations: 7 {4, 2, 0} >= 7 {4, 1, 1} 2 {4, 2, 0} >= 2 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} {3, 3, 0} >= {2, 2, 2} (d13) true (c14) /* 2.26 */ trineq(cprod(cos(A))<=(1/24)*csum(cos(B-C)^2)); 2 2 2 cos (C - B) + cos (C - A) + cos (B - A) To prove: --------------------------------------- >= cos(A) cos(B) cos(C) 24 Expanding the trigonometric expressions gives: 2 2 2 2 2 2 2 2 cos (B) cos (C) cos (A) cos (C) sin (B) sin (C) sin (A) sin (C) --------------- + --------------- + --------------- + --------------- 24 24 24 24 2 2 cos(B) sin(B) cos(C) sin(C) cos(A) sin(A) cos(C) sin(C) cos (A) cos (B) + --------------------------- + --------------------------- + --------------- 12 12 24 2 2 sin (A) sin (B) cos(A) sin(A) cos(B) sin(B) + --------------- + --------------------------- >= cos(A) cos(B) cos(C) 24 12 Removing the trigonometric expressions gives: 2 2 10 4 2 2 4 8 ((b + a ) c + (- 4 b + a b - 4 a ) c 6 2 4 4 2 2 6 2 2 6 + (6 b - 2 a b + (- 2 a - 32 K ) b + 6 a - 32 K a ) c 8 2 6 4 2 4 2 2 6 2 8 + (- 4 b - 2 a b + (12 a + 64 K ) b + (32 K a - 2 a ) b - 4 a 2 4 4 10 2 8 4 2 6 2 2 6 4 + 64 K a ) c + (b + a b + (- 2 a - 32 K ) b + (32 K a - 2 a ) b 8 2 4 4 2 10 2 6 4 2 2 2 10 + (a + 32 K a + 256 K ) b + a - 32 K a + 256 K a ) c + a b 4 8 6 2 2 6 2 4 8 4 - 4 a b + (6 a - 32 K a ) b + (64 K a - 4 a ) b 10 2 6 4 2 2 4 4 4 + (a - 32 K a + 256 K a ) b )/(384 a b c ) >= 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 c + (- b - a ) c + (- b + 2 a b - a ) c + b - a b - a b + a - ------------------------------------------------------------------------ 2 2 2 8 a b c 4 4 4 Multiplying both sides by 384 a b c gives: 2 10 2 10 4 8 2 2 8 4 8 6 6 2 4 6 b c + a c - 4 b c + a b c - 4 a c + 6 b c - 2 a b c 4 2 6 2 2 6 6 6 2 2 6 8 4 2 6 4 - 2 a b c - 32 K b c + 6 a c - 32 K a c - 4 b c - 2 a b c 4 4 4 2 4 4 6 2 4 2 2 2 4 8 4 + 12 a b c + 64 K b c - 2 a b c + 32 K a b c - 4 a c 2 4 4 10 2 2 8 2 4 6 2 2 6 2 6 4 2 + 64 K a c + b c + a b c - 2 a b c - 32 K b c - 2 a b c 2 2 4 2 8 2 2 2 4 2 2 4 2 2 10 2 + 32 K a b c + a b c + 32 K a b c + 256 K b c + a c 2 6 2 4 2 2 2 10 4 8 6 6 2 2 6 - 32 K a c + 256 K a c + a b - 4 a b + 6 a b - 32 K a b 8 4 2 4 4 10 2 2 6 2 4 2 2 - 4 a b + 64 K a b + a b - 32 K a b + 256 K a b >= 2 2 8 2 4 6 4 2 6 2 6 4 4 4 4 - 48 a b c + 48 a b c + 48 a b c + 48 a b c - 96 a b c 6 2 4 2 8 2 4 6 2 6 4 2 8 2 2 + 48 a b c - 48 a b c + 48 a b c + 48 a b c - 48 a b c Expanding and collecting terms of the same sign gives: 2 10 2 10 2 2 8 6 6 6 6 4 4 4 2 4 4 b c + a c + 49 a b c + 6 b c + 6 a c + 108 a b c + 64 K b c 2 2 2 4 2 4 4 10 2 2 8 2 2 2 4 2 + 32 K a b c + 64 K a c + b c + 49 a b c + 32 K a b c 8 2 2 2 4 2 2 4 2 2 10 2 4 2 2 2 10 + 49 a b c + 32 K a b c + 256 K b c + a c + 256 K a c + a b 6 6 2 4 4 10 2 4 2 2 + 6 a b + 64 K a b + a b + 256 K a b >= 4 8 4 8 2 4 6 4 2 6 2 2 6 2 2 6 4 b c + 4 a c + 50 a b c + 50 a b c + 32 K b c + 32 K a c 8 4 2 6 4 6 2 4 8 4 4 6 2 2 6 2 + 4 b c + 50 a b c + 50 a b c + 4 a c + 50 a b c + 32 K b c 6 4 2 2 6 2 4 8 2 2 6 8 4 2 6 2 + 50 a b c + 32 K a c + 4 a b + 32 K a b + 4 a b + 32 K a b Replacing K^2 by F^2 gives: 2 2 10 2 2 8 6 6 6 (b + a ) c + 49 a b c + (6 b + 6 a ) c 4 2 4 2 2 2 2 4 4 + ((108 a + 64 F ) b + 32 F a b + 64 F a ) c 10 2 8 2 2 4 8 2 4 4 2 10 + (b + 49 a b + 32 F a b + (49 a + 32 F a + 256 F ) b + a 4 2 2 2 10 6 6 2 4 4 10 4 2 2 + 256 F a ) c + a b + 6 a b + 64 F a b + (a + 256 F a ) b >= 4 4 8 2 4 4 2 2 2 2 6 (4 b + 4 a ) c + (50 a b + (50 a + 32 F ) b + 32 F a ) c 8 2 6 6 2 8 4 + (4 b + 50 a b + 50 a b + 4 a ) c 4 2 6 6 4 2 6 2 4 8 2 2 6 + ((50 a + 32 F ) b + 50 a b + 32 F a ) c + 4 a b + 32 F a b 8 4 2 6 2 + 4 a b + 32 F a b Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 10 4 2 2 4 8 (2 b + 2 a ) c + (- 8 b + 40 a b - 8 a ) c 6 2 4 4 2 6 6 + (20 b + 16 a b + 16 a b + 20 a ) c 8 2 6 4 4 6 2 8 4 + (- 8 b + 16 a b + 120 a b + 16 a b - 8 a ) c 10 2 8 4 6 6 4 8 2 10 2 2 10 + (2 b + 40 a b + 16 a b + 16 a b + 40 a b + 2 a ) c + 2 a b 4 8 6 6 8 4 10 2 - 8 a b + 20 a b - 8 a b + 2 a b >= 2 2 10 4 2 2 4 8 (- 2 b - 2 a ) c + (8 b + 8 a b + 8 a ) c 6 2 4 4 2 6 6 + (- 4 b + 52 a b + 52 a b - 4 a ) c 8 2 6 6 2 8 4 + (8 b + 52 a b + 52 a b + 8 a ) c 10 2 8 4 6 6 4 8 2 10 2 2 10 + (- 2 b + 8 a b + 52 a b + 52 a b + 8 a b - 2 a ) c - 2 a b 4 8 6 6 8 4 10 2 + 8 a b - 4 a b + 8 a b - 2 a b Expanding and collecting terms of the same sign gives: 2 10 2 10 2 2 8 6 6 6 6 4 4 4 4 b c + 4 a c + 32 a b c + 24 b c + 24 a c + 120 a b c 10 2 2 8 2 8 2 2 10 2 2 10 6 6 + 4 b c + 32 a b c + 32 a b c + 4 a c + 4 a b + 24 a b 10 2 4 8 4 8 2 4 6 4 2 6 8 4 + 4 a b >= 16 b c + 16 a c + 36 a b c + 36 a b c + 16 b c 2 6 4 6 2 4 8 4 4 6 2 6 4 2 4 8 + 36 a b c + 36 a b c + 16 a c + 36 a b c + 36 a b c + 16 a b 8 4 + 16 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 12 11 2 2 10 (8 z + (48 y + 48 x) z + (154 y + 292 x y + 154 x ) z 3 2 2 3 9 + (330 y + 910 x y + 910 x y + 330 x ) z 4 3 2 2 3 4 8 + (607 y + 1890 x y + 2686 x y + 1890 x y + 607 x ) z 5 4 2 3 3 2 4 5 7 + (976 y + 3208 x y + 5224 x y + 5224 x y + 3208 x y + 976 x ) z 6 5 2 4 3 3 4 2 5 + (1178 y + 4428 x y + 7930 x y + 9648 x y + 7930 x y + 4428 x y 6 6 7 6 2 5 3 4 4 3 + 1178 x ) z + (976 y + 4428 x y + 9256 x y + 13324 x y + 13324 x y 5 2 6 7 5 8 7 2 6 + 9256 x y + 4428 x y + 976 x ) z + (607 y + 3208 x y + 7930 x y 3 5 4 4 5 3 6 2 7 8 + 13324 x y + 16110 x y + 13324 x y + 7930 x y + 3208 x y + 607 x ) 4 9 8 2 7 3 6 4 5 5 4 z + (330 y + 1890 x y + 5224 x y + 9648 x y + 13324 x y + 13324 x y 6 3 7 2 8 9 3 + 9648 x y + 5224 x y + 1890 x y + 330 x ) z 10 9 2 8 3 7 4 6 5 5 + (154 y + 910 x y + 2686 x y + 5224 x y + 7930 x y + 9256 x y 6 4 7 3 8 2 9 10 2 + 7930 x y + 5224 x y + 2686 x y + 910 x y + 154 x ) z 11 10 2 9 3 8 4 7 5 6 + (48 y + 292 x y + 910 x y + 1890 x y + 3208 x y + 4428 x y 6 5 7 4 8 3 9 2 10 11 + 4428 x y + 3208 x y + 1890 x y + 910 x y + 292 x y + 48 x ) z 12 11 2 10 3 9 4 8 5 7 + 8 y + 48 x y + 154 x y + 330 x y + 607 x y + 976 x y 6 6 7 5 8 4 9 3 10 2 11 + 1178 x y + 976 x y + 607 x y + 330 x y + 154 x y + 48 x y 12 12 11 2 2 10 + 8 x )/1024 >= (8 z + (48 y + 48 x) z + (154 y + 292 x y + 154 x ) z 3 2 2 3 9 + (330 y + 910 x y + 910 x y + 330 x ) z 4 3 2 2 3 4 8 + (499 y + 1938 x y + 2742 x y + 1938 x y + 499 x ) z 5 4 2 3 3 2 4 5 7 + (544 y + 2968 x y + 5640 x y + 5640 x y + 2968 x y + 544 x ) z 6 5 2 4 3 3 4 2 5 + (530 y + 3468 x y + 8354 x y + 10608 x y + 8354 x y + 3468 x y 6 6 7 6 2 5 3 4 4 3 + 530 x ) z + (544 y + 3468 x y + 9384 x y + 13948 x y + 13948 x y 5 2 6 7 5 8 7 2 6 + 9384 x y + 3468 x y + 544 x ) z + (499 y + 2968 x y + 8354 x y 3 5 4 4 5 3 6 2 7 8 + 13948 x y + 15990 x y + 13948 x y + 8354 x y + 2968 x y + 499 x ) 4 9 8 2 7 3 6 4 5 z + (330 y + 1938 x y + 5640 x y + 10608 x y + 13948 x y 5 4 6 3 7 2 8 9 3 + 13948 x y + 10608 x y + 5640 x y + 1938 x y + 330 x ) z 10 9 2 8 3 7 4 6 5 5 + (154 y + 910 x y + 2742 x y + 5640 x y + 8354 x y + 9384 x y 6 4 7 3 8 2 9 10 2 + 8354 x y + 5640 x y + 2742 x y + 910 x y + 154 x ) z 11 10 2 9 3 8 4 7 5 6 + (48 y + 292 x y + 910 x y + 1938 x y + 2968 x y + 3468 x y 6 5 7 4 8 3 9 2 10 11 + 3468 x y + 2968 x y + 1938 x y + 910 x y + 292 x y + 48 x ) z 12 11 2 10 3 9 4 8 5 7 + 8 y + 48 x y + 154 x y + 330 x y + 499 x y + 544 x y 6 6 7 5 8 4 9 3 10 2 11 + 530 x y + 544 x y + 499 x y + 330 x y + 154 x y + 48 x y 12 + 8 x )/1024 Multiplying both sides by 1024 gives: 12 11 11 2 10 10 2 10 3 9 8 z + 48 y z + 48 x z + 154 y z + 292 x y z + 154 x z + 330 y z 2 9 2 9 3 9 4 8 3 8 + 910 x y z + 910 x y z + 330 x z + 607 y z + 1890 x y z 2 2 8 3 8 4 8 5 7 4 7 + 2686 x y z + 1890 x y z + 607 x z + 976 y z + 3208 x y z 2 3 7 3 2 7 4 7 5 7 6 6 + 5224 x y z + 5224 x y z + 3208 x y z + 976 x z + 1178 y z 5 6 2 4 6 3 3 6 4 2 6 5 6 + 4428 x y z + 7930 x y z + 9648 x y z + 7930 x y z + 4428 x y z 6 6 7 5 6 5 2 5 5 3 4 5 + 1178 x z + 976 y z + 4428 x y z + 9256 x y z + 13324 x y z 4 3 5 5 2 5 6 5 7 5 8 4 + 13324 x y z + 9256 x y z + 4428 x y z + 976 x z + 607 y z 7 4 2 6 4 3 5 4 4 4 4 + 3208 x y z + 7930 x y z + 13324 x y z + 16110 x y z 5 3 4 6 2 4 7 4 8 4 9 3 + 13324 x y z + 7930 x y z + 3208 x y z + 607 x z + 330 y z 8 3 2 7 3 3 6 3 4 5 3 + 1890 x y z + 5224 x y z + 9648 x y z + 13324 x y z 5 4 3 6 3 3 7 2 3 8 3 9 3 + 13324 x y z + 9648 x y z + 5224 x y z + 1890 x y z + 330 x z 10 2 9 2 2 8 2 3 7 2 4 6 2 + 154 y z + 910 x y z + 2686 x y z + 5224 x y z + 7930 x y z 5 5 2 6 4 2 7 3 2 8 2 2 9 2 + 9256 x y z + 7930 x y z + 5224 x y z + 2686 x y z + 910 x y z 10 2 11 10 2 9 3 8 + 154 x z + 48 y z + 292 x y z + 910 x y z + 1890 x y z 4 7 5 6 6 5 7 4 8 3 + 3208 x y z + 4428 x y z + 4428 x y z + 3208 x y z + 1890 x y z 9 2 10 11 12 11 2 10 + 910 x y z + 292 x y z + 48 x z + 8 y + 48 x y + 154 x y 3 9 4 8 5 7 6 6 7 5 8 4 + 330 x y + 607 x y + 976 x y + 1178 x y + 976 x y + 607 x y 9 3 10 2 11 12 + 330 x y + 154 x y + 48 x y + 8 x >= 12 11 11 2 10 10 2 10 3 9 8 z + 48 y z + 48 x z + 154 y z + 292 x y z + 154 x z + 330 y z 2 9 2 9 3 9 4 8 3 8 + 910 x y z + 910 x y z + 330 x z + 499 y z + 1938 x y z 2 2 8 3 8 4 8 5 7 4 7 + 2742 x y z + 1938 x y z + 499 x z + 544 y z + 2968 x y z 2 3 7 3 2 7 4 7 5 7 6 6 + 5640 x y z + 5640 x y z + 2968 x y z + 544 x z + 530 y z 5 6 2 4 6 3 3 6 4 2 6 5 6 + 3468 x y z + 8354 x y z + 10608 x y z + 8354 x y z + 3468 x y z 6 6 7 5 6 5 2 5 5 3 4 5 + 530 x z + 544 y z + 3468 x y z + 9384 x y z + 13948 x y z 4 3 5 5 2 5 6 5 7 5 8 4 + 13948 x y z + 9384 x y z + 3468 x y z + 544 x z + 499 y z 7 4 2 6 4 3 5 4 4 4 4 + 2968 x y z + 8354 x y z + 13948 x y z + 15990 x y z 5 3 4 6 2 4 7 4 8 4 9 3 + 13948 x y z + 8354 x y z + 2968 x y z + 499 x z + 330 y z 8 3 2 7 3 3 6 3 4 5 3 + 1938 x y z + 5640 x y z + 10608 x y z + 13948 x y z 5 4 3 6 3 3 7 2 3 8 3 9 3 + 13948 x y z + 10608 x y z + 5640 x y z + 1938 x y z + 330 x z 10 2 9 2 2 8 2 3 7 2 4 6 2 + 154 y z + 910 x y z + 2742 x y z + 5640 x y z + 8354 x y z 5 5 2 6 4 2 7 3 2 8 2 2 9 2 + 9384 x y z + 8354 x y z + 5640 x y z + 2742 x y z + 910 x y z 10 2 11 10 2 9 3 8 + 154 x z + 48 y z + 292 x y z + 910 x y z + 1938 x y z 4 7 5 6 6 5 7 4 8 3 + 2968 x y z + 3468 x y z + 3468 x y z + 2968 x y z + 1938 x y z 9 2 10 11 12 11 2 10 + 910 x y z + 292 x y z + 48 x z + 8 y + 48 x y + 154 x y 3 9 4 8 5 7 6 6 7 5 8 4 + 330 x y + 499 x y + 544 x y + 530 x y + 544 x y + 499 x y 9 3 10 2 11 12 + 330 x y + 154 x y + 48 x y + 8 x Expanding and collecting terms of the same sign gives: 4 8 4 8 5 7 4 7 4 7 5 7 108 y z + 108 x z + 432 y z + 240 x y z + 240 x y z + 432 x z 6 6 5 6 5 6 6 6 7 5 6 5 + 648 y z + 960 x y z + 960 x y z + 648 x z + 432 y z + 960 x y z 6 5 7 5 8 4 7 4 4 4 4 + 960 x y z + 432 x z + 108 y z + 240 x y z + 120 x y z 7 4 8 4 4 7 5 6 6 5 + 240 x y z + 108 x z + 240 x y z + 960 x y z + 960 x y z 7 4 4 8 5 7 6 6 7 5 8 4 + 240 x y z + 108 x y + 432 x y + 648 x y + 432 x y + 108 x y >= 3 8 2 2 8 3 8 2 3 7 3 2 7 48 x y z + 56 x y z + 48 x y z + 416 x y z + 416 x y z 2 4 6 3 3 6 4 2 6 2 5 5 3 4 5 + 424 x y z + 960 x y z + 424 x y z + 128 x y z + 624 x y z 4 3 5 5 2 5 2 6 4 3 5 4 5 3 4 + 624 x y z + 128 x y z + 424 x y z + 624 x y z + 624 x y z 6 2 4 8 3 2 7 3 3 6 3 4 5 3 + 424 x y z + 48 x y z + 416 x y z + 960 x y z + 624 x y z 5 4 3 6 3 3 7 2 3 8 3 2 8 2 + 624 x y z + 960 x y z + 416 x y z + 48 x y z + 56 x y z 3 7 2 4 6 2 5 5 2 6 4 2 7 3 2 + 416 x y z + 424 x y z + 128 x y z + 424 x y z + 416 x y z 8 2 2 3 8 8 3 + 56 x y z + 48 x y z + 48 x y z Dividing both sides by 4 gives: 4 8 4 8 5 7 4 7 4 7 5 7 27 y z + 27 x z + 108 y z + 60 x y z + 60 x y z + 108 x z 6 6 5 6 5 6 6 6 7 5 6 5 + 162 y z + 240 x y z + 240 x y z + 162 x z + 108 y z + 240 x y z 6 5 7 5 8 4 7 4 4 4 4 7 4 + 240 x y z + 108 x z + 27 y z + 60 x y z + 30 x y z + 60 x y z 8 4 4 7 5 6 6 5 7 4 4 8 + 27 x z + 60 x y z + 240 x y z + 240 x y z + 60 x y z + 27 x y 5 7 6 6 7 5 8 4 + 108 x y + 162 x y + 108 x y + 27 x y >= 3 8 2 2 8 3 8 2 3 7 3 2 7 12 x y z + 14 x y z + 12 x y z + 104 x y z + 104 x y z 2 4 6 3 3 6 4 2 6 2 5 5 3 4 5 + 106 x y z + 240 x y z + 106 x y z + 32 x y z + 156 x y z 4 3 5 5 2 5 2 6 4 3 5 4 5 3 4 + 156 x y z + 32 x y z + 106 x y z + 156 x y z + 156 x y z 6 2 4 8 3 2 7 3 3 6 3 4 5 3 + 106 x y z + 12 x y z + 104 x y z + 240 x y z + 156 x y z 5 4 3 6 3 3 7 2 3 8 3 2 8 2 + 156 x y z + 240 x y z + 104 x y z + 12 x y z + 14 x y z 3 7 2 4 6 2 5 5 2 6 4 2 7 3 2 + 104 x y z + 106 x y z + 32 x y z + 106 x y z + 104 x y z 8 2 2 3 8 8 3 + 14 x y z + 12 x y z + 12 x y z Expressing in terms of symmetric polynomials gives: 27 {8, 4, 0} + 108 {7, 5, 0} + 60 {7, 4, 1} + 81 {6, 6, 0} + 240 {6, 5, 1} + 5 {4, 4, 4} >= 12 {8, 3, 1} + 7 {8, 2, 2} + 104 {7, 3, 2} + 106 {6, 4, 2} + 120 {6, 3, 3} + 16 {5, 5, 2} + 156 {5, 4, 3} This follows from the following majorizations: 5 {6, 6, 0} + 5 {4, 4, 4} >= 10 {6, 4, 2} 12 {8, 4, 0} >= 12 {8, 3, 1} 7 {8, 4, 0} >= 7 {8, 2, 2} left side: [5 {4, 4, 4}, 240 {6, 5, 1}, 81 {6, 6, 0}, 60 {7, 4, 1}, 108 {7, 5, 0}, 27 {8, 4, 0}] right side: [156 {5, 4, 3}, 16 {5, 5, 2}, 120 {6, 3, 3}, 106 {6, 4, 2}, 104 {7, 3, 2}, 7 {8, 2, 2}, 12 {8, 3, 1}] (d14) notsure (c15) /* 2.38 */ trineq(csum(cot(A))>=sqrt(3)); To prove: cot(C) + cot(B) + cot(A) >= sqrt(3) Removing the trigonometric expressions gives: 2 2 2 c + b + a ------------ >= sqrt(3) 4 K Multiplying both sides by 4 K gives: 2 2 2 c + b + a >= 4 sqrt(3) K Since 4 sqrt(3) is positive, and since 2 2 2 c + b + a is positive, we can square both sides to get: 4 2 2 2 4 2 2 4 c + (2 b + 2 a ) c + b + 2 a b + a >= 4 3 2 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s - 48 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 2 4 48 c s + 48 b s + 48 a s + 48 a b c s + c + 2 b c + 2 a c + b 2 2 4 4 2 2 2 + 2 a b + a >= 48 s + 48 b c s + 48 a c s + 48 a b s Let s = (c+b+a)/2 . We get: 4 3 2 2 2 7 c + (24 b + 24 a) c + (38 b + 96 a b + 38 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 7 b + 24 a b + 38 a b + 24 a b 4 4 3 2 2 2 + 7 a >= 3 c + (24 b + 24 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 3 b + 24 a b + 42 a b + 24 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 4 c + 4 b + 4 a >= 4 b c + 4 a c + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/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 )/4 Multiplying both sides by 4 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d15) true (c16) /* 2.39 */ trineq(csum(cot(A)^2)>=1); 2 2 2 To prove: cot (C) + cot (B) + cot (A) >= 1 Removing the trigonometric expressions gives: 4 2 2 2 4 2 2 4 3 c + (- 2 b - 2 a ) c + 3 b - 2 a b + 3 a ------------------------------------------------- >= 1 2 16 K 2 Multiplying both sides by 16 K gives: 4 2 2 2 2 4 2 2 4 2 3 c - 2 b c - 2 a c + 3 b - 2 a b + 3 a >= 16 K Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 2 3 c + 3 b + 3 a >= 2 b c + 2 a c + 2 a b + 16 K Replacing K^2 by F^2 gives: 4 4 4 2 2 2 2 2 2 3 c + 3 b + 3 a >= (2 b + 2 a ) c + 2 a b + 16 F Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 4 4 4 4 2 2 2 4 2 2 4 3 c + 3 b + 3 a >= - c + (4 b + 4 a ) c - b + 4 a b - a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 4 c + 4 b + 4 a >= 4 b c + 4 a c + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/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 )/4 Multiplying both sides by 4 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d16) true (c17) /* 2.45 */ trineq(csum(sec(A))>=6); To prove: sec(C) + sec(B) + sec(A) >= 6 Removing the trigonometric expressions gives: 5 4 3 3 3 ((2 b + 2 a) c - 2 a b c + (- 4 b - 4 a ) c 5 4 4 5 5 3 3 5 + (2 b - 2 a b - 2 a b + 2 a ) c + 2 a b - 4 a b + 2 a b) 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 /(c + (- b - a ) c + (- b + 2 a b - a ) c + b - a b - a b + a ) >= 6 2 2 2 2 2 2 2 2 2 Multiplying both sides by (c - b - a ) (c - b + a ) (c + b - a ) gives: 5 5 4 3 3 3 3 5 4 4 2 b c + 2 a c - 2 a b c - 4 b c - 4 a c + 2 b c - 2 a b c - 2 a b c 5 5 3 3 5 + 2 a c + 2 a b - 4 a b + 2 a b >= 6 2 4 2 4 4 2 2 2 2 4 2 6 2 4 6 c - 6 b c - 6 a c - 6 b c + 12 a b c - 6 a c + 6 b - 6 a b 4 2 6 - 6 a b + 6 a Expanding and collecting terms of the same sign gives: 5 5 2 4 2 4 4 2 4 2 5 5 2 b c + 2 a c + 6 b c + 6 a c + 6 b c + 6 a c + 2 b c + 2 a c 5 2 4 4 2 5 + 2 a b + 6 a b + 6 a b + 2 a b >= 6 4 3 3 3 3 2 2 2 4 4 6 6 c + 2 a b c + 4 b c + 4 a c + 12 a b c + 2 a b c + 2 a b c + 6 b 3 3 6 + 4 a b + 6 a Dividing both sides by 2 gives: 5 5 2 4 2 4 4 2 4 2 5 5 5 b c + a c + 3 b c + 3 a c + 3 b c + 3 a c + b c + a c + a b 2 4 4 2 5 6 4 3 3 3 3 2 2 2 + 3 a b + 3 a b + a b >= 3 c + a b c + 2 b c + 2 a c + 6 a b c 4 4 6 3 3 6 + a b c + a b c + 3 b + 2 a b + 3 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 6 5 2 2 4 (4 z + (13 y + 13 x) z + (21 y + 40 x y + 21 x ) z 3 2 2 3 3 + (22 y + 52 x y + 52 x y + 22 x ) z 4 3 2 2 3 4 2 + (21 y + 52 x y + 54 x y + 52 x y + 21 x ) z 5 4 2 3 3 2 4 5 6 5 + (13 y + 40 x y + 52 x y + 52 x y + 40 x y + 13 x ) z + 4 y + 13 x y 2 4 3 3 4 2 5 6 + 21 x y + 22 x y + 21 x y + 13 x y + 4 x )/32 >= 6 5 2 2 4 (4 z + (13 y + 13 x) z + (31 y + 20 x y + 31 x ) z 3 2 2 3 3 + (42 y + 40 x y + 40 x y + 42 x ) z 4 3 2 2 3 4 2 + (31 y + 40 x y + 66 x y + 40 x y + 31 x ) z 5 4 2 3 3 2 4 5 6 5 + (13 y + 20 x y + 40 x y + 40 x y + 20 x y + 13 x ) z + 4 y + 13 x y 2 4 3 3 4 2 5 6 + 31 x y + 42 x y + 31 x y + 13 x y + 4 x )/32 Multiplying both sides by 32 gives: 6 5 5 2 4 4 2 4 3 3 4 z + 13 y z + 13 x z + 21 y z + 40 x y z + 21 x z + 22 y z 2 3 2 3 3 3 4 2 3 2 2 2 2 + 52 x y z + 52 x y z + 22 x z + 21 y z + 52 x y z + 54 x y z 3 2 4 2 5 4 2 3 3 2 + 52 x y z + 21 x z + 13 y z + 40 x y z + 52 x y z + 52 x y z 4 5 6 5 2 4 3 3 4 2 + 40 x y z + 13 x z + 4 y + 13 x y + 21 x y + 22 x y + 21 x y 5 6 6 5 5 2 4 4 2 4 + 13 x y + 4 x >= 4 z + 13 y z + 13 x z + 31 y z + 20 x y z + 31 x z 3 3 2 3 2 3 3 3 4 2 3 2 + 42 y z + 40 x y z + 40 x y z + 42 x z + 31 y z + 40 x y z 2 2 2 3 2 4 2 5 4 2 3 + 66 x y z + 40 x y z + 31 x z + 13 y z + 20 x y z + 40 x y z 3 2 4 5 6 5 2 4 3 3 + 40 x y z + 20 x y z + 13 x z + 4 y + 13 x y + 31 x y + 42 x y 4 2 5 6 + 31 x y + 13 x y + 4 x Expanding and collecting terms of the same sign gives: 4 2 3 2 3 3 2 3 2 4 20 x y z + 12 x y z + 12 x y z + 12 x y z + 12 x y z + 20 x y z 2 3 3 2 4 + 12 x y z + 12 x y z + 20 x y z >= 2 4 2 4 3 3 3 3 4 2 2 2 2 4 2 10 y z + 10 x z + 20 y z + 20 x z + 10 y z + 12 x y z + 10 x z 2 4 3 3 4 2 + 10 x y + 20 x y + 10 x y Dividing both sides by 2 gives: 4 2 3 2 3 3 2 3 2 4 10 x y z + 6 x y z + 6 x y z + 6 x y z + 6 x y z + 10 x y z 2 3 3 2 4 + 6 x y z + 6 x y z + 10 x y z >= 2 4 2 4 3 3 3 3 4 2 2 2 2 4 2 5 y z + 5 x z + 10 y z + 10 x z + 5 y z + 6 x y z + 5 x z 2 4 3 3 4 2 + 5 x y + 10 x y + 5 x y Expressing in terms of symmetric polynomials gives: 5 {4, 1, 1} + 6 {3, 2, 1} >= 5 {4, 2, 0} + 5 {3, 3, 0} + {2, 2, 2} This follows from the following majorizations: left side: [6 {3, 2, 1}, 5 {4, 1, 1}] right side: [{2, 2, 2}, 5 {3, 3, 0}, 5 {4, 2, 0}] (d17) notsure (c18) /* 2.47 */ trineq(csum(sec(A)*sec(B))>=12); To prove: sec(B) sec(C) + sec(A) sec(C) + sec(A) sec(B) >= 12 Removing the trigonometric expressions gives: 4 2 2 3 3 3 2 (4 a b c + (- 4 a b - 4 a b) c + (- 4 a b - 4 a b) c 4 2 3 3 2 4 + (4 a b - 4 a b - 4 a b + 4 a b) c) 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 /(c + (- b - a ) c + (- b + 2 a b - a ) c + b - a b - a b + a ) >= 12 2 2 2 2 2 2 2 2 2 Multiplying both sides by (c - b - a ) (c - b + a ) (c + b - a ) gives: 4 2 3 2 3 3 2 3 2 4 2 3 4 a b c - 4 a b c - 4 a b c - 4 a b c - 4 a b c + 4 a b c - 4 a b c 3 2 4 6 2 4 2 4 4 2 2 2 2 - 4 a b c + 4 a b c >= 12 c - 12 b c - 12 a c - 12 b c + 24 a b c 4 2 6 2 4 4 2 6 - 12 a c + 12 b - 12 a b - 12 a b + 12 a Expanding and collecting terms of the same sign gives: 2 4 4 2 4 4 2 4 2 4 4 12 b c + 4 a b c + 12 a c + 12 b c + 12 a c + 4 a b c + 4 a b c 2 4 4 2 6 2 3 2 3 3 2 + 12 a b + 12 a b >= 12 c + 4 a b c + 4 a b c + 4 a b c 2 2 2 3 2 2 3 3 2 6 6 + 24 a b c + 4 a b c + 4 a b c + 4 a b c + 12 b + 12 a Dividing both sides by 4 gives: 2 4 4 2 4 4 2 4 2 4 4 2 4 3 b c + a b c + 3 a c + 3 b c + 3 a c + a b c + a b c + 3 a b 4 2 6 2 3 2 3 3 2 2 2 2 3 2 + 3 a b >= 3 c + a b c + a b c + a b c + 6 a b c + a b c 2 3 3 2 6 6 + a b c + a b c + 3 b + 3 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 6 5 2 2 4 (3 z + (10 y + 10 x) z + (16 y + 35 x y + 16 x ) z 3 2 2 3 3 + (15 y + 49 x y + 49 x y + 15 x ) z 4 3 2 2 3 4 2 + (16 y + 49 x y + 63 x y + 49 x y + 16 x ) z 5 4 2 3 3 2 4 5 6 5 + (10 y + 35 x y + 49 x y + 49 x y + 35 x y + 10 x ) z + 3 y + 10 x y 2 4 3 3 4 2 5 6 + 16 x y + 15 x y + 16 x y + 10 x y + 3 x )/32 >= 6 5 2 2 4 (3 z + (10 y + 10 x) z + (29 y + 13 x y + 29 x ) z 3 2 2 3 3 + (41 y + 35 x y + 35 x y + 41 x ) z 4 3 2 2 3 4 2 + (29 y + 35 x y + 57 x y + 35 x y + 29 x ) z 5 4 2 3 3 2 4 5 6 5 + (10 y + 13 x y + 35 x y + 35 x y + 13 x y + 10 x ) z + 3 y + 10 x y 2 4 3 3 4 2 5 6 + 29 x y + 41 x y + 29 x y + 10 x y + 3 x )/32 Multiplying both sides by 32 gives: 6 5 5 2 4 4 2 4 3 3 3 z + 10 y z + 10 x z + 16 y z + 35 x y z + 16 x z + 15 y z 2 3 2 3 3 3 4 2 3 2 2 2 2 + 49 x y z + 49 x y z + 15 x z + 16 y z + 49 x y z + 63 x y z 3 2 4 2 5 4 2 3 3 2 + 49 x y z + 16 x z + 10 y z + 35 x y z + 49 x y z + 49 x y z 4 5 6 5 2 4 3 3 4 2 + 35 x y z + 10 x z + 3 y + 10 x y + 16 x y + 15 x y + 16 x y 5 6 6 5 5 2 4 4 2 4 + 10 x y + 3 x >= 3 z + 10 y z + 10 x z + 29 y z + 13 x y z + 29 x z 3 3 2 3 2 3 3 3 4 2 3 2 + 41 y z + 35 x y z + 35 x y z + 41 x z + 29 y z + 35 x y z 2 2 2 3 2 4 2 5 4 2 3 + 57 x y z + 35 x y z + 29 x z + 10 y z + 13 x y z + 35 x y z 3 2 4 5 6 5 2 4 3 3 + 35 x y z + 13 x y z + 10 x z + 3 y + 10 x y + 29 x y + 41 x y 4 2 5 6 + 29 x y + 10 x y + 3 x Expanding and collecting terms of the same sign gives: 4 2 3 2 3 3 2 2 2 2 3 2 22 x y z + 14 x y z + 14 x y z + 14 x y z + 6 x y z + 14 x y z 4 2 3 3 2 4 + 22 x y z + 14 x y z + 14 x y z + 22 x y z >= 2 4 2 4 3 3 3 3 4 2 4 2 2 4 13 y z + 13 x z + 26 y z + 26 x z + 13 y z + 13 x z + 13 x y 3 3 4 2 + 26 x y + 13 x y Expressing in terms of symmetric polynomials gives: 11 {4, 1, 1} + 14 {3, 2, 1} + {2, 2, 2} >= 13 {4, 2, 0} + 13 {3, 3, 0} This follows from the following majorizations: left side: [{2, 2, 2}, 14 {3, 2, 1}, 11 {4, 1, 1}] right side: [13 {3, 3, 0}, 13 {4, 2, 0}] (d18) notsure (c19) /* 2.49 */ trineq(csum(csc(A))>=2*sqrt(3)); To prove: csc(C) + csc(B) + csc(A) >= 2 sqrt(3) Removing the trigonometric expressions gives: (b + a) c + a b --------------- >= 2 sqrt(3) 2 K Multiplying both sides by 2 K gives: b c + a c + a b >= 4 sqrt(3) K Since 4 sqrt(3) is positive, and since (b + a) c + a b is positive, we can square both sides to get: 2 2 2 2 2 2 2 (b + 2 a b + a ) c + (2 a b + 2 a b) c + a b >= 4 3 2 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s - 48 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 48 c s + 48 b s + 48 a s + 48 a b c s + b c + 2 a b c + a c + 2 a b c 2 2 2 4 2 2 2 + 2 a b c + a b >= 48 s + 48 b c s + 48 a c s + 48 a b s Let s = (c+b+a)/2 . We get: 4 3 2 2 2 6 c + (24 b + 24 a) c + (37 b + 98 a b + 37 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 98 a b + 98 a b + 24 a ) c + 6 b + 24 a b + 37 a b + 24 a b 4 4 3 2 2 2 + 6 a >= 3 c + (24 b + 24 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 3 b + 24 a b + 42 a b + 24 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 3 c + 2 a b c + 2 a b c + 2 a b c + 3 b + 3 a >= 2 2 2 2 2 2 5 b c + 5 a c + 5 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (3 z + (8 y + 8 x) z + (13 y + 8 x y + 13 x ) z 3 2 2 3 4 3 2 2 3 + (8 y + 8 x y + 8 x y + 8 x ) z + 3 y + 8 x y + 13 x y + 8 x y 4 4 3 2 2 2 + 3 x )/8 >= (5 z + (10 y + 10 x) z + (15 y + 40 x y + 15 x ) z 3 2 2 3 4 3 2 2 3 + (10 y + 40 x y + 40 x y + 10 x ) z + 5 y + 10 x y + 15 x y + 10 x y 4 + 5 x )/16 Multiplying both sides by 16 gives: 4 3 3 2 2 2 2 2 3 6 z + 16 y z + 16 x z + 26 y z + 16 x y z + 26 x z + 16 y z 2 2 3 4 3 2 2 3 + 16 x y z + 16 x y z + 16 x z + 6 y + 16 x y + 26 x y + 16 x y 4 4 3 3 2 2 2 2 2 3 + 6 x >= 5 z + 10 y z + 10 x z + 15 y z + 40 x y z + 15 x z + 10 y z 2 2 3 4 3 2 2 3 4 + 40 x y z + 40 x y z + 10 x z + 5 y + 10 x y + 15 x y + 10 x y + 5 x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 6 y z + 6 x z + 11 y z + 11 x z + 6 y z + 6 x z + y + 6 x y 2 2 3 4 2 2 2 + 11 x y + 6 x y + x >= 24 x y z + 24 x y z + 24 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 12 {3, 1, 0} + 11 {2, 2, 0} >= 24 {2, 1, 1} This follows from the following majorizations: 11 {2, 2, 0} >= 11 {2, 1, 1} 12 {3, 1, 0} >= 12 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d19) true (c20) /* 2.50 */ trineq(csum(csc(A)^2)>=4); 2 2 2 To prove: csc (C) + csc (B) + csc (A) >= 4 Removing the trigonometric expressions gives: 2 2 2 2 2 (b + a ) c + a b -------------------- >= 4 2 4 K 2 Multiplying both sides by 4 K gives: 2 2 2 2 2 2 2 b c + a c + a b >= 16 K Replacing K^2 by F^2 gives: 2 2 2 2 2 2 (b + a ) c + a b >= 16 F Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 2 2 2 4 2 2 2 4 2 2 4 (b + a ) c + a b >= - c + (2 b + 2 a ) c - b + 2 a b - a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 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: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/8 >= (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 )/16 Multiplying both sides by 16 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d20) true (c21) /* 2.55 */ trineq(csum(csc(2*A))>=csum(csc(A))); To prove: csc(2 C) + csc(2 B) + csc(2 A) >= csc(C) + csc(B) + csc(A) Expanding the trigonometric expressions gives: csc(C) sec(C) csc(B) sec(B) csc(A) sec(A) ------------- + ------------- + ------------- >= csc(C) + csc(B) + csc(A) 2 2 2 Removing the trigonometric expressions gives: 2 2 6 4 2 2 4 4 6 2 4 4 2 6 2 ((b + a ) c + (- 2 b - a b - 2 a ) c + (b - a b - a b + a ) c 2 6 4 4 6 2 6 2 2 4 + a b - 2 a b + a b )/(2 K c + (- 2 K b - 2 K a ) c 4 2 2 4 2 6 2 4 4 2 + (- 2 K b + 4 K a b - 2 K a ) c + 2 K b - 2 K a b - 2 K a b 6 (b + a) c + a b + 2 K a ) >= --------------- 2 K 2 2 2 2 2 2 2 2 2 Multiplying both sides by 2 K (c - b - a ) (c - b + a ) (c + b - a ) gives: 2 6 2 6 4 4 2 2 4 4 4 6 2 2 4 2 4 2 2 b c + a c - 2 b c - a b c - 2 a c + b c - a b c - a b c 6 2 2 6 4 4 6 2 7 7 6 3 5 2 5 + a c + a b - 2 a b + a b >= b c + a c + a b c - b c - a b c 2 5 3 5 3 4 3 4 5 3 4 3 2 3 3 - a b c - a c - a b c - a b c - b c - a b c + 2 a b c 3 2 3 4 3 5 3 5 2 3 3 2 5 2 7 + 2 a b c - a b c - a c - a b c + 2 a b c - a b c + b c 6 2 5 3 4 4 3 5 2 6 7 7 + a b c - a b c - a b c - a b c - a b c + a b c + a c + a b 3 5 5 3 7 - a b - a b + a b Expanding and collecting terms of the same sign gives: 2 6 2 6 3 5 2 5 2 5 3 5 3 4 3 4 5 3 b c + a c + b c + a b c + a b c + a c + a b c + a b c + b c 4 3 4 3 5 3 6 2 5 2 5 2 6 2 2 5 + a b c + a b c + a c + b c + a b c + a b c + a c + a b c 3 4 4 3 5 2 2 6 3 5 5 3 6 2 + a b c + a b c + a b c + a b + a b + a b + a b >= 7 7 6 4 4 2 2 4 4 4 2 3 3 3 2 3 b c + a c + a b c + 2 b c + a b c + 2 a c + 2 a b c + 2 a b c 2 4 2 3 3 2 4 2 2 7 6 6 7 7 + a b c + 2 a b c + a b c + b c + a b c + a b c + a c + a b 4 4 7 + 2 a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 8 7 2 2 6 (4 z + (20 y + 20 x) z + (47 y + 90 x y + 47 x ) z 3 2 2 3 5 + (67 y + 193 x y + 193 x y + 67 x ) z 4 3 2 2 3 4 4 + (72 y + 253 x y + 342 x y + 253 x y + 72 x ) z 5 4 2 3 3 2 4 5 3 + (67 y + 253 x y + 380 x y + 380 x y + 253 x y + 67 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (47 y + 193 x y + 342 x y + 380 x y + 342 x y + 193 x y + 47 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (20 y + 90 x y + 193 x y + 253 x y + 253 x y + 193 x y + 90 x y 7 8 7 2 6 3 5 4 4 5 3 + 20 x ) z + 4 y + 20 x y + 47 x y + 67 x y + 72 x y + 67 x y 6 2 7 8 8 7 + 47 x y + 20 x y + 4 x )/256 >= (4 z + (20 y + 20 x) z 2 2 6 3 2 2 3 5 + (51 y + 82 x y + 51 x ) z + (95 y + 165 x y + 165 x y + 95 x ) z 4 3 2 2 3 4 4 + (120 y + 257 x y + 286 x y + 257 x y + 120 x ) z 5 4 2 3 3 2 4 5 3 + (95 y + 257 x y + 380 x y + 380 x y + 257 x y + 95 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (51 y + 165 x y + 286 x y + 380 x y + 286 x y + 165 x y + 51 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (20 y + 82 x y + 165 x y + 257 x y + 257 x y + 165 x y + 82 x y 7 8 7 2 6 3 5 4 4 5 3 + 20 x ) z + 4 y + 20 x y + 51 x y + 95 x y + 120 x y + 95 x y 6 2 7 8 + 51 x y + 20 x y + 4 x )/256 Multiplying both sides by 256 gives: 8 7 7 2 6 6 2 6 3 5 4 z + 20 y z + 20 x z + 47 y z + 90 x y z + 47 x z + 67 y z 2 5 2 5 3 5 4 4 3 4 2 2 4 + 193 x y z + 193 x y z + 67 x z + 72 y z + 253 x y z + 342 x y z 3 4 4 4 5 3 4 3 2 3 3 + 253 x y z + 72 x z + 67 y z + 253 x y z + 380 x y z 3 2 3 4 3 5 3 6 2 5 2 + 380 x y z + 253 x y z + 67 x z + 47 y z + 193 x y z 2 4 2 3 3 2 4 2 2 5 2 6 2 + 342 x y z + 380 x y z + 342 x y z + 193 x y z + 47 x z 7 6 2 5 3 4 4 3 5 2 + 20 y z + 90 x y z + 193 x y z + 253 x y z + 253 x y z + 193 x y z 6 7 8 7 2 6 3 5 4 4 + 90 x y z + 20 x z + 4 y + 20 x y + 47 x y + 67 x y + 72 x y 5 3 6 2 7 8 + 67 x y + 47 x y + 20 x y + 4 x >= 8 7 7 2 6 6 2 6 3 5 4 z + 20 y z + 20 x z + 51 y z + 82 x y z + 51 x z + 95 y z 2 5 2 5 3 5 4 4 3 4 + 165 x y z + 165 x y z + 95 x z + 120 y z + 257 x y z 2 2 4 3 4 4 4 5 3 4 3 + 286 x y z + 257 x y z + 120 x z + 95 y z + 257 x y z 2 3 3 3 2 3 4 3 5 3 6 2 + 380 x y z + 380 x y z + 257 x y z + 95 x z + 51 y z 5 2 2 4 2 3 3 2 4 2 2 5 2 + 165 x y z + 286 x y z + 380 x y z + 286 x y z + 165 x y z 6 2 7 6 2 5 3 4 4 3 + 51 x z + 20 y z + 82 x y z + 165 x y z + 257 x y z + 257 x y z 5 2 6 7 8 7 2 6 3 5 + 165 x y z + 82 x y z + 20 x z + 4 y + 20 x y + 51 x y + 95 x y 4 4 5 3 6 2 7 8 + 120 x y + 95 x y + 51 x y + 20 x y + 4 x Expanding and collecting terms of the same sign gives: 6 2 5 2 5 2 2 4 5 2 2 4 2 8 x y z + 28 x y z + 28 x y z + 56 x y z + 28 x y z + 56 x y z 4 2 2 5 2 6 2 5 5 2 6 + 56 x y z + 28 x y z + 8 x y z + 28 x y z + 28 x y z + 8 x y z >= 2 6 2 6 3 5 3 5 4 4 3 4 3 4 4 y z + 4 x z + 28 y z + 28 x z + 48 y z + 4 x y z + 4 x y z 4 4 5 3 4 3 4 3 5 3 6 2 6 2 + 48 x z + 28 y z + 4 x y z + 4 x y z + 28 x z + 4 y z + 4 x z 3 4 4 3 2 6 3 5 4 4 5 3 6 2 + 4 x y z + 4 x y z + 4 x y + 28 x y + 48 x y + 28 x y + 4 x y Dividing both sides by 4 gives: 6 2 5 2 5 2 2 4 5 2 2 4 2 2 x y z + 7 x y z + 7 x y z + 14 x y z + 7 x y z + 14 x y z 4 2 2 5 2 6 2 5 5 2 6 + 14 x y z + 7 x y z + 2 x y z + 7 x y z + 7 x y z + 2 x y z >= 2 6 2 6 3 5 3 5 4 4 3 4 3 4 4 4 y z + x z + 7 y z + 7 x z + 12 y z + x y z + x y z + 12 x z 5 3 4 3 4 3 5 3 6 2 6 2 3 4 4 3 + 7 y z + x y z + x y z + 7 x z + y z + x z + x y z + x y z 2 6 3 5 4 4 5 3 6 2 + x y + 7 x y + 12 x y + 7 x y + x y Expressing in terms of symmetric polynomials gives: {6, 1, 1} + 7 {5, 2, 1} + 7 {4, 2, 2} >= {6, 2, 0} + 7 {5, 3, 0} + 6 {4, 4, 0} + {4, 3, 1} This follows from the following majorizations: left side: [7 {4, 2, 2}, 7 {5, 2, 1}, {6, 1, 1}] right side: [{4, 3, 1}, 6 {4, 4, 0}, 7 {5, 3, 0}, {6, 2, 0}] (d21) notsure (c22) /* 2.59 */ trineq((1+cprod(cos(A)))/cprod(sin(A))>=sqrt(3)); cos(A) cos(B) cos(C) + 1 To prove: ------------------------ >= sqrt(3) sin(A) sin(B) sin(C) Removing the trigonometric expressions gives: 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 c + (- b - a ) c + (- b - 6 a b - a ) c + b - a b - a b + a - ------------------------------------------------------------------------ >= 3 64 K sqrt(3) 3 Multiplying both sides by 64 K gives: 6 2 4 2 4 4 2 2 2 2 4 2 6 2 4 4 2 6 - c + b c + a c + b c + 6 a b c + a c - b + a b + a b - a >= 3 64 sqrt(3) K Expanding and collecting terms of the same sign gives: 2 4 2 4 4 2 2 2 2 4 2 2 4 4 2 b c + a c + b c + 6 a b c + a c + a b + a b >= 6 6 6 3 c + b + a + 64 sqrt(3) K Replacing K^2 by F^2 gives: 2 2 4 4 2 2 4 2 2 4 4 2 (b + a ) c + (b + 6 a b + a ) c + a b + a b >= 6 6 6 2 c + b + a + 64 sqrt(3) F K Bringing all terms involving K to the right side yields: 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 - c + (b + a ) c + (b + 6 a b + a ) c - b + a b + a b - a >= 2 64 sqrt(3) F K 2 Since 64 sqrt(3) F is positive, and since 6 2 2 4 4 2 2 4 2 6 2 4 4 2 6 - c + (b + a ) c + (b + 6 a b + a ) c - b + a b + a b - a is positive, we can square both sides to get: 12 2 2 10 4 2 2 4 8 c + (- 2 b - 2 a ) c + (- b - 10 a b - a ) c 6 2 4 4 2 6 6 + (4 b + 12 a b + 12 a b + 4 a ) c 8 2 6 4 4 6 2 8 4 + (- b + 12 a b + 42 a b + 12 a b - a ) c 10 2 8 4 6 6 4 8 2 10 2 12 + (- 2 b - 10 a b + 12 a b + 12 a b - 10 a b - 2 a ) c + b 2 10 4 8 6 6 8 4 10 2 12 - 2 a b - a b + 4 a b - a b - 2 a b + a >= 4 4 4 4 4 3 12288 F s + (- 12288 F c - 12288 F b - 12288 F a) s 4 4 4 2 4 + ((12288 F b + 12288 F a) c + 12288 F a b) s - 12288 F a b c s Expanding and collecting terms of the same sign gives: 4 3 4 3 4 3 4 12 12288 F c s + 12288 F b s + 12288 F a s + 12288 F a b c s + c 6 6 2 4 6 4 2 6 6 6 2 6 4 4 4 4 + 4 b c + 12 a b c + 12 a b c + 4 a c + 12 a b c + 42 a b c 6 2 4 4 6 2 6 4 2 12 6 6 12 + 12 a b c + 12 a b c + 12 a b c + b + 4 a b + a >= 4 4 4 2 4 2 4 2 2 10 12288 F s + 12288 F b c s + 12288 F a c s + 12288 F a b s + 2 b c 2 10 4 8 2 2 8 4 8 8 4 8 4 10 2 + 2 a c + b c + 10 a b c + a c + b c + a c + 2 b c 2 8 2 8 2 2 10 2 2 10 4 8 8 4 10 2 + 10 a b c + 10 a b c + 2 a c + 2 a b + a b + a b + 2 a b Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 12 11 2 2 10 3 3 9 7 c + (24 b + 24 a) c + (12 b + 96 a b + 12 a ) c + (- 72 b - 72 a ) c 4 3 2 2 3 4 8 + (- 102 b - 360 a b - 228 a b - 360 a b - 102 a ) c 5 4 2 3 3 2 4 5 7 + (48 b - 240 a b - 384 a b - 384 a b - 240 a b + 48 a ) c 6 5 2 4 3 3 4 2 5 6 + (172 b + 480 a b + 228 a b + 192 a b + 228 a b + 480 a b + 172 a ) 6 7 6 2 5 3 4 4 3 5 2 c + (48 b + 480 a b + 768 a b + 624 a b + 624 a b + 768 a b 6 7 5 8 7 2 6 3 5 + 480 a b + 48 a ) c + (- 102 b - 240 a b + 228 a b + 624 a b 4 4 5 3 6 2 7 8 4 + 582 a b + 624 a b + 228 a b - 240 a b - 102 a ) c 9 8 2 7 3 6 4 5 5 4 + (- 72 b - 360 a b - 384 a b + 192 a b + 624 a b + 624 a b 6 3 7 2 8 9 3 + 192 a b - 384 a b - 360 a b - 72 a ) c 10 2 8 3 7 4 6 5 5 6 4 + (12 b - 228 a b - 384 a b + 228 a b + 768 a b + 228 a b 7 3 8 2 10 2 11 10 3 8 - 384 a b - 228 a b + 12 a ) c + (24 b + 96 a b - 360 a b 4 7 5 6 6 5 7 4 8 3 10 - 240 a b + 480 a b + 480 a b - 240 a b - 360 a b + 96 a b 11 12 11 2 10 3 9 4 8 5 7 + 24 a ) c + 7 b + 24 a b + 12 a b - 72 a b - 102 a b + 48 a b 6 6 7 5 8 4 9 3 10 2 11 + 172 a b + 48 a b - 102 a b - 72 a b + 12 a b + 24 a b 12 12 11 2 2 10 + 7 a >= 3 c + (24 b + 24 a) c + (32 b + 96 a b + 32 a ) c 3 3 9 4 3 2 2 3 4 + (- 72 b - 72 a ) c + (- 146 b - 360 a b - 272 a b - 360 a b - 146 a ) 8 5 4 2 3 3 2 4 5 7 c + (48 b - 240 a b - 384 a b - 384 a b - 240 a b + 48 a ) c 6 5 2 4 3 3 4 2 5 6 + (228 b + 480 a b + 252 a b + 192 a b + 252 a b + 480 a b + 228 a ) 6 7 6 2 5 3 4 4 3 5 2 c + (48 b + 480 a b + 768 a b + 624 a b + 624 a b + 768 a b 6 7 5 8 7 2 6 3 5 + 480 a b + 48 a ) c + (- 146 b - 240 a b + 252 a b + 624 a b 4 4 5 3 6 2 7 8 4 + 558 a b + 624 a b + 252 a b - 240 a b - 146 a ) c 9 8 2 7 3 6 4 5 5 4 + (- 72 b - 360 a b - 384 a b + 192 a b + 624 a b + 624 a b 6 3 7 2 8 9 3 + 192 a b - 384 a b - 360 a b - 72 a ) c 10 2 8 3 7 4 6 5 5 6 4 + (32 b - 272 a b - 384 a b + 252 a b + 768 a b + 252 a b 7 3 8 2 10 2 11 10 3 8 - 384 a b - 272 a b + 32 a ) c + (24 b + 96 a b - 360 a b 4 7 5 6 6 5 7 4 8 3 10 - 240 a b + 480 a b + 480 a b - 240 a b - 360 a b + 96 a b 11 12 11 2 10 3 9 4 8 5 7 + 24 a ) c + 3 b + 24 a b + 32 a b - 72 a b - 146 a b + 48 a b 6 6 7 5 8 4 9 3 10 2 11 12 + 228 a b + 48 a b - 146 a b - 72 a b + 32 a b + 24 a b + 3 a Expanding and collecting terms of the same sign gives: 12 4 8 2 2 8 4 8 8 4 4 4 4 8 4 4 c + 44 b c + 44 a b c + 44 a c + 44 b c + 24 a b c + 44 a c 2 8 2 8 2 2 12 4 8 8 4 12 + 44 a b c + 44 a b c + 4 b + 44 a b + 44 a b + 4 a >= 2 10 2 10 6 6 2 4 6 4 2 6 6 6 20 b c + 20 a c + 56 b c + 24 a b c + 24 a b c + 56 a c 2 6 4 6 2 4 10 2 4 6 2 6 4 2 + 24 a b c + 24 a b c + 20 b c + 24 a b c + 24 a b c 10 2 2 10 6 6 10 2 + 20 a c + 20 a b + 56 a b + 20 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 12 11 2 2 10 (24 z + (144 y + 144 x) z + (462 y + 748 x y + 462 x ) z 3 2 2 3 9 + (990 y + 2090 x y + 2090 x y + 990 x ) z 4 3 2 2 3 4 8 + (1623 y + 3918 x y + 5206 x y + 3918 x y + 1623 x ) z 5 4 2 3 3 2 4 5 7 + (2136 y + 5664 x y + 8776 x y + 8776 x y + 5664 x y + 2136 x ) z 6 5 2 4 3 3 4 2 5 + (2346 y + 6708 x y + 11570 x y + 11952 x y + 11570 x y + 6708 x y 6 6 7 6 2 5 3 4 4 3 + 2346 x ) z + (2136 y + 6708 x y + 12568 x y + 11724 x y + 11724 x y 5 2 6 7 5 + 12568 x y + 6708 x y + 2136 x ) z 8 7 2 6 3 5 4 4 5 3 + (1623 y + 5664 x y + 11570 x y + 11724 x y + 9006 x y + 11724 x y 6 2 7 8 4 + 11570 x y + 5664 x y + 1623 x ) z 9 8 2 7 3 6 4 5 5 4 + (990 y + 3918 x y + 8776 x y + 11952 x y + 11724 x y + 11724 x y 6 3 7 2 8 9 3 + 11952 x y + 8776 x y + 3918 x y + 990 x ) z 10 9 2 8 3 7 4 6 5 5 + (462 y + 2090 x y + 5206 x y + 8776 x y + 11570 x y + 12568 x y 6 4 7 3 8 2 9 10 2 + 11570 x y + 8776 x y + 5206 x y + 2090 x y + 462 x ) z 11 10 2 9 3 8 4 7 5 6 + (144 y + 748 x y + 2090 x y + 3918 x y + 5664 x y + 6708 x y 6 5 7 4 8 3 9 2 10 11 + 6708 x y + 5664 x y + 3918 x y + 2090 x y + 748 x y + 144 x ) z 12 11 2 10 3 9 4 8 5 7 + 24 y + 144 x y + 462 x y + 990 x y + 1623 x y + 2136 x y 6 6 7 5 8 4 9 3 10 2 11 + 2346 x y + 2136 x y + 1623 x y + 990 x y + 462 x y + 144 x y 12 12 11 + 24 x )/1024 >= (24 z + (144 y + 144 x) z 2 2 10 3 2 2 3 + (462 y + 748 x y + 462 x ) z + (990 y + 2090 x y + 2090 x y + 990 x ) 9 4 3 2 2 3 4 8 z + (1623 y + 3918 x y + 4950 x y + 3918 x y + 1623 x ) z 5 4 2 3 3 2 4 5 7 + (2136 y + 5664 x y + 7752 x y + 7752 x y + 5664 x y + 2136 x ) z 6 5 2 4 3 3 4 2 5 + (2346 y + 6708 x y + 9522 x y + 11440 x y + 9522 x y + 6708 x y 6 6 7 6 2 5 3 4 4 3 + 2346 x ) z + (2136 y + 6708 x y + 10008 x y + 14796 x y + 14796 x y 5 2 6 7 5 + 10008 x y + 6708 x y + 2136 x ) z 8 7 2 6 3 5 4 4 5 3 + (1623 y + 5664 x y + 9522 x y + 14796 x y + 18990 x y + 14796 x y 6 2 7 8 4 + 9522 x y + 5664 x y + 1623 x ) z 9 8 2 7 3 6 4 5 5 4 + (990 y + 3918 x y + 7752 x y + 11440 x y + 14796 x y + 14796 x y 6 3 7 2 8 9 3 + 11440 x y + 7752 x y + 3918 x y + 990 x ) z 10 9 2 8 3 7 4 6 5 5 + (462 y + 2090 x y + 4950 x y + 7752 x y + 9522 x y + 10008 x y 6 4 7 3 8 2 9 10 2 + 9522 x y + 7752 x y + 4950 x y + 2090 x y + 462 x ) z 11 10 2 9 3 8 4 7 5 6 + (144 y + 748 x y + 2090 x y + 3918 x y + 5664 x y + 6708 x y 6 5 7 4 8 3 9 2 10 11 + 6708 x y + 5664 x y + 3918 x y + 2090 x y + 748 x y + 144 x ) z 12 11 2 10 3 9 4 8 5 7 + 24 y + 144 x y + 462 x y + 990 x y + 1623 x y + 2136 x y 6 6 7 5 8 4 9 3 10 2 11 + 2346 x y + 2136 x y + 1623 x y + 990 x y + 462 x y + 144 x y 12 + 24 x )/1024 Multiplying both sides by 1024 gives: 12 11 11 2 10 10 2 10 24 z + 144 y z + 144 x z + 462 y z + 748 x y z + 462 x z 3 9 2 9 2 9 3 9 4 8 + 990 y z + 2090 x y z + 2090 x y z + 990 x z + 1623 y z 3 8 2 2 8 3 8 4 8 5 7 + 3918 x y z + 5206 x y z + 3918 x y z + 1623 x z + 2136 y z 4 7 2 3 7 3 2 7 4 7 5 7 + 5664 x y z + 8776 x y z + 8776 x y z + 5664 x y z + 2136 x z 6 6 5 6 2 4 6 3 3 6 4 2 6 + 2346 y z + 6708 x y z + 11570 x y z + 11952 x y z + 11570 x y z 5 6 6 6 7 5 6 5 2 5 5 + 6708 x y z + 2346 x z + 2136 y z + 6708 x y z + 12568 x y z 3 4 5 4 3 5 5 2 5 6 5 7 5 + 11724 x y z + 11724 x y z + 12568 x y z + 6708 x y z + 2136 x z 8 4 7 4 2 6 4 3 5 4 4 4 4 + 1623 y z + 5664 x y z + 11570 x y z + 11724 x y z + 9006 x y z 5 3 4 6 2 4 7 4 8 4 9 3 + 11724 x y z + 11570 x y z + 5664 x y z + 1623 x z + 990 y z 8 3 2 7 3 3 6 3 4 5 3 + 3918 x y z + 8776 x y z + 11952 x y z + 11724 x y z 5 4 3 6 3 3 7 2 3 8 3 9 3 + 11724 x y z + 11952 x y z + 8776 x y z + 3918 x y z + 990 x z 10 2 9 2 2 8 2 3 7 2 4 6 2 + 462 y z + 2090 x y z + 5206 x y z + 8776 x y z + 11570 x y z 5 5 2 6 4 2 7 3 2 8 2 2 + 12568 x y z + 11570 x y z + 8776 x y z + 5206 x y z 9 2 10 2 11 10 2 9 + 2090 x y z + 462 x z + 144 y z + 748 x y z + 2090 x y z 3 8 4 7 5 6 6 5 7 4 + 3918 x y z + 5664 x y z + 6708 x y z + 6708 x y z + 5664 x y z 8 3 9 2 10 11 12 11 + 3918 x y z + 2090 x y z + 748 x y z + 144 x z + 24 y + 144 x y 2 10 3 9 4 8 5 7 6 6 7 5 + 462 x y + 990 x y + 1623 x y + 2136 x y + 2346 x y + 2136 x y 8 4 9 3 10 2 11 12 + 1623 x y + 990 x y + 462 x y + 144 x y + 24 x >= 12 11 11 2 10 10 2 10 24 z + 144 y z + 144 x z + 462 y z + 748 x y z + 462 x z 3 9 2 9 2 9 3 9 4 8 + 990 y z + 2090 x y z + 2090 x y z + 990 x z + 1623 y z 3 8 2 2 8 3 8 4 8 5 7 + 3918 x y z + 4950 x y z + 3918 x y z + 1623 x z + 2136 y z 4 7 2 3 7 3 2 7 4 7 5 7 + 5664 x y z + 7752 x y z + 7752 x y z + 5664 x y z + 2136 x z 6 6 5 6 2 4 6 3 3 6 4 2 6 + 2346 y z + 6708 x y z + 9522 x y z + 11440 x y z + 9522 x y z 5 6 6 6 7 5 6 5 2 5 5 + 6708 x y z + 2346 x z + 2136 y z + 6708 x y z + 10008 x y z 3 4 5 4 3 5 5 2 5 6 5 7 5 + 14796 x y z + 14796 x y z + 10008 x y z + 6708 x y z + 2136 x z 8 4 7 4 2 6 4 3 5 4 4 4 4 + 1623 y z + 5664 x y z + 9522 x y z + 14796 x y z + 18990 x y z 5 3 4 6 2 4 7 4 8 4 9 3 + 14796 x y z + 9522 x y z + 5664 x y z + 1623 x z + 990 y z 8 3 2 7 3 3 6 3 4 5 3 + 3918 x y z + 7752 x y z + 11440 x y z + 14796 x y z 5 4 3 6 3 3 7 2 3 8 3 9 3 + 14796 x y z + 11440 x y z + 7752 x y z + 3918 x y z + 990 x z 10 2 9 2 2 8 2 3 7 2 4 6 2 + 462 y z + 2090 x y z + 4950 x y z + 7752 x y z + 9522 x y z 5 5 2 6 4 2 7 3 2 8 2 2 + 10008 x y z + 9522 x y z + 7752 x y z + 4950 x y z 9 2 10 2 11 10 2 9 + 2090 x y z + 462 x z + 144 y z + 748 x y z + 2090 x y z 3 8 4 7 5 6 6 5 7 4 + 3918 x y z + 5664 x y z + 6708 x y z + 6708 x y z + 5664 x y z 8 3 9 2 10 11 12 11 + 3918 x y z + 2090 x y z + 748 x y z + 144 x z + 24 y + 144 x y 2 10 3 9 4 8 5 7 6 6 7 5 + 462 x y + 990 x y + 1623 x y + 2136 x y + 2346 x y + 2136 x y 8 4 9 3 10 2 11 12 + 1623 x y + 990 x y + 462 x y + 144 x y + 24 x Expanding and collecting terms of the same sign gives: 2 2 8 2 3 7 3 2 7 2 4 6 3 3 6 256 x y z + 1024 x y z + 1024 x y z + 2048 x y z + 512 x y z 4 2 6 2 5 5 5 2 5 2 6 4 + 2048 x y z + 2560 x y z + 2560 x y z + 2048 x y z 6 2 4 2 7 3 3 6 3 6 3 3 7 2 3 + 2048 x y z + 1024 x y z + 512 x y z + 512 x y z + 1024 x y z 2 8 2 3 7 2 4 6 2 5 5 2 6 4 2 + 256 x y z + 1024 x y z + 2048 x y z + 2560 x y z + 2048 x y z 7 3 2 8 2 2 3 4 5 4 3 5 + 1024 x y z + 256 x y z >= 3072 x y z + 3072 x y z 3 5 4 4 4 4 5 3 4 4 5 3 + 3072 x y z + 9984 x y z + 3072 x y z + 3072 x y z 5 4 3 + 3072 x y z 2 2 2 Dividing both sides by 256 x y z gives: 6 5 5 2 4 4 2 4 3 3 3 3 z + 4 y z + 4 x z + 8 y z + 2 x y z + 8 x z + 10 y z + 10 x z 4 2 4 2 5 4 4 5 6 5 + 8 y z + 8 x z + 4 y z + 2 x y z + 2 x y z + 4 x z + y + 4 x y 2 4 3 3 4 2 5 6 + 8 x y + 10 x y + 8 x y + 4 x y + x >= 2 3 2 3 3 2 2 2 2 3 2 2 3 12 x y z + 12 x y z + 12 x y z + 39 x y z + 12 x y z + 12 x y z 3 2 + 12 x y z Expressing in terms of symmetric polynomials gives: {6, 0, 0} + 8 {5, 1, 0} + 16 {4, 2, 0} + 2 {4, 1, 1} + 10 {3, 3, 0} >= 24 {3, 2, 1} + 13 {2, 2, 2} This follows from the following majorizations: {6, 0, 0} >= {3, 2, 1} 8 {5, 1, 0} >= 8 {3, 2, 1} 15 {4, 2, 0} >= 15 {3, 2, 1} {4, 2, 0} >= {2, 2, 2} 2 {4, 1, 1} >= 2 {2, 2, 2} 10 {3, 3, 0} >= 10 {2, 2, 2} (d22) true (c23) /* 2.62 */ trineq(2*csum(cot(A))>=csum(csc(A))); To prove: 2 (cot(C) + cot(B) + cot(A)) >= csc(C) + csc(B) + csc(A) Removing the trigonometric expressions gives: 2 2 2 c + b + a (b + a) c + a b ------------ >= --------------- 2 K 2 K Multiplying both sides by 2 K 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. (d23) true (c24) /* 3.11 */ trineq(-1+4*r/R-(r/R)^2<=csum(cos(A)*cos(B))); 2 r 4 r To prove: cos(B) cos(C) + cos(A) cos(C) + cos(A) cos(B) >= - -- + --- - 1 2 R R Removing the trigonometric expressions gives: 5 4 3 3 3 5 4 4 5 5 - ((b + a) c - a b c + (- 2 b - 2 a ) c + (b - a b - a b + a ) c + a b 2 2 3 3 5 2 2 2 r - 4 R r + R - 2 a b + a b)/(4 a b c ) >= - --------------- 2 R 2 2 2 2 Multiplying both sides by 4 R a b c gives: 2 5 2 5 2 4 2 3 3 2 3 3 2 5 2 4 - R b c - R a c + R a b c + 2 R b c + 2 R a c - R b c + R a b c 2 4 2 5 2 5 2 3 3 2 5 + R a b c - R a c - R a b + 2 R a b - R a b >= 2 2 2 2 2 2 2 2 2 2 2 - 4 a b c r + 16 R a b c r - 4 R a b c Expanding and collecting terms of the same sign gives: 2 2 2 2 2 4 2 3 3 2 3 3 2 2 2 2 2 4 4 a b c r + R a b c + 2 R b c + 2 R a c + 4 R a b c + R a b c 2 4 2 3 3 2 2 2 2 5 2 5 2 5 + R a b c + 2 R a b >= 16 R a b c r + R b c + R a c + R b c 2 5 2 5 2 5 + R a c + R a b + R a b Let r = K/s . Let R = a*b*c/(4*K) . We get: 3 3 6 2 5 5 2 5 4 4 4 3 6 6 3 3 ((a b c + (2 a b + 2 a b ) c + 4 a b c + (a b + a b ) c 5 5 2 2 4 2 2 2 2 2 + 2 a b c ) s + 64 K a b c )/(16 K s ) >= 2 3 3 2 7 2 7 7 2 3 3 7 7 3 2 (((a b + a b ) c + (a b + a b ) c + (a b + a b ) c ) s 2 3 3 3 2 + 64 K a b c )/(16 K s) 2 2 Multiplying both sides by 16 K s gives: 3 3 6 2 2 5 5 2 5 2 5 2 4 4 4 2 3 6 3 2 a b c s + 2 a b c s + 2 a b c s + 4 a b c s + a b c s 6 3 3 2 5 5 2 2 4 2 2 2 + a b c s + 2 a b c s + 64 K a b c >= 2 3 7 2 3 2 7 2 2 7 3 2 7 2 3 2 3 7 2 2 a b c s + a b c s + a b c s + a b c s + a b c s 7 3 2 2 2 3 3 3 + a b c s + 64 K a b c s Replacing K^2 by F^2 gives: 3 3 6 2 5 5 2 5 4 4 4 3 6 6 3 3 (a b c + (2 a b + 2 a b ) c + 4 a b c + (a b + a b ) c 5 5 2 2 4 2 2 2 2 3 3 2 7 2 7 7 2 3 + 2 a b c ) s + 64 F a b c >= ((a b + a b ) c + (a b + a b ) c 3 7 7 3 2 2 2 3 3 3 + (a b + a b ) c ) s + 64 F a b c s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 10 2 4 3 3 4 2 8 (a b c + (- 4 a b + a b - 4 a b ) c 2 5 3 4 4 3 5 2 7 + (2 a b + 2 a b + 2 a b + 2 a b ) c 2 6 3 5 4 4 5 3 6 2 6 + (10 a b + 5 a b + 10 a b + 5 a b + 10 a b ) c 2 7 3 6 4 5 5 4 6 3 7 2 5 + (2 a b + 5 a b + 10 a b + 10 a b + 5 a b + 2 a b ) c 2 8 3 7 4 6 5 5 6 4 7 3 8 2 + (- 4 a b + 2 a b + 10 a b + 10 a b + 10 a b + 2 a b - 4 a b ) 4 3 8 4 7 5 6 6 5 7 4 8 3 3 c + (a b + 2 a b + 5 a b + 5 a b + 2 a b + a b ) c 2 10 4 8 5 7 6 6 7 5 8 4 10 2 2 + (a b - 4 a b + 2 a b + 10 a b + 2 a b - 4 a b + a b ) c ) 2 3 3 2 9 2 4 3 3 4 2 8 /4 >= ((a b + a b ) c + (2 a b - 4 a b + 2 a b ) c 2 5 3 4 4 3 5 2 7 3 5 5 3 6 + (a b - 5 a b - 5 a b + a b ) c + (16 a b + 16 a b ) c 2 7 3 6 4 5 5 4 6 3 7 2 5 + (a b + 16 a b + 16 a b + 16 a b + 16 a b + a b ) c 2 8 3 7 5 5 7 3 8 2 4 + (2 a b - 5 a b + 16 a b - 5 a b + 2 a b ) c 2 9 3 8 4 7 5 6 6 5 7 4 8 3 + (a b - 4 a b - 5 a b + 16 a b + 16 a b - 5 a b - 4 a b 9 2 3 3 9 4 8 5 7 7 5 8 4 9 3 2 + a b ) c + (a b + 2 a b + a b + a b + 2 a b + a b ) c )/4 Multiplying both sides by 4 gives: 2 2 10 2 4 8 3 3 8 4 2 8 2 5 7 3 4 7 a b c - 4 a b c + a b c - 4 a b c + 2 a b c + 2 a b c 4 3 7 5 2 7 2 6 6 3 5 6 4 4 6 + 2 a b c + 2 a b c + 10 a b c + 5 a b c + 10 a b c 5 3 6 6 2 6 2 7 5 3 6 5 4 5 5 + 5 a b c + 10 a b c + 2 a b c + 5 a b c + 10 a b c 5 4 5 6 3 5 7 2 5 2 8 4 3 7 4 + 10 a b c + 5 a b c + 2 a b c - 4 a b c + 2 a b c 4 6 4 5 5 4 6 4 4 7 3 4 8 2 4 3 8 3 + 10 a b c + 10 a b c + 10 a b c + 2 a b c - 4 a b c + a b c 4 7 3 5 6 3 6 5 3 7 4 3 8 3 3 2 10 2 + 2 a b c + 5 a b c + 5 a b c + 2 a b c + a b c + a b c 4 8 2 5 7 2 6 6 2 7 5 2 8 4 2 - 4 a b c + 2 a b c + 10 a b c + 2 a b c - 4 a b c 10 2 2 2 3 9 3 2 9 2 4 8 3 3 8 4 2 8 + a b c >= a b c + a b c + 2 a b c - 4 a b c + 2 a b c 2 5 7 3 4 7 4 3 7 5 2 7 3 5 6 5 3 6 + a b c - 5 a b c - 5 a b c + a b c + 16 a b c + 16 a b c 2 7 5 3 6 5 4 5 5 5 4 5 6 3 5 7 2 5 + a b c + 16 a b c + 16 a b c + 16 a b c + 16 a b c + a b c 2 8 4 3 7 4 5 5 4 7 3 4 8 2 4 2 9 3 + 2 a b c - 5 a b c + 16 a b c - 5 a b c + 2 a b c + a b c 3 8 3 4 7 3 5 6 3 6 5 3 7 4 3 - 4 a b c - 5 a b c + 16 a b c + 16 a b c - 5 a b c 8 3 3 9 2 3 3 9 2 4 8 2 5 7 2 7 5 2 - 4 a b c + a b c + a b c + 2 a b c + a b c + a b c 8 4 2 9 3 2 + 2 a b c + a b c Expanding and collecting terms of the same sign gives: 2 2 10 3 3 8 2 5 7 3 4 7 4 3 7 5 2 7 a b c + 5 a b c + a b c + 7 a b c + 7 a b c + a b c 2 6 6 4 4 6 6 2 6 2 7 5 7 2 5 3 7 4 + 10 a b c + 10 a b c + 10 a b c + a b c + a b c + 7 a b c 4 6 4 6 4 4 7 3 4 3 8 3 4 7 3 + 10 a b c + 10 a b c + 7 a b c + 5 a b c + 7 a b c 7 4 3 8 3 3 2 10 2 5 7 2 6 6 2 7 5 2 + 7 a b c + 5 a b c + a b c + a b c + 10 a b c + a b c 10 2 2 2 3 9 3 2 9 2 4 8 4 2 8 3 5 6 + a b c >= a b c + a b c + 6 a b c + 6 a b c + 11 a b c 5 3 6 3 6 5 4 5 5 5 4 5 6 3 5 + 11 a b c + 11 a b c + 6 a b c + 6 a b c + 11 a b c 2 8 4 5 5 4 8 2 4 2 9 3 5 6 3 6 5 3 + 6 a b c + 6 a b c + 6 a b c + a b c + 11 a b c + 11 a b c 9 2 3 3 9 2 4 8 2 8 4 2 9 3 2 + a b c + a b c + 6 a b c + 6 a b c + a b c Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 12 3 2 2 3 11 ((14 y + 28 x y + 14 x ) z + (108 y + 324 x y + 324 x y + 108 x ) z 4 3 2 2 3 4 10 + (393 y + 1588 x y + 2390 x y + 1588 x y + 393 x ) z 5 4 2 3 3 2 4 5 9 + (881 y + 4429 x y + 8882 x y + 8882 x y + 4429 x y + 881 x ) z 6 5 2 4 3 3 4 2 5 + (1375 y + 8101 x y + 20219 x y + 26986 x y + 20219 x y + 8101 x y 6 8 7 6 2 5 3 4 + 1375 x ) z + (1586 y + 10666 x y + 31582 x y + 52518 x y 4 3 5 2 6 7 7 + 52518 x y + 31582 x y + 10666 x y + 1586 x ) z 8 7 2 6 3 5 4 4 + (1375 y + 10666 x y + 36330 x y + 71694 x y + 89310 x y 5 3 6 2 7 8 6 + 71694 x y + 36330 x y + 10666 x y + 1375 x ) z 9 8 2 7 3 6 4 5 + (881 y + 8101 x y + 31582 x y + 71694 x y + 105950 x y 5 4 6 3 7 2 8 9 5 + 105950 x y + 71694 x y + 31582 x y + 8101 x y + 881 x ) z 10 9 2 8 3 7 4 6 + (393 y + 4429 x y + 20219 x y + 52518 x y + 89310 x y 5 5 6 4 7 3 8 2 9 + 105950 x y + 89310 x y + 52518 x y + 20219 x y + 4429 x y 10 4 11 10 2 9 3 8 4 7 + 393 x ) z + (108 y + 1588 x y + 8882 x y + 26986 x y + 52518 x y 5 6 6 5 7 4 8 3 9 2 + 71694 x y + 71694 x y + 52518 x y + 26986 x y + 8882 x y 10 11 3 12 11 2 10 3 9 + 1588 x y + 108 x ) z + (14 y + 324 x y + 2390 x y + 8882 x y 4 8 5 7 6 6 7 5 8 4 + 20219 x y + 31582 x y + 36330 x y + 31582 x y + 20219 x y 9 3 10 2 11 12 2 + 8882 x y + 2390 x y + 324 x y + 14 x ) z 12 2 11 3 10 4 9 5 8 6 7 + (28 x y + 324 x y + 1588 x y + 4429 x y + 8101 x y + 10666 x y 7 6 8 5 9 4 10 3 11 2 12 + 10666 x y + 8101 x y + 4429 x y + 1588 x y + 324 x y + 28 x y) 2 12 3 11 4 10 5 9 6 8 7 7 z + 14 x y + 108 x y + 393 x y + 881 x y + 1375 x y + 1586 x y 8 6 9 5 10 4 11 3 12 2 + 1375 x y + 881 x y + 393 x y + 108 x y + 14 x y )/16384 >= 2 2 12 3 2 2 3 11 ((14 y + 28 x y + 14 x ) z + (108 y + 324 x y + 324 x y + 108 x ) z 4 3 2 2 3 4 10 + (393 y + 1524 x y + 2262 x y + 1524 x y + 393 x ) z 5 4 2 3 3 2 4 5 9 + (881 y + 4237 x y + 8306 x y + 8306 x y + 4237 x y + 881 x ) z 6 5 2 4 3 3 4 2 5 + (1375 y + 8037 x y + 19515 x y + 25706 x y + 19515 x y + 8037 x y 6 8 7 6 2 5 3 4 + 1375 x ) z + (1586 y + 10986 x y + 31902 x y + 51878 x y 4 3 5 2 6 7 7 + 51878 x y + 31902 x y + 10986 x y + 1586 x ) z 8 7 2 6 3 5 4 4 + (1375 y + 10986 x y + 37482 x y + 72718 x y + 89694 x y 5 3 6 2 7 8 6 + 72718 x y + 37482 x y + 10986 x y + 1375 x ) z 9 8 2 7 3 6 4 5 + (881 y + 8037 x y + 31902 x y + 72718 x y + 106974 x y 5 4 6 3 7 2 8 9 5 + 106974 x y + 72718 x y + 31902 x y + 8037 x y + 881 x ) z 10 9 2 8 3 7 4 6 + (393 y + 4237 x y + 19515 x y + 51878 x y + 89694 x y 5 5 6 4 7 3 8 2 9 + 106974 x y + 89694 x y + 51878 x y + 19515 x y + 4237 x y 10 4 11 10 2 9 3 8 4 7 + 393 x ) z + (108 y + 1524 x y + 8306 x y + 25706 x y + 51878 x y 5 6 6 5 7 4 8 3 9 2 + 72718 x y + 72718 x y + 51878 x y + 25706 x y + 8306 x y 10 11 3 12 11 2 10 3 9 + 1524 x y + 108 x ) z + (14 y + 324 x y + 2262 x y + 8306 x y 4 8 5 7 6 6 7 5 8 4 + 19515 x y + 31902 x y + 37482 x y + 31902 x y + 19515 x y 9 3 10 2 11 12 2 + 8306 x y + 2262 x y + 324 x y + 14 x ) z 12 2 11 3 10 4 9 5 8 6 7 + (28 x y + 324 x y + 1524 x y + 4237 x y + 8037 x y + 10986 x y 7 6 8 5 9 4 10 3 11 2 12 + 10986 x y + 8037 x y + 4237 x y + 1524 x y + 324 x y + 28 x y) 2 12 3 11 4 10 5 9 6 8 7 7 z + 14 x y + 108 x y + 393 x y + 881 x y + 1375 x y + 1586 x y 8 6 9 5 10 4 11 3 12 2 + 1375 x y + 881 x y + 393 x y + 108 x y + 14 x y )/16384 Multiplying both sides by 16384 gives: 2 12 12 2 12 3 11 2 11 2 11 14 y z + 28 x y z + 14 x z + 108 y z + 324 x y z + 324 x y z 3 11 4 10 3 10 2 2 10 3 10 + 108 x z + 393 y z + 1588 x y z + 2390 x y z + 1588 x y z 4 10 5 9 4 9 2 3 9 3 2 9 + 393 x z + 881 y z + 4429 x y z + 8882 x y z + 8882 x y z 4 9 5 9 6 8 5 8 2 4 8 + 4429 x y z + 881 x z + 1375 y z + 8101 x y z + 20219 x y z 3 3 8 4 2 8 5 8 6 8 7 7 + 26986 x y z + 20219 x y z + 8101 x y z + 1375 x z + 1586 y z 6 7 2 5 7 3 4 7 4 3 7 + 10666 x y z + 31582 x y z + 52518 x y z + 52518 x y z 5 2 7 6 7 7 7 8 6 7 6 + 31582 x y z + 10666 x y z + 1586 x z + 1375 y z + 10666 x y z 2 6 6 3 5 6 4 4 6 5 3 6 + 36330 x y z + 71694 x y z + 89310 x y z + 71694 x y z 6 2 6 7 6 8 6 9 5 8 5 + 36330 x y z + 10666 x y z + 1375 x z + 881 y z + 8101 x y z 2 7 5 3 6 5 4 5 5 5 4 5 + 31582 x y z + 71694 x y z + 105950 x y z + 105950 x y z 6 3 5 7 2 5 8 5 9 5 10 4 + 71694 x y z + 31582 x y z + 8101 x y z + 881 x z + 393 y z 9 4 2 8 4 3 7 4 4 6 4 + 4429 x y z + 20219 x y z + 52518 x y z + 89310 x y z 5 5 4 6 4 4 7 3 4 8 2 4 + 105950 x y z + 89310 x y z + 52518 x y z + 20219 x y z 9 4 10 4 11 3 10 3 2 9 3 + 4429 x y z + 393 x z + 108 y z + 1588 x y z + 8882 x y z 3 8 3 4 7 3 5 6 3 6 5 3 + 26986 x y z + 52518 x y z + 71694 x y z + 71694 x y z 7 4 3 8 3 3 9 2 3 10 3 11 3 + 52518 x y z + 26986 x y z + 8882 x y z + 1588 x y z + 108 x z 12 2 11 2 2 10 2 3 9 2 4 8 2 + 14 y z + 324 x y z + 2390 x y z + 8882 x y z + 20219 x y z 5 7 2 6 6 2 7 5 2 8 4 2 + 31582 x y z + 36330 x y z + 31582 x y z + 20219 x y z 9 3 2 10 2 2 11 2 12 2 12 + 8882 x y z + 2390 x y z + 324 x y z + 14 x z + 28 x y z 2 11 3 10 4 9 5 8 6 7 + 324 x y z + 1588 x y z + 4429 x y z + 8101 x y z + 10666 x y z 7 6 8 5 9 4 10 3 11 2 + 10666 x y z + 8101 x y z + 4429 x y z + 1588 x y z + 324 x y z 12 2 12 3 11 4 10 5 9 6 8 + 28 x y z + 14 x y + 108 x y + 393 x y + 881 x y + 1375 x y 7 7 8 6 9 5 10 4 11 3 + 1586 x y + 1375 x y + 881 x y + 393 x y + 108 x y 12 2 2 12 12 2 12 3 11 2 11 + 14 x y >= 14 y z + 28 x y z + 14 x z + 108 y z + 324 x y z 2 11 3 11 4 10 3 10 2 2 10 + 324 x y z + 108 x z + 393 y z + 1524 x y z + 2262 x y z 3 10 4 10 5 9 4 9 2 3 9 + 1524 x y z + 393 x z + 881 y z + 4237 x y z + 8306 x y z 3 2 9 4 9 5 9 6 8 5 8 + 8306 x y z + 4237 x y z + 881 x z + 1375 y z + 8037 x y z 2 4 8 3 3 8 4 2 8 5 8 6 8 + 19515 x y z + 25706 x y z + 19515 x y z + 8037 x y z + 1375 x z 7 7 6 7 2 5 7 3 4 7 + 1586 y z + 10986 x y z + 31902 x y z + 51878 x y z 4 3 7 5 2 7 6 7 7 7 8 6 + 51878 x y z + 31902 x y z + 10986 x y z + 1586 x z + 1375 y z 7 6 2 6 6 3 5 6 4 4 6 + 10986 x y z + 37482 x y z + 72718 x y z + 89694 x y z 5 3 6 6 2 6 7 6 8 6 9 5 + 72718 x y z + 37482 x y z + 10986 x y z + 1375 x z + 881 y z 8 5 2 7 5 3 6 5 4 5 5 + 8037 x y z + 31902 x y z + 72718 x y z + 106974 x y z 5 4 5 6 3 5 7 2 5 8 5 9 5 + 106974 x y z + 72718 x y z + 31902 x y z + 8037 x y z + 881 x z 10 4 9 4 2 8 4 3 7 4 4 6 4 + 393 y z + 4237 x y z + 19515 x y z + 51878 x y z + 89694 x y z 5 5 4 6 4 4 7 3 4 8 2 4 + 106974 x y z + 89694 x y z + 51878 x y z + 19515 x y z 9 4 10 4 11 3 10 3 2 9 3 + 4237 x y z + 393 x z + 108 y z + 1524 x y z + 8306 x y z 3 8 3 4 7 3 5 6 3 6 5 3 + 25706 x y z + 51878 x y z + 72718 x y z + 72718 x y z 7 4 3 8 3 3 9 2 3 10 3 11 3 + 51878 x y z + 25706 x y z + 8306 x y z + 1524 x y z + 108 x z 12 2 11 2 2 10 2 3 9 2 4 8 2 + 14 y z + 324 x y z + 2262 x y z + 8306 x y z + 19515 x y z 5 7 2 6 6 2 7 5 2 8 4 2 + 31902 x y z + 37482 x y z + 31902 x y z + 19515 x y z 9 3 2 10 2 2 11 2 12 2 12 + 8306 x y z + 2262 x y z + 324 x y z + 14 x z + 28 x y z 2 11 3 10 4 9 5 8 6 7 + 324 x y z + 1524 x y z + 4237 x y z + 8037 x y z + 10986 x y z 7 6 8 5 9 4 10 3 11 2 + 10986 x y z + 8037 x y z + 4237 x y z + 1524 x y z + 324 x y z 12 2 12 3 11 4 10 5 9 6 8 + 28 x y z + 14 x y + 108 x y + 393 x y + 881 x y + 1375 x y 7 7 8 6 9 5 10 4 11 3 12 2 + 1586 x y + 1375 x y + 881 x y + 393 x y + 108 x y + 14 x y Expanding and collecting terms of the same sign gives: 3 10 2 2 10 3 10 4 9 2 3 9 64 x y z + 128 x y z + 64 x y z + 192 x y z + 576 x y z 3 2 9 4 9 5 8 2 4 8 3 3 8 + 576 x y z + 192 x y z + 64 x y z + 704 x y z + 1280 x y z 4 2 8 5 8 3 4 7 4 3 7 8 5 + 704 x y z + 64 x y z + 640 x y z + 640 x y z + 64 x y z 8 5 9 4 2 8 4 3 7 4 7 3 4 + 64 x y z + 192 x y z + 704 x y z + 640 x y z + 640 x y z 8 2 4 9 4 10 3 2 9 3 3 8 3 + 704 x y z + 192 x y z + 64 x y z + 576 x y z + 1280 x y z 4 7 3 7 4 3 8 3 3 9 2 3 10 3 + 640 x y z + 640 x y z + 1280 x y z + 576 x y z + 64 x y z 2 10 2 3 9 2 4 8 2 8 4 2 9 3 2 + 128 x y z + 576 x y z + 704 x y z + 704 x y z + 576 x y z 10 2 2 3 10 4 9 5 8 8 5 + 128 x y z + 64 x y z + 192 x y z + 64 x y z + 64 x y z 9 4 10 3 6 7 2 5 7 5 2 7 + 192 x y z + 64 x y z >= 320 x y z + 320 x y z + 320 x y z 6 7 7 6 2 6 6 3 5 6 4 4 6 + 320 x y z + 320 x y z + 1152 x y z + 1024 x y z + 384 x y z 5 3 6 6 2 6 7 6 2 7 5 3 6 5 + 1024 x y z + 1152 x y z + 320 x y z + 320 x y z + 1024 x y z 4 5 5 5 4 5 6 3 5 7 2 5 4 6 4 + 1024 x y z + 1024 x y z + 1024 x y z + 320 x y z + 384 x y z 5 5 4 6 4 4 5 6 3 6 5 3 5 7 2 + 1024 x y z + 384 x y z + 1024 x y z + 1024 x y z + 320 x y z 6 6 2 7 5 2 6 7 7 6 + 1152 x y z + 320 x y z + 320 x y z + 320 x y z Dividing both sides by 64 x y z gives: 2 9 9 2 9 3 8 2 8 2 8 3 8 4 7 y z + 2 x y z + x z + 3 y z + 9 x y z + 9 x y z + 3 x z + y z 3 7 2 2 7 3 7 4 7 2 3 6 3 2 6 + 11 x y z + 20 x y z + 11 x y z + x z + 10 x y z + 10 x y z 7 4 7 4 8 3 7 3 2 6 3 6 2 3 + y z + x z + 3 y z + 11 x y z + 10 x y z + 10 x y z 7 3 8 3 9 2 8 2 2 7 2 3 6 2 + 11 x y z + 3 x z + y z + 9 x y z + 20 x y z + 10 x y z 6 3 2 7 2 2 8 2 9 2 9 2 8 + 10 x y z + 20 x y z + 9 x y z + x z + 2 x y z + 9 x y z 3 7 7 3 8 2 9 2 9 3 8 4 7 + 11 x y z + 11 x y z + 9 x y z + 2 x y z + x y + 3 x y + x y 7 4 8 3 9 2 5 6 4 6 4 6 5 6 + x y + 3 x y + x y >= 5 y z + 5 x y z + 5 x y z + 5 x z 6 5 5 5 2 4 5 3 3 5 4 2 5 5 5 + 5 y z + 18 x y z + 16 x y z + 6 x y z + 16 x y z + 18 x y z 6 5 6 4 2 5 4 3 4 4 4 3 4 5 2 4 + 5 x z + 5 x y z + 16 x y z + 16 x y z + 16 x y z + 16 x y z 6 4 3 5 3 4 4 3 5 3 3 4 5 2 + 5 x y z + 6 x y z + 16 x y z + 6 x y z + 16 x y z 5 4 2 4 6 5 5 6 4 5 6 6 5 + 16 x y z + 5 x y z + 18 x y z + 5 x y z + 5 x y + 5 x y Expressing in terms of symmetric polynomials gives: {9, 2, 0} + {9, 1, 1} + 3 {8, 3, 0} + 9 {8, 2, 1} + {7, 4, 0} + 11 {7, 3, 1} + 10 {7, 2, 2} + 10 {6, 3, 2} >= 5 {6, 5, 0} + 5 {6, 4, 1} + 9 {5, 5, 1} + 16 {5, 4, 2} + 3 {5, 3, 3} + 8 {4, 4, 3} This follows from the following majorizations: left side: [10 {6, 3, 2}, 10 {7, 2, 2}, 11 {7, 3, 1}, {7, 4, 0}, 9 {8, 2, 1}, 3 {8, 3, 0}, {9, 1, 1}, {9, 2, 0}] right side: [8 {4, 4, 3}, 3 {5, 3, 3}, 16 {5, 4, 2}, 9 {5, 5, 1}, 5 {6, 4, 1}, 5 {6, 5, 0}] (d24) notsure (c25) trineq(csum(cos(A)*cos(B))<=r/R+(r/R)^2); 2 r r To prove: -- + - >= cos(B) cos(C) + cos(A) cos(C) + cos(A) cos(B) 2 R R Removing the trigonometric expressions gives: 2 r + R r 5 4 3 3 3 -------- >= - ((b + a) c - a b c + (- 2 b - 2 a ) c 2 R 5 4 4 5 5 3 3 5 2 2 2 + (b - a b - a b + a ) c + a b - 2 a b + a b)/(4 a b c ) 2 2 2 2 Multiplying both sides by 4 R a b c gives: 2 2 2 2 2 2 2 2 5 2 5 2 4 2 3 3 4 a b c r + 4 R a b c r >= - R b c - R a c + R a b c + 2 R b c 2 3 3 2 5 2 4 2 4 2 5 2 5 + 2 R a c - R b c + R a b c + R a b c - R a c - R a b 2 3 3 2 5 + 2 R a b - R a b Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 5 2 5 2 5 2 5 4 a b c r + 4 R a b c r + R b c + R a c + R b c + R a c 2 5 2 5 2 4 2 3 3 2 3 3 2 4 + R a b + R a b >= R a b c + 2 R b c + 2 R a c + R a b c 2 4 2 3 3 + R a b c + 2 R a b Let r = K/s . Let R = a*b*c/(4*K) . We get: 2 3 3 2 7 2 7 7 2 3 3 7 7 3 2 2 (((a b + a b ) c + (a b + a b ) c + (a b + a b ) c ) s 2 3 3 3 4 2 2 2 2 2 + 16 K a b c s + 64 K a b c )/(16 K s ) >= 3 3 6 2 5 5 2 5 3 6 6 3 3 5 5 2 a b c + (2 a b + 2 a b ) c + (a b + a b ) c + 2 a b c ------------------------------------------------------------------- 2 16 K 2 2 Multiplying both sides by 16 K s gives: 2 3 7 2 3 2 7 2 2 7 3 2 7 2 3 2 3 7 2 2 a b c s + a b c s + a b c s + a b c s + a b c s 7 3 2 2 2 3 3 3 4 2 2 2 + a b c s + 16 K a b c s + 64 K a b c >= 3 3 6 2 2 5 5 2 5 2 5 2 3 6 3 2 6 3 3 2 a b c s + 2 a b c s + 2 a b c s + a b c s + a b c s 5 5 2 2 + 2 a b c s Replacing K^2 by F^2 gives: 2 3 3 2 7 2 7 7 2 3 3 7 7 3 2 2 ((a b + a b ) c + (a b + a b ) c + (a b + a b ) c ) s 2 3 3 3 4 2 2 2 + 16 F a b c s + 64 F a b c >= 3 3 6 2 5 5 2 5 3 6 6 3 3 5 5 2 2 (a b c + (2 a b + 2 a b ) c + (a b + a b ) c + 2 a b c ) s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 10 2 3 3 2 9 2 4 3 3 4 2 8 (a b c + (a b + a b ) c + (- 2 a b + 2 a b - 2 a b ) c 2 5 3 4 4 3 5 2 7 2 6 3 5 4 4 5 3 + (a b + a b + a b + a b ) c + (6 a b + 4 a b + 4 a b + 4 a b 6 2 6 2 7 3 6 4 5 5 4 6 3 7 2 5 + 6 a b ) c + (a b + 4 a b + 4 a b + 4 a b + 4 a b + a b ) c 2 8 3 7 4 6 5 5 6 4 7 3 8 2 4 + (- 2 a b + a b + 4 a b + 4 a b + 4 a b + a b - 2 a b ) c 2 9 3 8 4 7 5 6 6 5 7 4 8 3 9 2 3 + (a b + 2 a b + a b + 4 a b + 4 a b + a b + 2 a b + a b ) c 2 10 3 9 4 8 5 7 6 6 7 5 8 4 9 3 + (a b + a b - 2 a b + a b + 6 a b + a b - 2 a b + a b 10 2 2 3 3 8 2 5 3 4 4 3 5 2 7 + a b ) c )/4 >= (a b c + (2 a b + 2 a b + 2 a b + 2 a b ) c 2 6 3 5 4 4 5 3 6 2 6 + (4 a b + 5 a b + 2 a b + 5 a b + 4 a b ) c 2 7 3 6 4 5 5 4 6 3 7 2 5 + (2 a b + 5 a b + 2 a b + 2 a b + 5 a b + 2 a b ) c 3 7 4 6 5 5 6 4 7 3 4 + (2 a b + 2 a b + 2 a b + 2 a b + 2 a b ) c 3 8 4 7 5 6 6 5 7 4 8 3 3 + (a b + 2 a b + 5 a b + 5 a b + 2 a b + a b ) c 5 7 6 6 7 5 2 + (2 a b + 4 a b + 2 a b ) c )/4 Multiplying both sides by 4 gives: 2 2 10 2 3 9 3 2 9 2 4 8 3 3 8 4 2 8 a b c + a b c + a b c - 2 a b c + 2 a b c - 2 a b c 2 5 7 3 4 7 4 3 7 5 2 7 2 6 6 3 5 6 + a b c + a b c + a b c + a b c + 6 a b c + 4 a b c 4 4 6 5 3 6 6 2 6 2 7 5 3 6 5 4 5 5 + 4 a b c + 4 a b c + 6 a b c + a b c + 4 a b c + 4 a b c 5 4 5 6 3 5 7 2 5 2 8 4 3 7 4 4 6 4 + 4 a b c + 4 a b c + a b c - 2 a b c + a b c + 4 a b c 5 5 4 6 4 4 7 3 4 8 2 4 2 9 3 3 8 3 + 4 a b c + 4 a b c + a b c - 2 a b c + a b c + 2 a b c 4 7 3 5 6 3 6 5 3 7 4 3 8 3 3 9 2 3 + a b c + 4 a b c + 4 a b c + a b c + 2 a b c + a b c 2 10 2 3 9 2 4 8 2 5 7 2 6 6 2 7 5 2 + a b c + a b c - 2 a b c + a b c + 6 a b c + a b c 8 4 2 9 3 2 10 2 2 - 2 a b c + a b c + a b c >= 3 3 8 2 5 7 3 4 7 4 3 7 5 2 7 2 6 6 a b c + 2 a b c + 2 a b c + 2 a b c + 2 a b c + 4 a b c 3 5 6 4 4 6 5 3 6 6 2 6 2 7 5 3 6 5 + 5 a b c + 2 a b c + 5 a b c + 4 a b c + 2 a b c + 5 a b c 4 5 5 5 4 5 6 3 5 7 2 5 3 7 4 4 6 4 + 2 a b c + 2 a b c + 5 a b c + 2 a b c + 2 a b c + 2 a b c 5 5 4 6 4 4 7 3 4 3 8 3 4 7 3 5 6 3 + 2 a b c + 2 a b c + 2 a b c + a b c + 2 a b c + 5 a b c 6 5 3 7 4 3 8 3 3 5 7 2 6 6 2 7 5 2 + 5 a b c + 2 a b c + a b c + 2 a b c + 4 a b c + 2 a b c Expanding and collecting terms of the same sign gives: 2 2 10 2 3 9 3 2 9 3 3 8 2 6 6 4 4 6 a b c + a b c + a b c + a b c + 2 a b c + 2 a b c 6 2 6 4 5 5 5 4 5 4 6 4 5 5 4 6 4 4 + 2 a b c + 2 a b c + 2 a b c + 2 a b c + 2 a b c + 2 a b c 2 9 3 3 8 3 8 3 3 9 2 3 2 10 2 3 9 2 + a b c + a b c + a b c + a b c + a b c + a b c 6 6 2 9 3 2 10 2 2 + 2 a b c + a b c + a b c >= 2 4 8 4 2 8 2 5 7 3 4 7 4 3 7 5 2 7 3 5 6 2 a b c + 2 a b c + a b c + a b c + a b c + a b c + a b c 5 3 6 2 7 5 3 6 5 6 3 5 7 2 5 2 8 4 3 7 4 + a b c + a b c + a b c + a b c + a b c + 2 a b c + a b c 7 3 4 8 2 4 4 7 3 5 6 3 6 5 3 7 4 3 + a b c + 2 a b c + a b c + a b c + a b c + a b c 4 8 2 5 7 2 7 5 2 8 4 2 + 2 a b c + a b c + a b c + 2 a b c Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 12 3 2 2 3 11 ((6 y + 12 x y + 6 x ) z + (40 y + 120 x y + 120 x y + 40 x ) z 4 3 2 2 3 4 10 + (143 y + 508 x y + 730 x y + 508 x y + 143 x ) z 5 4 2 3 3 2 4 5 9 + (347 y + 1363 x y + 2354 x y + 2354 x y + 1363 x y + 347 x ) z 6 5 2 4 3 3 4 2 5 + (593 y + 2623 x y + 5161 x y + 6262 x y + 5161 x y + 2623 x y 6 8 7 6 2 5 3 4 4 3 + 593 x ) z + (710 y + 3662 x y + 8338 x y + 11674 x y + 11674 x y 5 2 6 7 7 8 7 2 6 + 8338 x y + 3662 x y + 710 x ) z + (593 y + 3662 x y + 9830 x y 3 5 4 4 5 3 6 2 7 8 + 16058 x y + 18594 x y + 16058 x y + 9830 x y + 3662 x y + 593 x ) 6 9 8 2 7 3 6 4 5 z + (347 y + 2623 x y + 8338 x y + 16058 x y + 21722 x y 5 4 6 3 7 2 8 9 5 + 21722 x y + 16058 x y + 8338 x y + 2623 x y + 347 x ) z 10 9 2 8 3 7 4 6 5 5 + (143 y + 1363 x y + 5161 x y + 11674 x y + 18594 x y + 21722 x y 6 4 7 3 8 2 9 10 4 + 18594 x y + 11674 x y + 5161 x y + 1363 x y + 143 x ) z 11 10 2 9 3 8 4 7 5 6 + (40 y + 508 x y + 2354 x y + 6262 x y + 11674 x y + 16058 x y 6 5 7 4 8 3 9 2 10 11 3 + 16058 x y + 11674 x y + 6262 x y + 2354 x y + 508 x y + 40 x ) z 12 11 2 10 3 9 4 8 5 7 + (6 y + 120 x y + 730 x y + 2354 x y + 5161 x y + 8338 x y 6 6 7 5 8 4 9 3 10 2 11 + 9830 x y + 8338 x y + 5161 x y + 2354 x y + 730 x y + 120 x y 12 2 12 2 11 3 10 4 9 5 8 + 6 x ) z + (12 x y + 120 x y + 508 x y + 1363 x y + 2623 x y 6 7 7 6 8 5 9 4 10 3 11 2 + 3662 x y + 3662 x y + 2623 x y + 1363 x y + 508 x y + 120 x y 12 2 12 3 11 4 10 5 9 6 8 + 12 x y) z + 6 x y + 40 x y + 143 x y + 347 x y + 593 x y 7 7 8 6 9 5 10 4 11 3 12 2 + 710 x y + 593 x y + 347 x y + 143 x y + 40 x y + 6 x y ) 2 2 12 3 2 2 3 /16384 >= ((6 y + 12 x y + 6 x ) z + (40 y + 120 x y + 120 x y + 40 x ) 11 4 3 2 2 3 4 10 z + (127 y + 508 x y + 762 x y + 508 x y + 127 x ) z 5 4 2 3 3 2 4 5 9 + (251 y + 1267 x y + 2546 x y + 2546 x y + 1267 x y + 251 x ) z 6 5 2 4 3 3 4 2 5 + (353 y + 2143 x y + 5337 x y + 7094 x y + 5337 x y + 2143 x y 6 8 7 6 2 5 3 4 4 3 + 353 x ) z + (390 y + 2702 x y + 7826 x y + 12698 x y + 12698 x y 5 2 6 7 7 8 7 2 6 + 7826 x y + 2702 x y + 390 x ) z + (353 y + 2702 x y + 8774 x y 3 5 4 4 5 3 6 2 7 8 + 16314 x y + 19778 x y + 16314 x y + 8774 x y + 2702 x y + 353 x ) 6 9 8 2 7 3 6 4 5 z + (251 y + 2143 x y + 7826 x y + 16314 x y + 22554 x y 5 4 6 3 7 2 8 9 5 + 22554 x y + 16314 x y + 7826 x y + 2143 x y + 251 x ) z 10 9 2 8 3 7 4 6 5 5 + (127 y + 1267 x y + 5337 x y + 12698 x y + 19778 x y + 22554 x y 6 4 7 3 8 2 9 10 4 + 19778 x y + 12698 x y + 5337 x y + 1267 x y + 127 x ) z 11 10 2 9 3 8 4 7 5 6 + (40 y + 508 x y + 2546 x y + 7094 x y + 12698 x y + 16314 x y 6 5 7 4 8 3 9 2 10 11 3 + 16314 x y + 12698 x y + 7094 x y + 2546 x y + 508 x y + 40 x ) z 12 11 2 10 3 9 4 8 5 7 + (6 y + 120 x y + 762 x y + 2546 x y + 5337 x y + 7826 x y 6 6 7 5 8 4 9 3 10 2 11 + 8774 x y + 7826 x y + 5337 x y + 2546 x y + 762 x y + 120 x y 12 2 12 2 11 3 10 4 9 5 8 + 6 x ) z + (12 x y + 120 x y + 508 x y + 1267 x y + 2143 x y 6 7 7 6 8 5 9 4 10 3 11 2 + 2702 x y + 2702 x y + 2143 x y + 1267 x y + 508 x y + 120 x y 12 2 12 3 11 4 10 5 9 6 8 + 12 x y) z + 6 x y + 40 x y + 127 x y + 251 x y + 353 x y 7 7 8 6 9 5 10 4 11 3 12 2 + 390 x y + 353 x y + 251 x y + 127 x y + 40 x y + 6 x y )/16384 Multiplying both sides by 16384 gives: 2 12 12 2 12 3 11 2 11 2 11 6 y z + 12 x y z + 6 x z + 40 y z + 120 x y z + 120 x y z 3 11 4 10 3 10 2 2 10 3 10 + 40 x z + 143 y z + 508 x y z + 730 x y z + 508 x y z 4 10 5 9 4 9 2 3 9 3 2 9 + 143 x z + 347 y z + 1363 x y z + 2354 x y z + 2354 x y z 4 9 5 9 6 8 5 8 2 4 8 + 1363 x y z + 347 x z + 593 y z + 2623 x y z + 5161 x y z 3 3 8 4 2 8 5 8 6 8 7 7 + 6262 x y z + 5161 x y z + 2623 x y z + 593 x z + 710 y z 6 7 2 5 7 3 4 7 4 3 7 + 3662 x y z + 8338 x y z + 11674 x y z + 11674 x y z 5 2 7 6 7 7 7 8 6 7 6 + 8338 x y z + 3662 x y z + 710 x z + 593 y z + 3662 x y z 2 6 6 3 5 6 4 4 6 5 3 6 + 9830 x y z + 16058 x y z + 18594 x y z + 16058 x y z 6 2 6 7 6 8 6 9 5 8 5 + 9830 x y z + 3662 x y z + 593 x z + 347 y z + 2623 x y z 2 7 5 3 6 5 4 5 5 5 4 5 + 8338 x y z + 16058 x y z + 21722 x y z + 21722 x y z 6 3 5 7 2 5 8 5 9 5 10 4 + 16058 x y z + 8338 x y z + 2623 x y z + 347 x z + 143 y z 9 4 2 8 4 3 7 4 4 6 4 + 1363 x y z + 5161 x y z + 11674 x y z + 18594 x y z 5 5 4 6 4 4 7 3 4 8 2 4 + 21722 x y z + 18594 x y z + 11674 x y z + 5161 x y z 9 4 10 4 11 3 10 3 2 9 3 + 1363 x y z + 143 x z + 40 y z + 508 x y z + 2354 x y z 3 8 3 4 7 3 5 6 3 6 5 3 + 6262 x y z + 11674 x y z + 16058 x y z + 16058 x y z 7 4 3 8 3 3 9 2 3 10 3 11 3 + 11674 x y z + 6262 x y z + 2354 x y z + 508 x y z + 40 x z 12 2 11 2 2 10 2 3 9 2 4 8 2 + 6 y z + 120 x y z + 730 x y z + 2354 x y z + 5161 x y z 5 7 2 6 6 2 7 5 2 8 4 2 + 8338 x y z + 9830 x y z + 8338 x y z + 5161 x y z 9 3 2 10 2 2 11 2 12 2 12 + 2354 x y z + 730 x y z + 120 x y z + 6 x z + 12 x y z 2 11 3 10 4 9 5 8 6 7 + 120 x y z + 508 x y z + 1363 x y z + 2623 x y z + 3662 x y z 7 6 8 5 9 4 10 3 11 2 + 3662 x y z + 2623 x y z + 1363 x y z + 508 x y z + 120 x y z 12 2 12 3 11 4 10 5 9 6 8 + 12 x y z + 6 x y + 40 x y + 143 x y + 347 x y + 593 x y 7 7 8 6 9 5 10 4 11 3 12 2 + 710 x y + 593 x y + 347 x y + 143 x y + 40 x y + 6 x y >= 2 12 12 2 12 3 11 2 11 2 11 6 y z + 12 x y z + 6 x z + 40 y z + 120 x y z + 120 x y z 3 11 4 10 3 10 2 2 10 3 10 + 40 x z + 127 y z + 508 x y z + 762 x y z + 508 x y z 4 10 5 9 4 9 2 3 9 3 2 9 + 127 x z + 251 y z + 1267 x y z + 2546 x y z + 2546 x y z 4 9 5 9 6 8 5 8 2 4 8 + 1267 x y z + 251 x z + 353 y z + 2143 x y z + 5337 x y z 3 3 8 4 2 8 5 8 6 8 7 7 + 7094 x y z + 5337 x y z + 2143 x y z + 353 x z + 390 y z 6 7 2 5 7 3 4 7 4 3 7 + 2702 x y z + 7826 x y z + 12698 x y z + 12698 x y z 5 2 7 6 7 7 7 8 6 7 6 + 7826 x y z + 2702 x y z + 390 x z + 353 y z + 2702 x y z 2 6 6 3 5 6 4 4 6 5 3 6 + 8774 x y z + 16314 x y z + 19778 x y z + 16314 x y z 6 2 6 7 6 8 6 9 5 8 5 + 8774 x y z + 2702 x y z + 353 x z + 251 y z + 2143 x y z 2 7 5 3 6 5 4 5 5 5 4 5 + 7826 x y z + 16314 x y z + 22554 x y z + 22554 x y z 6 3 5 7 2 5 8 5 9 5 10 4 + 16314 x y z + 7826 x y z + 2143 x y z + 251 x z + 127 y z 9 4 2 8 4 3 7 4 4 6 4 + 1267 x y z + 5337 x y z + 12698 x y z + 19778 x y z 5 5 4 6 4 4 7 3 4 8 2 4 + 22554 x y z + 19778 x y z + 12698 x y z + 5337 x y z 9 4 10 4 11 3 10 3 2 9 3 + 1267 x y z + 127 x z + 40 y z + 508 x y z + 2546 x y z 3 8 3 4 7 3 5 6 3 6 5 3 + 7094 x y z + 12698 x y z + 16314 x y z + 16314 x y z 7 4 3 8 3 3 9 2 3 10 3 11 3 + 12698 x y z + 7094 x y z + 2546 x y z + 508 x y z + 40 x z 12 2 11 2 2 10 2 3 9 2 4 8 2 + 6 y z + 120 x y z + 762 x y z + 2546 x y z + 5337 x y z 5 7 2 6 6 2 7 5 2 8 4 2 + 7826 x y z + 8774 x y z + 7826 x y z + 5337 x y z 9 3 2 10 2 2 11 2 12 2 12 + 2546 x y z + 762 x y z + 120 x y z + 6 x z + 12 x y z 2 11 3 10 4 9 5 8 6 7 + 120 x y z + 508 x y z + 1267 x y z + 2143 x y z + 2702 x y z 7 6 8 5 9 4 10 3 11 2 + 2702 x y z + 2143 x y z + 1267 x y z + 508 x y z + 120 x y z 12 2 12 3 11 4 10 5 9 6 8 + 12 x y z + 6 x y + 40 x y + 127 x y + 251 x y + 353 x y 7 7 8 6 9 5 10 4 11 3 12 2 + 390 x y + 353 x y + 251 x y + 127 x y + 40 x y + 6 x y Expanding and collecting terms of the same sign gives: 4 10 4 10 5 9 4 9 4 9 5 9 16 y z + 16 x z + 96 y z + 96 x y z + 96 x y z + 96 x z 6 8 5 8 5 8 6 8 7 7 6 7 + 240 y z + 480 x y z + 480 x y z + 240 x z + 320 y z + 960 x y z 2 5 7 5 2 7 6 7 7 7 8 6 + 512 x y z + 512 x y z + 960 x y z + 320 x z + 240 y z 7 6 2 6 6 6 2 6 7 6 8 6 + 960 x y z + 1056 x y z + 1056 x y z + 960 x y z + 240 x z 9 5 8 5 2 7 5 7 2 5 8 5 + 96 y z + 480 x y z + 512 x y z + 512 x y z + 480 x y z 9 5 10 4 9 4 9 4 10 4 5 7 2 + 96 x z + 16 y z + 96 x y z + 96 x y z + 16 x z + 512 x y z 6 6 2 7 5 2 4 9 5 8 6 7 + 1056 x y z + 512 x y z + 96 x y z + 480 x y z + 960 x y z 7 6 8 5 9 4 4 10 5 9 6 8 + 960 x y z + 480 x y z + 96 x y z + 16 x y + 96 x y + 240 x y 7 7 8 6 9 5 10 4 + 320 x y + 240 x y + 96 x y + 16 x y >= 2 2 10 2 3 9 3 2 9 2 4 8 3 3 8 32 x y z + 192 x y z + 192 x y z + 176 x y z + 832 x y z 4 2 8 3 4 7 4 3 7 3 5 6 4 4 6 + 176 x y z + 1024 x y z + 1024 x y z + 256 x y z + 1184 x y z 5 3 6 3 6 5 4 5 5 5 4 5 6 3 5 + 256 x y z + 256 x y z + 832 x y z + 832 x y z + 256 x y z 2 8 4 3 7 4 4 6 4 5 5 4 6 4 4 + 176 x y z + 1024 x y z + 1184 x y z + 832 x y z + 1184 x y z 7 3 4 8 2 4 2 9 3 3 8 3 4 7 3 + 1024 x y z + 176 x y z + 192 x y z + 832 x y z + 1024 x y z 5 6 3 6 5 3 7 4 3 8 3 3 9 2 3 + 256 x y z + 256 x y z + 1024 x y z + 832 x y z + 192 x y z 2 10 2 3 9 2 4 8 2 8 4 2 9 3 2 + 32 x y z + 192 x y z + 176 x y z + 176 x y z + 192 x y z 10 2 2 + 32 x y z Dividing both sides by 16 gives: 4 10 4 10 5 9 4 9 4 9 5 9 6 8 y z + x z + 6 y z + 6 x y z + 6 x y z + 6 x z + 15 y z 5 8 5 8 6 8 7 7 6 7 2 5 7 + 30 x y z + 30 x y z + 15 x z + 20 y z + 60 x y z + 32 x y z 5 2 7 6 7 7 7 8 6 7 6 2 6 6 + 32 x y z + 60 x y z + 20 x z + 15 y z + 60 x y z + 66 x y z 6 2 6 7 6 8 6 9 5 8 5 2 7 5 + 66 x y z + 60 x y z + 15 x z + 6 y z + 30 x y z + 32 x y z 7 2 5 8 5 9 5 10 4 9 4 9 4 10 4 + 32 x y z + 30 x y z + 6 x z + y z + 6 x y z + 6 x y z + x z 5 7 2 6 6 2 7 5 2 4 9 5 8 + 32 x y z + 66 x y z + 32 x y z + 6 x y z + 30 x y z 6 7 7 6 8 5 9 4 4 10 5 9 + 60 x y z + 60 x y z + 30 x y z + 6 x y z + x y + 6 x y 6 8 7 7 8 6 9 5 10 4 + 15 x y + 20 x y + 15 x y + 6 x y + x y >= 2 2 10 2 3 9 3 2 9 2 4 8 3 3 8 2 x y z + 12 x y z + 12 x y z + 11 x y z + 52 x y z 4 2 8 3 4 7 4 3 7 3 5 6 4 4 6 + 11 x y z + 64 x y z + 64 x y z + 16 x y z + 74 x y z 5 3 6 3 6 5 4 5 5 5 4 5 6 3 5 + 16 x y z + 16 x y z + 52 x y z + 52 x y z + 16 x y z 2 8 4 3 7 4 4 6 4 5 5 4 6 4 4 + 11 x y z + 64 x y z + 74 x y z + 52 x y z + 74 x y z 7 3 4 8 2 4 2 9 3 3 8 3 4 7 3 + 64 x y z + 11 x y z + 12 x y z + 52 x y z + 64 x y z 5 6 3 6 5 3 7 4 3 8 3 3 9 2 3 + 16 x y z + 16 x y z + 64 x y z + 52 x y z + 12 x y z 2 10 2 3 9 2 4 8 2 8 4 2 9 3 2 + 2 x y z + 12 x y z + 11 x y z + 11 x y z + 12 x y z 10 2 2 + 2 x y z Expressing in terms of symmetric polynomials gives: {10, 4, 0} + 6 {9, 5, 0} + 6 {9, 4, 1} + 15 {8, 6, 0} + 30 {8, 5, 1} + 10 {7, 7, 0} + 60 {7, 6, 1} + 32 {7, 5, 2} + 33 {6, 6, 2} >= {10, 2, 2} + 12 {9, 3, 2} + 11 {8, 4, 2} + 26 {8, 3, 3} + 64 {7, 4, 3} + 16 {6, 5, 3} + 37 {6, 4, 4} + 26 {5, 5, 4} This follows from the following majorizations: {10, 4, 0} >= {10, 2, 2} left side: [33 {6, 6, 2}, 32 {7, 5, 2}, 60 {7, 6, 1}, 10 {7, 7, 0}, 30 {8, 5, 1}, 15 {8, 6, 0}, 6 {9, 4, 1}, 6 {9, 5, 0}, {10, 4, 0}] right side: [26 {5, 5, 4}, 37 {6, 4, 4}, 16 {6, 5, 3}, 64 {7, 4, 3}, 26 {8, 3, 3}, 11 {8, 4, 2}, 12 {9, 3, 2}, {10, 2, 2}] (d25) notsure (c26) /* 3.13 */ trineq(csum(a*sin(A))>=2*K*sqrt(3)/R); 2 sqrt(3) K To prove: sin(C) c + sin(B) b + sin(A) a >= ----------- R Removing the trigonometric expressions gives: 2 2 2 2 K c + 2 K b + 2 K a 2 sqrt(3) K ------------------------ >= ----------- a b c R Multiplying both sides by R a b c gives: 2 2 2 2 K R c + 2 K R b + 2 K R a >= 2 sqrt(3) K a b c Dividing both sides by 2 K gives: 2 2 2 R c + R b + R a >= sqrt(3) a b c Let R = a*b*c/(4*K) . We get: 3 3 3 a b c + (a b + a b) c ------------------------ >= sqrt(3) a b c 4 K Multiplying both sides by 4 K gives: 3 3 3 a b c + a b c + a b c >= 4 sqrt(3) K a b c Since 4 sqrt(3) a b c is positive, and since 3 3 3 a b c + (a b + a b) c is positive, we can square both sides to get: 2 2 6 2 4 4 2 4 2 6 4 4 6 2 2 a b c + (2 a b + 2 a b ) c + (a b + 2 a b + a b ) c >= 2 2 2 4 2 3 3 2 2 2 2 3 3 48 a b c s + ((- 48 a b - 48 a b ) c - 48 a b c ) s 2 3 3 2 3 3 3 2 2 3 3 3 + ((48 a b + 48 a b ) c + 48 a b c ) s - 48 a b c s Expanding and collecting terms of the same sign gives: 2 2 3 3 2 3 2 3 3 2 2 3 3 3 3 2 2 6 48 a b c s + 48 a b c s + 48 a b c s + 48 a b c s + a b c 2 4 4 4 2 4 2 6 2 4 4 2 6 2 2 + 2 a b c + 2 a b c + a b c + 2 a b c + a b c >= 2 2 2 4 2 3 3 2 3 2 3 2 3 3 2 2 48 a b c s + 48 a b c s + 48 a b c s + 48 a b c s 2 2 2 Dividing both sides by a b c gives: 3 3 3 4 2 2 2 2 4 48 c s + 48 b s + 48 a s + 48 a b c s + c + 2 b c + 2 a c + b 2 2 4 4 2 2 2 + 2 a b + a >= 48 s + 48 b c s + 48 a c s + 48 a b s Let s = (c+b+a)/2 . We get: 4 3 2 2 2 7 c + (24 b + 24 a) c + (38 b + 96 a b + 38 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 7 b + 24 a b + 38 a b + 24 a b 4 4 3 2 2 2 + 7 a >= 3 c + (24 b + 24 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 3 b + 24 a b + 42 a b + 24 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 4 c + 4 b + 4 a >= 4 b c + 4 a c + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/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 )/4 Multiplying both sides by 4 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d26) true (c27) /* 3.14 */ trineq(9*r<=csum(a*sin(A))); To prove: sin(C) c + sin(B) b + sin(A) a >= 9 r Removing the trigonometric expressions gives: 2 2 2 2 K c + 2 K b + 2 K a ------------------------ >= 9 r a b c Multiplying both sides by a b c gives: 2 2 2 2 K c + 2 K b + 2 K a >= 9 a b c r Let r = K/s . We get: 2 2 2 9 K a b c 2 K c + 2 K b + 2 K a >= --------- s Multiplying both sides by s gives: 2 2 2 2 K c s + 2 K b s + 2 K a s >= 9 K a b c left side: [{1, 1, 1}, {2, 1, 0}] right side: [2 {3, 0, 0}] Bringing all terms involving K to the left side yields: 2 2 2 K (2 c + 2 b + 2 a ) s - 9 K a b c >= 0 2 2 2 Since (2 c + 2 b + 2 a ) s - 9 a b c is positive, and since 0 is positive, we can square both sides to get: 4 2 2 2 4 2 2 4 6 (4 c + (8 b + 8 a ) c + 4 b + 8 a b + 4 a ) s 5 4 2 2 3 + (- 4 c + (- 4 b - 4 a) c + (- 8 b - 36 a b - 8 a ) c 3 2 2 3 2 + (- 8 b - 8 a b - 8 a b - 8 a ) c 4 3 2 2 3 4 5 4 2 3 + (- 4 b - 36 a b - 8 a b - 36 a b - 4 a ) c - 4 b - 4 a b - 8 a b 3 2 4 5 5 5 4 - 8 a b - 4 a b - 4 a ) s + ((4 b + 4 a) c + 40 a b c 3 2 2 3 3 3 2 2 3 2 + (8 b + 44 a b + 44 a b + 8 a ) c + (44 a b + 81 a b + 44 a b) c 5 4 2 3 3 2 4 5 5 3 3 + (4 b + 40 a b + 44 a b + 44 a b + 40 a b + 4 a ) c + 4 a b + 8 a b 5 4 5 2 2 4 + 4 a b) s + (- 4 a b c + (- 36 a b - 36 a b) c 3 2 2 3 3 4 2 3 3 2 + (- 8 a b - 117 a b - 8 a b) c + (- 36 a b - 117 a b - 117 a b 4 2 5 2 4 3 3 4 2 5 3 - 36 a b) c + (- 4 a b - 36 a b - 8 a b - 36 a b - 4 a b) c) s 2 2 4 2 3 3 2 3 + (36 a b c + (81 a b + 81 a b ) c 2 4 3 3 4 2 2 2 3 3 3 + (36 a b + 81 a b + 36 a b ) c ) s - 81 a b c s >= 0 Expanding and collecting terms of the same sign gives: 4 6 2 2 6 2 2 6 4 6 2 2 6 4 6 5 4 4 c s + 8 b c s + 8 a c s + 4 b s + 8 a b s + 4 a s + 4 b c s 5 4 4 4 3 3 4 2 3 4 2 3 4 + 4 a c s + 40 a b c s + 8 b c s + 44 a b c s + 44 a b c s 3 3 4 3 2 4 2 2 2 4 3 2 4 5 4 + 8 a c s + 44 a b c s + 81 a b c s + 44 a b c s + 4 b c s 4 4 2 3 4 3 2 4 4 4 5 4 + 40 a b c s + 44 a b c s + 44 a b c s + 40 a b c s + 4 a c s 5 4 3 3 4 5 4 2 2 4 2 2 3 3 2 + 4 a b s + 8 a b s + 4 a b s + 36 a b c s + 81 a b c s 3 2 3 2 2 4 2 2 3 3 2 2 4 2 2 2 + 81 a b c s + 36 a b c s + 81 a b c s + 36 a b c s >= 5 5 4 5 4 5 2 3 5 3 5 2 3 5 4 c s + 4 b c s + 4 a c s + 8 b c s + 36 a b c s + 8 a c s 3 2 5 2 2 5 2 2 5 3 2 5 4 5 + 8 b c s + 8 a b c s + 8 a b c s + 8 a c s + 4 b c s 3 5 2 2 5 3 5 4 5 5 5 4 5 + 36 a b c s + 8 a b c s + 36 a b c s + 4 a c s + 4 b s + 4 a b s 2 3 5 3 2 5 4 5 5 5 5 3 2 4 3 + 8 a b s + 8 a b s + 4 a b s + 4 a s + 4 a b c s + 36 a b c s 2 4 3 3 3 3 2 2 3 3 3 3 3 + 36 a b c s + 8 a b c s + 117 a b c s + 8 a b c s 4 2 3 2 3 2 3 3 2 2 3 4 2 3 + 36 a b c s + 117 a b c s + 117 a b c s + 36 a b c s 5 3 2 4 3 3 3 3 4 2 3 5 3 + 4 a b c s + 36 a b c s + 8 a b c s + 36 a b c s + 4 a b c s 3 3 3 + 81 a b c s Dividing both sides by s gives: 4 5 2 2 5 2 2 5 4 5 2 2 5 4 5 5 3 4 c s + 8 b c s + 8 a c s + 4 b s + 8 a b s + 4 a s + 4 b c s 5 3 4 3 3 3 3 2 3 3 2 3 3 + 4 a c s + 40 a b c s + 8 b c s + 44 a b c s + 44 a b c s 3 3 3 3 2 3 2 2 2 3 3 2 3 5 3 + 8 a c s + 44 a b c s + 81 a b c s + 44 a b c s + 4 b c s 4 3 2 3 3 3 2 3 4 3 5 3 + 40 a b c s + 44 a b c s + 44 a b c s + 40 a b c s + 4 a c s 5 3 3 3 3 5 3 2 2 4 2 3 3 + 4 a b s + 8 a b s + 4 a b s + 36 a b c s + 81 a b c s 3 2 3 2 4 2 3 3 2 4 2 2 + 81 a b c s + 36 a b c s + 81 a b c s + 36 a b c s >= 5 4 4 4 4 4 2 3 4 3 4 2 3 4 4 c s + 4 b c s + 4 a c s + 8 b c s + 36 a b c s + 8 a c s 3 2 4 2 2 4 2 2 4 3 2 4 4 4 + 8 b c s + 8 a b c s + 8 a b c s + 8 a c s + 4 b c s 3 4 2 2 4 3 4 4 4 5 4 4 4 + 36 a b c s + 8 a b c s + 36 a b c s + 4 a c s + 4 b s + 4 a b s 2 3 4 3 2 4 4 4 5 4 5 2 2 4 2 + 8 a b s + 8 a b s + 4 a b s + 4 a s + 4 a b c s + 36 a b c s 2 4 2 3 3 2 2 2 3 2 3 3 2 + 36 a b c s + 8 a b c s + 117 a b c s + 8 a b c s 4 2 2 2 3 2 2 3 2 2 2 4 2 2 + 36 a b c s + 117 a b c s + 117 a b c s + 36 a b c s 5 2 2 4 2 3 3 2 4 2 2 5 2 + 4 a b c s + 36 a b c s + 8 a b c s + 36 a b c s + 4 a b c s 3 3 3 + 81 a b c Let s = (c+b+a)/2 . We get: 9 8 2 2 7 (c + (9 b + 9 a) c + (24 b + 84 a b + 24 a ) c 3 2 2 3 6 + (40 b + 240 a b + 240 a b + 40 a ) c 4 3 2 2 3 4 5 + (54 b + 396 a b + 825 a b + 396 a b + 54 a ) c 5 4 2 3 3 2 4 5 4 + (54 b + 462 a b + 1527 a b + 1527 a b + 462 a b + 54 a ) c 6 5 2 4 3 3 4 2 5 6 + (40 b + 396 a b + 1527 a b + 2394 a b + 1527 a b + 396 a b + 40 a ) 3 7 6 2 5 3 4 4 3 5 2 c + (24 b + 240 a b + 825 a b + 1527 a b + 1527 a b + 825 a b 6 7 2 8 7 2 6 3 5 4 4 + 240 a b + 24 a ) c + (9 b + 84 a b + 240 a b + 396 a b + 462 a b 5 3 6 2 7 8 9 8 2 7 + 396 a b + 240 a b + 84 a b + 9 a ) c + b + 9 a b + 24 a b 3 6 4 5 5 4 6 3 7 2 8 9 + 40 a b + 54 a b + 54 a b + 40 a b + 24 a b + 9 a b + a )/8 >= 9 8 2 2 7 (c + (5 b + 5 a) c + (12 b + 33 a b + 12 a ) c 3 2 2 3 6 + (20 b + 120 a b + 120 a b + 20 a ) c 4 3 2 2 3 4 5 + (26 b + 207 a b + 449 a b + 207 a b + 26 a ) c 5 4 2 3 3 2 4 5 4 + (26 b + 230 a b + 719 a b + 719 a b + 230 a b + 26 a ) c 6 5 2 4 3 3 4 2 5 6 + (20 b + 207 a b + 719 a b + 1332 a b + 719 a b + 207 a b + 20 a ) 3 7 6 2 5 3 4 4 3 5 2 c + (12 b + 120 a b + 449 a b + 719 a b + 719 a b + 449 a b 6 7 2 8 7 2 6 3 5 4 4 + 120 a b + 12 a ) c + (5 b + 33 a b + 120 a b + 207 a b + 230 a b 5 3 6 2 7 8 9 8 2 7 + 207 a b + 120 a b + 33 a b + 5 a ) c + b + 5 a b + 12 a b 3 6 4 5 5 4 6 3 7 2 8 9 + 20 a b + 26 a b + 26 a b + 20 a b + 12 a b + 5 a b + a )/4 Multiplying both sides by 8 gives: 9 8 8 2 7 7 2 7 3 6 2 6 c + 9 b c + 9 a c + 24 b c + 84 a b c + 24 a c + 40 b c + 240 a b c 2 6 3 6 4 5 3 5 2 2 5 3 5 + 240 a b c + 40 a c + 54 b c + 396 a b c + 825 a b c + 396 a b c 4 5 5 4 4 4 2 3 4 3 2 4 + 54 a c + 54 b c + 462 a b c + 1527 a b c + 1527 a b c 4 4 5 4 6 3 5 3 2 4 3 + 462 a b c + 54 a c + 40 b c + 396 a b c + 1527 a b c 3 3 3 4 2 3 5 3 6 3 7 2 + 2394 a b c + 1527 a b c + 396 a b c + 40 a c + 24 b c 6 2 2 5 2 3 4 2 4 3 2 5 2 2 + 240 a b c + 825 a b c + 1527 a b c + 1527 a b c + 825 a b c 6 2 7 2 8 7 2 6 3 5 + 240 a b c + 24 a c + 9 b c + 84 a b c + 240 a b c + 396 a b c 4 4 5 3 6 2 7 8 9 8 + 462 a b c + 396 a b c + 240 a b c + 84 a b c + 9 a c + b + 9 a b 2 7 3 6 4 5 5 4 6 3 7 2 8 + 24 a b + 40 a b + 54 a b + 54 a b + 40 a b + 24 a b + 9 a b 9 9 8 8 2 7 7 2 7 3 6 + a >= 2 c + 10 b c + 10 a c + 24 b c + 66 a b c + 24 a c + 40 b c 2 6 2 6 3 6 4 5 3 5 2 2 5 + 240 a b c + 240 a b c + 40 a c + 52 b c + 414 a b c + 898 a b c 3 5 4 5 5 4 4 4 2 3 4 + 414 a b c + 52 a c + 52 b c + 460 a b c + 1438 a b c 3 2 4 4 4 5 4 6 3 5 3 + 1438 a b c + 460 a b c + 52 a c + 40 b c + 414 a b c 2 4 3 3 3 3 4 2 3 5 3 6 3 + 1438 a b c + 2664 a b c + 1438 a b c + 414 a b c + 40 a c 7 2 6 2 2 5 2 3 4 2 4 3 2 + 24 b c + 240 a b c + 898 a b c + 1438 a b c + 1438 a b c 5 2 2 6 2 7 2 8 7 2 6 + 898 a b c + 240 a b c + 24 a c + 10 b c + 66 a b c + 240 a b c 3 5 4 4 5 3 6 2 7 8 + 414 a b c + 460 a b c + 414 a b c + 240 a b c + 66 a b c + 10 a c 9 8 2 7 3 6 4 5 5 4 6 3 + 2 b + 10 a b + 24 a b + 40 a b + 52 a b + 52 a b + 40 a b 7 2 8 9 + 24 a b + 10 a b + 2 a Expanding and collecting terms of the same sign gives: 7 4 5 4 5 5 4 4 4 2 3 4 3 2 4 18 a b c + 2 b c + 2 a c + 2 b c + 2 a b c + 89 a b c + 89 a b c 4 4 5 4 2 4 3 4 2 3 3 4 2 4 3 2 + 2 a b c + 2 a c + 89 a b c + 89 a b c + 89 a b c + 89 a b c 7 4 4 7 4 5 5 4 + 18 a b c + 2 a b c + 18 a b c + 2 a b + 2 a b >= 9 8 8 3 5 2 2 5 3 5 5 3 c + b c + a c + 18 a b c + 73 a b c + 18 a b c + 18 a b c 3 3 3 5 3 2 5 2 5 2 2 8 3 5 + 270 a b c + 18 a b c + 73 a b c + 73 a b c + b c + 18 a b c 5 3 8 9 8 8 9 + 18 a b c + a c + b + a b + a b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 9 8 2 2 7 (4 z + (56 y + 56 x) z + (362 y + 740 x y + 362 x ) z 3 2 2 3 6 + (1219 y + 3217 x y + 3217 x y + 1219 x ) z 4 3 2 2 3 4 5 + (2171 y + 7802 x y + 11286 x y + 7802 x y + 2171 x ) z 5 4 2 3 3 2 4 5 4 + (2171 y + 10542 x y + 20843 x y + 20843 x y + 10542 x y + 2171 x ) z 6 5 2 4 3 3 4 2 5 + (1219 y + 7802 x y + 20843 x y + 28536 x y + 20843 x y + 7802 x y 6 3 7 6 2 5 3 4 4 3 + 1219 x ) z + (362 y + 3217 x y + 11286 x y + 20843 x y + 20843 x y 5 2 6 7 2 + 11286 x y + 3217 x y + 362 x ) z 8 7 2 6 3 5 4 4 5 3 + (56 y + 740 x y + 3217 x y + 7802 x y + 10542 x y + 7802 x y 6 2 7 8 9 8 2 7 3 6 + 3217 x y + 740 x y + 56 x ) z + 4 y + 56 x y + 362 x y + 1219 x y 4 5 5 4 6 3 7 2 8 9 + 2171 x y + 2171 x y + 1219 x y + 362 x y + 56 x y + 4 x )/512 >= 9 8 2 2 7 (4 z + (56 y + 56 x) z + (362 y + 612 x y + 362 x ) z 3 2 2 3 6 + (1219 y + 3281 x y + 3281 x y + 1219 x ) z 4 3 2 2 3 4 5 + (2171 y + 7858 x y + 11654 x y + 7858 x y + 2171 x ) z 5 4 2 3 3 2 4 5 4 + (2171 y + 10270 x y + 20795 x y + 20795 x y + 10270 x y + 2171 x ) z 6 5 2 4 3 3 4 2 5 + (1219 y + 7858 x y + 20795 x y + 28200 x y + 20795 x y + 7858 x y 6 3 7 6 2 5 3 4 4 3 + 1219 x ) z + (362 y + 3281 x y + 11654 x y + 20795 x y + 20795 x y 5 2 6 7 2 + 11654 x y + 3281 x y + 362 x ) z 8 7 2 6 3 5 4 4 5 3 + (56 y + 612 x y + 3281 x y + 7858 x y + 10270 x y + 7858 x y 6 2 7 8 9 8 2 7 3 6 + 3281 x y + 612 x y + 56 x ) z + 4 y + 56 x y + 362 x y + 1219 x y 4 5 5 4 6 3 7 2 8 9 + 2171 x y + 2171 x y + 1219 x y + 362 x y + 56 x y + 4 x )/512 Multiplying both sides by 512 gives: 9 8 8 2 7 7 2 7 3 6 4 z + 56 y z + 56 x z + 362 y z + 740 x y z + 362 x z + 1219 y z 2 6 2 6 3 6 4 5 3 5 + 3217 x y z + 3217 x y z + 1219 x z + 2171 y z + 7802 x y z 2 2 5 3 5 4 5 5 4 4 4 + 11286 x y z + 7802 x y z + 2171 x z + 2171 y z + 10542 x y z 2 3 4 3 2 4 4 4 5 4 6 3 + 20843 x y z + 20843 x y z + 10542 x y z + 2171 x z + 1219 y z 5 3 2 4 3 3 3 3 4 2 3 + 7802 x y z + 20843 x y z + 28536 x y z + 20843 x y z 5 3 6 3 7 2 6 2 2 5 2 + 7802 x y z + 1219 x z + 362 y z + 3217 x y z + 11286 x y z 3 4 2 4 3 2 5 2 2 6 2 7 2 + 20843 x y z + 20843 x y z + 11286 x y z + 3217 x y z + 362 x z 8 7 2 6 3 5 4 4 + 56 y z + 740 x y z + 3217 x y z + 7802 x y z + 10542 x y z 5 3 6 2 7 8 9 8 + 7802 x y z + 3217 x y z + 740 x y z + 56 x z + 4 y + 56 x y 2 7 3 6 4 5 5 4 6 3 7 2 + 362 x y + 1219 x y + 2171 x y + 2171 x y + 1219 x y + 362 x y 8 9 9 8 8 2 7 7 + 56 x y + 4 x >= 4 z + 56 y z + 56 x z + 362 y z + 612 x y z 2 7 3 6 2 6 2 6 3 6 + 362 x z + 1219 y z + 3281 x y z + 3281 x y z + 1219 x z 4 5 3 5 2 2 5 3 5 4 5 + 2171 y z + 7858 x y z + 11654 x y z + 7858 x y z + 2171 x z 5 4 4 4 2 3 4 3 2 4 4 4 + 2171 y z + 10270 x y z + 20795 x y z + 20795 x y z + 10270 x y z 5 4 6 3 5 3 2 4 3 3 3 3 + 2171 x z + 1219 y z + 7858 x y z + 20795 x y z + 28200 x y z 4 2 3 5 3 6 3 7 2 6 2 + 20795 x y z + 7858 x y z + 1219 x z + 362 y z + 3281 x y z 2 5 2 3 4 2 4 3 2 5 2 2 + 11654 x y z + 20795 x y z + 20795 x y z + 11654 x y z 6 2 7 2 8 7 2 6 + 3281 x y z + 362 x z + 56 y z + 612 x y z + 3281 x y z 3 5 4 4 5 3 6 2 7 + 7858 x y z + 10270 x y z + 7858 x y z + 3281 x y z + 612 x y z 8 9 8 2 7 3 6 4 5 5 4 + 56 x z + 4 y + 56 x y + 362 x y + 1219 x y + 2171 x y + 2171 x y 6 3 7 2 8 9 + 1219 x y + 362 x y + 56 x y + 4 x Expanding and collecting terms of the same sign gives: 7 4 4 2 3 4 3 2 4 4 4 128 x y z + 272 x y z + 48 x y z + 48 x y z + 272 x y z 2 4 3 3 3 3 4 2 3 3 4 2 4 3 2 + 48 x y z + 336 x y z + 48 x y z + 48 x y z + 48 x y z 7 4 4 7 + 128 x y z + 272 x y z + 128 x y z >= 2 6 2 6 3 5 2 2 5 3 5 5 3 64 x y z + 64 x y z + 56 x y z + 368 x y z + 56 x y z + 56 x y z 5 3 6 2 2 5 2 5 2 2 6 2 + 56 x y z + 64 x y z + 368 x y z + 368 x y z + 64 x y z 2 6 3 5 5 3 6 2 + 64 x y z + 56 x y z + 56 x y z + 64 x y z Dividing both sides by 8 x y z gives: 6 3 3 2 3 2 3 3 3 3 2 2 2 2 16 z + 34 y z + 6 x y z + 6 x y z + 34 x z + 6 x y z + 42 x y z 3 2 2 3 3 2 6 3 3 6 + 6 x y z + 6 x y z + 6 x y z + 16 y + 34 x y + 16 x >= 5 5 2 4 4 2 4 4 2 4 2 5 8 y z + 8 x z + 7 y z + 46 x y z + 7 x z + 7 y z + 7 x z + 8 y z 4 4 5 5 2 4 4 2 5 + 46 x y z + 46 x y z + 8 x z + 8 x y + 7 x y + 7 x y + 8 x y Expressing in terms of symmetric polynomials gives: 8 {6, 0, 0} + 17 {3, 3, 0} + 6 {3, 2, 1} + 7 {2, 2, 2} >= 8 {5, 1, 0} + 7 {4, 2, 0} + 23 {4, 1, 1} This follows from the following majorizations: 3 {6, 0, 0} + 3 {2, 2, 2} >= 6 {4, 2, 0} 0 >= 0 5 {6, 0, 0} >= 5 {5, 1, 0} left side: [7 {2, 2, 2}, 6 {3, 2, 1}, 17 {3, 3, 0}, 8 {6, 0, 0}] right side: [23 {4, 1, 1}, 7 {4, 2, 0}, 8 {5, 1, 0}] (d27) notsure (c28) trineq(csum(a*sin(A))<=9*R/2); 9 R To prove: --- >= sin(C) c + sin(B) b + sin(A) a 2 Removing the trigonometric expressions gives: 2 2 2 9 R 2 K c + 2 K b + 2 K a --- >= ------------------------ 2 a b c Multiplying both sides by 2 a b c gives: 2 2 2 9 R a b c >= 4 K c + 4 K b + 4 K a Let R = a*b*c/(4*K) . We get: 2 2 2 9 a b c 2 2 2 ---------- >= 4 K c + 4 K b + 4 K a 4 K Multiplying both sides by 4 K gives: 2 2 2 2 2 2 2 2 2 9 a b c >= 16 K c + 16 K b + 16 K a Replacing K^2 by F^2 gives: 2 2 2 2 2 2 2 2 2 9 a b c >= 16 F c + 16 F b + 16 F a Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 2 6 2 2 4 4 2 2 4 2 6 2 4 4 2 9 a b c >= - c + (b + a ) c + (b + 6 a b + a ) c - b + a b + a b 6 - a Expanding and collecting terms of the same sign gives: 6 2 2 2 6 6 2 4 2 4 4 2 4 2 2 4 4 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: 6 5 2 2 4 (z + (3 y + 3 x) z + (9 y + 3 x y + 9 x ) z 3 2 2 3 3 + (13 y + 9 x y + 9 x y + 13 x ) z 4 3 2 2 3 4 2 + (9 y + 9 x y + 15 x y + 9 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (3 y + 3 x y + 9 x y + 9 x y + 3 x y + 3 x ) z + y + 3 x y 2 4 3 3 4 2 5 6 + 9 x y + 13 x y + 9 x y + 3 x y + x )/32 >= 6 5 2 2 4 (2 z + (6 y + 6 x) z + (9 y + 20 x y + 9 x ) z 3 2 2 3 3 + (8 y + 28 x y + 28 x y + 8 x ) z 4 3 2 2 3 4 2 + (9 y + 28 x y + 36 x y + 28 x y + 9 x ) z 5 4 2 3 3 2 4 5 6 5 + (6 y + 20 x y + 28 x y + 28 x y + 20 x y + 6 x ) z + 2 y + 6 x y 2 4 3 3 4 2 5 6 + 9 x y + 8 x y + 9 x y + 6 x y + 2 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 18 y z + 6 x y z + 18 x z + 26 y z + 18 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 18 x y z + 26 x z + 18 y z + 18 x y z + 30 x y z + 18 x y z 4 2 5 4 2 3 3 2 4 5 + 18 x z + 6 y z + 6 x y z + 18 x y z + 18 x y z + 6 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 18 x y + 26 x y + 18 x y + 6 x y + 2 x >= 6 5 5 2 4 4 2 4 3 3 2 3 2 z + 6 y z + 6 x z + 9 y z + 20 x y z + 9 x z + 8 y z + 28 x y z 2 3 3 3 4 2 3 2 2 2 2 3 2 + 28 x y z + 8 x z + 9 y z + 28 x y z + 36 x y z + 28 x y z 4 2 5 4 2 3 3 2 4 5 + 9 x z + 6 y z + 20 x y z + 28 x y z + 28 x y z + 20 x y z + 6 x z 6 5 2 4 3 3 4 2 5 6 + 2 y + 6 x y + 9 x y + 8 x y + 9 x y + 6 x y + 2 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 9 y z + 9 x z + 18 y z + 18 x z + 9 y z + 9 x z + 9 x y 3 3 4 2 4 2 3 2 3 3 2 + 18 x y + 9 x y >= 14 x y z + 10 x y z + 10 x y z + 10 x y z 2 2 2 3 2 4 2 3 3 2 4 + 6 x y z + 10 x y z + 14 x y z + 10 x y z + 10 x y z + 14 x y z Expressing in terms of symmetric polynomials gives: 9 {4, 2, 0} + 9 {3, 3, 0} >= 7 {4, 1, 1} + 10 {3, 2, 1} + {2, 2, 2} This follows from the following majorizations: 7 {4, 2, 0} >= 7 {4, 1, 1} 2 {4, 2, 0} >= 2 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} {3, 3, 0} >= {2, 2, 2} (d28) true (c29) /* 3.15 */ trineq(csum(sin(A))<=2(3*sqrt(3)-4)*r/R); Syntax error csum ( sin ( A ) ) <= 2 ( **$** 3 * sqrt ( 3 ) - 4 ) * Please rephrase or edit. MACSYMA ERROR Error in batch file MACSYMA ERROR (c29)