DOE MACSYMA Version 10. (c1) Batching the file triang Batching done. (d1) triang (c2) (c3) showproof: true $ (c4) /* 6.1 */ trineq(2*csum(h(a))<=sqrt(3)*csum(a)); 2 K 2 K 2 K To prove: sqrt(3) (c + b + a) >= 2 (--- + --- + ---) c b a Multiplying both sides by a b c gives: 2 2 2 sqrt(3) a b c + sqrt(3) a b c + sqrt(3) a b c >= 4 K b c + 4 K a c + 4 K a b Since (4 b + 4 a) c + 4 a b is positive, and since 2 2 2 sqrt(3) a b c + (sqrt(3) a b + sqrt(3) a b) c is positive, we can square both sides to get: 2 2 4 2 3 3 2 3 2 4 3 3 4 2 2 3 a b c + (6 a b + 6 a b ) c + (3 a b + 6 a b + 3 a b ) c >= 2 2 2 2 2 2 2 4 ((16 b + 32 a b + 16 a ) c + (32 a b + 32 a b) c + 16 a b ) s 2 2 3 3 2 2 3 2 + ((- 16 b - 32 a b - 16 a ) c + (- 16 b - 80 a b - 80 a b - 16 a ) c 3 2 2 3 2 3 3 2 3 + (- 32 a b - 80 a b - 32 a b) c - 16 a b - 16 a b ) s 3 2 2 3 3 3 2 2 3 2 + ((16 b + 48 a b + 48 a b + 16 a ) c + (48 a b + 96 a b + 48 a b) c 2 3 3 2 3 3 2 + (48 a b + 48 a b ) c + 16 a b ) s 3 2 2 3 3 2 3 3 2 2 + ((- 16 a b - 32 a b - 16 a b) c + (- 32 a b - 32 a b ) c 3 3 - 16 a b c) s Expanding and collecting terms of the same sign gives: 2 3 3 3 3 2 3 3 3 2 3 2 2 3 16 b c s + 32 a b c s + 16 a c s + 16 b c s + 80 a b c s 2 2 3 3 2 3 3 3 2 2 3 3 3 + 80 a b c s + 16 a c s + 32 a b c s + 80 a b c s + 32 a b c s 2 3 3 3 2 3 3 3 2 2 3 3 3 + 16 a b s + 16 a b s + 16 a b c s + 32 a b c s + 16 a b c s 2 3 2 3 2 2 3 3 2 2 4 2 3 3 + 32 a b c s + 32 a b c s + 16 a b c s + 3 a b c + 6 a b c 3 2 3 2 4 2 3 3 2 4 2 2 + 6 a b c + 3 a b c + 6 a b c + 3 a b c >= 2 2 4 2 4 2 2 4 2 4 2 4 16 b c s + 32 a b c s + 16 a c s + 32 a b c s + 32 a b c s 2 2 4 3 3 2 2 3 2 2 3 2 3 3 2 + 16 a b s + 16 b c s + 48 a b c s + 48 a b c s + 16 a c s 3 2 2 2 2 2 2 3 2 2 2 3 2 + 48 a b c s + 96 a b c s + 48 a b c s + 48 a b c s 3 2 2 3 3 2 + 48 a b c s + 16 a b s Let s = (c+b+a)/2 . We get: 2 2 6 3 2 2 3 5 (2 b + 4 a b + 2 a ) c + (8 b + 28 a b + 28 a b + 8 a ) c 4 3 2 2 3 4 4 + (12 b + 72 a b + 125 a b + 72 a b + 12 a ) c 5 4 2 3 3 2 4 5 3 + (8 b + 72 a b + 206 a b + 206 a b + 72 a b + 8 a ) c 6 5 2 4 3 3 4 2 5 6 2 + (2 b + 28 a b + 125 a b + 206 a b + 125 a b + 28 a b + 2 a ) c 6 2 5 3 4 4 3 5 2 6 2 6 + (4 a b + 28 a b + 72 a b + 72 a b + 28 a b + 4 a b) c + 2 a b 3 5 4 4 5 3 6 2 + 8 a b + 12 a b + 8 a b + 2 a b >= 2 2 6 3 2 2 3 5 (b + 2 a b + a ) c + (8 b + 26 a b + 26 a b + 8 a ) c 4 3 2 2 3 4 4 + (14 b + 76 a b + 125 a b + 76 a b + 14 a ) c 5 4 2 3 3 2 4 5 3 + (8 b + 76 a b + 204 a b + 204 a b + 76 a b + 8 a ) c 6 5 2 4 3 3 4 2 5 6 2 + (b + 26 a b + 125 a b + 204 a b + 125 a b + 26 a b + a ) c 6 2 5 3 4 4 3 5 2 6 2 6 + (2 a b + 26 a b + 76 a b + 76 a b + 26 a b + 2 a b) c + a b 3 5 4 4 5 3 6 2 + 8 a b + 14 a b + 8 a b + a b Expanding and collecting terms of the same sign gives: 2 6 6 2 6 2 5 2 5 2 3 3 3 2 3 b c + 2 a b c + a c + 2 a b c + 2 a b c + 2 a b c + 2 a b c 6 2 5 2 3 3 2 5 2 6 2 6 2 5 + b c + 2 a b c + 2 a b c + 2 a b c + a c + 2 a b c + 2 a b c 5 2 6 2 6 6 2 + 2 a b c + 2 a b c + a b + a b >= 4 4 3 4 3 4 4 4 4 3 4 3 3 4 2 b c + 4 a b c + 4 a b c + 2 a c + 4 a b c + 4 a b c + 4 a b c 4 3 4 4 + 4 a b c + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 8 7 2 2 6 (z + (8 y + 8 x) z + (26 y + 48 x y + 26 x ) z 3 2 2 3 5 + (50 y + 118 x y + 118 x y + 50 x ) z 4 3 2 2 3 4 4 + (63 y + 170 x y + 204 x y + 170 x y + 63 x ) z 5 4 2 3 3 2 4 5 3 + (50 y + 170 x y + 220 x y + 220 x y + 170 x y + 50 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (26 y + 118 x y + 204 x y + 220 x y + 204 x y + 118 x y + 26 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (8 y + 48 x y + 118 x y + 170 x y + 170 x y + 118 x y + 48 x y 7 8 7 2 6 3 5 4 4 5 3 6 2 + 8 x ) z + y + 8 x y + 26 x y + 50 x y + 63 x y + 50 x y + 26 x y 7 8 8 7 2 2 6 + 8 x y + x )/128 >= (z + (8 y + 8 x) z + (20 y + 44 x y + 20 x ) z 3 2 2 3 5 + (26 y + 102 x y + 102 x y + 26 x ) z 4 3 2 2 3 4 4 + (27 y + 150 x y + 252 x y + 150 x y + 27 x ) z 5 4 2 3 3 2 4 5 3 + (26 y + 150 x y + 344 x y + 344 x y + 150 x y + 26 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (20 y + 102 x y + 252 x y + 344 x y + 252 x y + 102 x y + 20 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (8 y + 44 x y + 102 x y + 150 x y + 150 x y + 102 x y + 44 x y 7 8 7 2 6 3 5 4 4 5 3 6 2 + 8 x ) z + y + 8 x y + 20 x y + 26 x y + 27 x y + 26 x y + 20 x y 7 8 + 8 x y + x )/128 Multiplying both sides by 128 gives: 8 7 7 2 6 6 2 6 3 5 2 5 z + 8 y z + 8 x z + 26 y z + 48 x y z + 26 x z + 50 y z + 118 x y z 2 5 3 5 4 4 3 4 2 2 4 3 4 + 118 x y z + 50 x z + 63 y z + 170 x y z + 204 x y z + 170 x y z 4 4 5 3 4 3 2 3 3 3 2 3 + 63 x z + 50 y z + 170 x y z + 220 x y z + 220 x y z 4 3 5 3 6 2 5 2 2 4 2 + 170 x y z + 50 x z + 26 y z + 118 x y z + 204 x y z 3 3 2 4 2 2 5 2 6 2 7 6 + 220 x y z + 204 x y z + 118 x y z + 26 x z + 8 y z + 48 x y z 2 5 3 4 4 3 5 2 6 7 + 118 x y z + 170 x y z + 170 x y z + 118 x y z + 48 x y z + 8 x z 8 7 2 6 3 5 4 4 5 3 6 2 7 + y + 8 x y + 26 x y + 50 x y + 63 x y + 50 x y + 26 x y + 8 x y 8 8 7 7 2 6 6 2 6 3 5 + x >= z + 8 y z + 8 x z + 20 y z + 44 x y z + 20 x z + 26 y z 2 5 2 5 3 5 4 4 3 4 2 2 4 + 102 x y z + 102 x y z + 26 x z + 27 y z + 150 x y z + 252 x y z 3 4 4 4 5 3 4 3 2 3 3 + 150 x y z + 27 x z + 26 y z + 150 x y z + 344 x y z 3 2 3 4 3 5 3 6 2 5 2 + 344 x y z + 150 x y z + 26 x z + 20 y z + 102 x y z 2 4 2 3 3 2 4 2 2 5 2 6 2 7 + 252 x y z + 344 x y z + 252 x y z + 102 x y z + 20 x z + 8 y z 6 2 5 3 4 4 3 5 2 + 44 x y z + 102 x y z + 150 x y z + 150 x y z + 102 x y z 6 7 8 7 2 6 3 5 4 4 5 3 + 44 x y z + 8 x z + y + 8 x y + 20 x y + 26 x y + 27 x y + 26 x y 6 2 7 8 + 20 x y + 8 x y + x Expanding and collecting terms of the same sign gives: 2 6 6 2 6 3 5 2 5 2 5 3 5 6 y z + 4 x y z + 6 x z + 24 y z + 16 x y z + 16 x y z + 24 x z 4 4 3 4 3 4 4 4 5 3 4 3 + 36 y z + 20 x y z + 20 x y z + 36 x z + 24 y z + 20 x y z 4 3 5 3 6 2 5 2 5 2 6 2 + 20 x y z + 24 x z + 6 y z + 16 x y z + 16 x y z + 6 x z 6 2 5 3 4 4 3 5 2 6 + 4 x y z + 16 x y z + 20 x y z + 20 x y z + 16 x y z + 4 x y z 2 6 3 5 4 4 5 3 6 2 + 6 x y + 24 x y + 36 x y + 24 x y + 6 x y >= 2 2 4 2 3 3 3 2 3 2 4 2 3 3 2 48 x y z + 124 x y z + 124 x y z + 48 x y z + 124 x y z 4 2 2 + 48 x y z Dividing both sides by 2 gives: 2 6 6 2 6 3 5 2 5 2 5 3 5 3 y z + 2 x y z + 3 x z + 12 y z + 8 x y z + 8 x y z + 12 x z 4 4 3 4 3 4 4 4 5 3 4 3 + 18 y z + 10 x y z + 10 x y z + 18 x z + 12 y z + 10 x y z 4 3 5 3 6 2 5 2 5 2 6 2 6 + 10 x y z + 12 x z + 3 y z + 8 x y z + 8 x y z + 3 x z + 2 x y z 2 5 3 4 4 3 5 2 6 2 6 + 8 x y z + 10 x y z + 10 x y z + 8 x y z + 2 x y z + 3 x y 3 5 4 4 5 3 6 2 + 12 x y + 18 x y + 12 x y + 3 x y >= 2 2 4 2 3 3 3 2 3 2 4 2 3 3 2 24 x y z + 62 x y z + 62 x y z + 24 x y z + 62 x y z 4 2 2 + 24 x y z Expressing in terms of symmetric polynomials gives: 3 {6, 2, 0} + {6, 1, 1} + 12 {5, 3, 0} + 8 {5, 2, 1} + 9 {4, 4, 0} + 10 {4, 3, 1} >= 12 {4, 2, 2} + 31 {3, 3, 2} This follows from the following majorizations: 3 {6, 2, 0} >= 3 {4, 2, 2} {6, 1, 1} >= {4, 2, 2} 8 {5, 3, 0} >= 8 {4, 2, 2} 4 {5, 3, 0} >= 4 {3, 3, 2} 8 {5, 2, 1} >= 8 {3, 3, 2} 9 {4, 4, 0} >= 9 {3, 3, 2} 10 {4, 3, 1} >= 10 {3, 3, 2} (d4) true (c5) /* 6.4 */ trineq(3*csum(a*b)>=csum(h(a)*h(b))); 2 2 2 4 K 4 K 4 K To prove: 3 (b c + a c + a b) >= ---- + ---- + ---- b c a c a b Multiplying both sides by a b c gives: 2 2 2 2 2 2 2 2 2 3 a b c + 3 a b c + 3 a b c >= 4 K c + 4 K b + 4 K a Replacing K^2 by F^2 gives: 2 2 2 2 2 2 2 2 (3 a b + 3 a b) c + 3 a b c >= 4 F c + 4 F b + 4 F a Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 2 2 2 5 4 2 2 3 (3 a b + 3 a b) c + 3 a b c >= - (c + (b + a) c + (- 2 b - 2 a ) c 3 2 2 3 2 4 2 2 4 5 4 + (- 2 b - 2 a b - 2 a b - 2 a ) c + (b - 2 a b + a ) c + b + a b 2 3 3 2 4 5 - 2 a b - 2 a b + a b + a )/4 Multiplying both sides by 4 gives: 2 2 2 2 2 2 12 a b c + 12 a b c + 12 a b c >= 5 4 4 2 3 2 3 3 2 2 2 2 2 - c - b c - a c + 2 b c + 2 a c + 2 b c + 2 a b c + 2 a b c 3 2 4 2 2 4 5 4 2 3 3 2 4 + 2 a c - b c + 2 a b c - a c - b - a b + 2 a b + 2 a b - a b 5 - a Expanding and collecting terms of the same sign gives: 5 4 4 2 2 2 2 4 2 2 4 5 c + b c + a c + 10 a b c + 10 a b c + b c + 10 a b c + a c + b 4 4 5 2 3 2 3 3 2 3 2 2 3 + a b + a b + a >= 2 b c + 2 a c + 2 b c + 2 a c + 2 a b 3 2 + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 5 4 2 2 3 (2 z + (11 y + 11 x) z + (30 y + 48 x y + 30 x ) z 3 2 2 3 2 + (30 y + 76 x y + 76 x y + 30 x ) z 4 3 2 2 3 4 5 4 2 3 + (11 y + 48 x y + 76 x y + 48 x y + 11 x ) z + 2 y + 11 x y + 30 x y 3 2 4 5 5 4 + 30 x y + 11 x y + 2 x )/16 >= (2 z + (5 y + 5 x) z 2 2 3 3 2 2 3 2 + (6 y + 16 x y + 6 x ) z + (6 y + 24 x y + 24 x y + 6 x ) z 4 3 2 2 3 4 5 4 2 3 + (5 y + 16 x y + 24 x y + 16 x y + 5 x ) z + 2 y + 5 x y + 6 x y 3 2 4 5 + 6 x y + 5 x y + 2 x )/16 Multiplying both sides by 16 gives: 5 4 4 2 3 3 2 3 3 2 2 z + 11 y z + 11 x z + 30 y z + 48 x y z + 30 x z + 30 y z 2 2 2 2 3 2 4 3 2 2 + 76 x y z + 76 x y z + 30 x z + 11 y z + 48 x y z + 76 x y z 3 4 5 4 2 3 3 2 4 + 48 x y z + 11 x z + 2 y + 11 x y + 30 x y + 30 x y + 11 x y 5 5 4 4 2 3 3 2 3 3 2 + 2 x >= 2 z + 5 y z + 5 x z + 6 y z + 16 x y z + 6 x z + 6 y z 2 2 2 2 3 2 4 3 2 2 + 24 x y z + 24 x y z + 6 x z + 5 y z + 16 x y z + 24 x y z 3 4 5 4 2 3 3 2 4 5 + 16 x y z + 5 x z + 2 y + 5 x y + 6 x y + 6 x y + 5 x y + 2 x Expanding and collecting terms of the same sign gives: 4 4 2 3 3 2 3 3 2 2 2 6 y z + 6 x z + 24 y z + 32 x y z + 24 x z + 24 y z + 52 x y z 2 2 3 2 4 3 2 2 3 4 + 52 x y z + 24 x z + 6 y z + 32 x y z + 52 x y z + 32 x y z + 6 x z 4 2 3 3 2 4 + 6 x y + 24 x y + 24 x y + 6 x y >= 0 This is true because a sum of positive terms must be positive. (d5) true (c6) /* 6.5 */ trineq(csum(a^3)>(8/7)*csum(h(a)^3)); 3 3 3 8 K 8 K 8 K 8 (---- + ---- + ----) 3 3 3 3 3 3 c b a To prove: c + b + a > ---------------------- 7 3 3 3 Multiplying both sides by 7 a b c gives: 3 3 6 3 6 3 6 3 3 3 3 3 3 3 3 3 3 3 7 a b c + 7 a b c + 7 a b c > 64 K b c + 64 K a c + 64 K a b Replacing K^2 by F^2 gives: 3 3 6 3 6 6 3 3 2 3 2 3 3 7 a b c + (7 a b + 7 a b ) c > (64 F K b + 64 F K a ) c 2 3 3 + 64 F K a b 2 3 2 3 3 2 3 3 Since (64 F b + 64 F a ) c + 64 F a b is positive, and since 3 3 6 3 6 6 3 3 7 a b c + (7 a b + 7 a b ) c is positive, we can square both sides to get: 6 6 12 6 9 9 6 9 49 a b c + (98 a b + 98 a b ) c 6 12 9 9 12 6 6 + (49 a b + 98 a b + 49 a b ) c > 4 6 4 3 3 4 6 6 ((4096 F b + 8192 F a b + 4096 F a ) c 4 3 6 4 6 3 3 4 6 6 4 + (8192 F a b + 8192 F a b ) c + 4096 F a b ) s 4 6 4 3 3 4 6 7 + ((- 4096 F b - 8192 F a b - 4096 F a ) c 4 7 4 6 4 3 4 4 4 3 4 6 + (- 4096 F b - 4096 F a b - 8192 F a b - 8192 F a b - 4096 F a b 4 7 6 4 3 6 4 6 3 4 - 4096 F a ) c + (- 8192 F a b - 8192 F a b ) c 4 3 7 4 4 6 4 6 4 4 7 3 3 + (- 8192 F a b - 8192 F a b - 8192 F a b - 8192 F a b ) c 4 6 6 4 6 7 4 7 6 3 - 4096 F a b c - 4096 F a b - 4096 F a b ) s 4 7 4 6 4 3 4 4 4 3 4 6 + ((4096 F b + 4096 F a b + 8192 F a b + 8192 F a b + 4096 F a b 4 7 7 4 7 4 4 4 4 7 6 + 4096 F a ) c + (4096 F a b + 8192 F a b + 4096 F a b) c 4 3 7 4 4 6 4 6 4 4 7 3 4 + (8192 F a b + 8192 F a b + 8192 F a b + 8192 F a b ) c 4 4 7 4 7 4 3 4 6 7 4 7 6 + (8192 F a b + 8192 F a b ) c + (4096 F a b + 4096 F a b ) c 4 7 7 2 4 7 4 4 4 4 7 7 + 4096 F a b ) s + ((- 4096 F a b - 8192 F a b - 4096 F a b) c 4 4 7 4 7 4 4 4 7 7 + (- 8192 F a b - 8192 F a b ) c - 4096 F a b c) s Expanding and collecting terms of the same sign gives: 4 6 7 3 4 3 3 7 3 4 6 7 3 4 7 6 3 4096 F b c s + 8192 F a b c s + 4096 F a c s + 4096 F b c s 4 6 6 3 4 3 4 6 3 4 4 3 6 3 + 4096 F a b c s + 8192 F a b c s + 8192 F a b c s 4 6 6 3 4 7 6 3 4 3 6 4 3 + 4096 F a b c s + 4096 F a c s + 8192 F a b c s 4 6 3 4 3 4 3 7 3 3 4 4 6 3 3 + 8192 F a b c s + 8192 F a b c s + 8192 F a b c s 4 6 4 3 3 4 7 3 3 3 4 6 6 3 + 8192 F a b c s + 8192 F a b c s + 4096 F a b c s 4 6 7 3 4 7 6 3 4 7 7 4 4 4 7 + 4096 F a b s + 4096 F a b s + 4096 F a b c s + 8192 F a b c s 4 7 7 4 4 7 4 4 7 4 4 + 4096 F a b c s + 8192 F a b c s + 8192 F a b c s 4 7 7 6 6 12 6 9 9 9 6 9 6 12 6 + 4096 F a b c s + 49 a b c + 98 a b c + 98 a b c + 49 a b c 9 9 6 12 6 6 4 6 6 4 4 3 3 6 4 + 98 a b c + 49 a b c > 4096 F b c s + 8192 F a b c s 4 6 6 4 4 3 6 3 4 4 6 3 3 4 + 4096 F a c s + 8192 F a b c s + 8192 F a b c s 4 6 6 4 4 7 7 2 4 6 7 2 + 4096 F a b s + 4096 F b c s + 4096 F a b c s 4 3 4 7 2 4 4 3 7 2 4 6 7 2 + 8192 F a b c s + 8192 F a b c s + 4096 F a b c s 4 7 7 2 4 7 6 2 4 4 4 6 2 + 4096 F a c s + 4096 F a b c s + 8192 F a b c s 4 7 6 2 4 3 7 4 2 4 4 6 4 2 + 4096 F a b c s + 8192 F a b c s + 8192 F a b c s 4 6 4 4 2 4 7 3 4 2 4 4 7 3 2 + 8192 F a b c s + 8192 F a b c s + 8192 F a b c s 4 7 4 3 2 4 6 7 2 4 7 6 2 + 8192 F a b c s + 4096 F a b c s + 4096 F a b c s 4 7 7 2 + 4096 F a b s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 6 3 3 6 18 7 6 3 4 4 3 6 (2 b + 4 a b + 2 a ) c + (8 b + 8 a b + 16 a b + 16 a b + 8 a b 7 17 8 7 2 6 3 5 4 4 5 3 + 8 a ) c + (4 b + 32 a b + 4 a b + 8 a b + 64 a b + 8 a b 6 2 7 8 16 9 3 6 6 3 9 15 + 4 a b + 32 a b + 4 a ) c + (- 24 b - 68 a b - 68 a b - 24 a ) c 10 9 2 8 3 7 4 6 5 5 + (- 34 b - 120 a b - 76 a b - 172 a b - 258 a b - 152 a b 6 4 7 3 8 2 9 10 14 - 258 a b - 172 a b - 76 a b - 120 a b - 34 a ) c 11 10 2 9 3 8 4 7 5 6 + (16 b - 80 a b - 128 a b - 88 a b - 176 a b - 232 a b 6 5 7 4 8 3 9 2 10 11 13 - 232 a b - 176 a b - 88 a b - 128 a b - 80 a b + 16 a ) c 12 11 2 10 3 9 4 8 5 7 + (56 b + 160 a b + 72 a b + 128 a b + 392 a b + 304 a b 6 6 7 5 8 4 9 3 10 2 11 + 195 a b + 304 a b + 392 a b + 128 a b + 72 a b + 160 a b 12 12 13 12 2 11 3 10 4 9 + 56 a ) c + (16 b + 160 a b + 256 a b + 172 a b + 288 a b 5 8 6 7 7 6 8 5 9 4 10 3 + 616 a b + 292 a b + 292 a b + 616 a b + 288 a b + 172 a b 11 2 12 13 11 + 256 a b + 160 a b + 16 a ) c 14 13 2 12 3 11 4 10 5 9 + (- 34 b - 80 a b + 72 a b + 172 a b - 140 a b + 96 a b 6 8 7 7 8 6 9 5 10 4 11 3 + 234 a b - 88 a b + 234 a b + 96 a b - 140 a b + 172 a b 12 2 13 14 10 15 14 2 13 + 72 a b - 80 a b - 34 a ) c + (- 24 b - 120 a b - 128 a b 3 12 4 11 5 10 6 9 7 8 8 7 + 128 a b + 288 a b + 96 a b + 482 a b + 632 a b + 632 a b 9 6 10 5 11 4 12 3 13 2 14 + 482 a b + 96 a b + 288 a b + 128 a b - 128 a b - 120 a b 15 9 16 2 14 3 13 4 12 5 11 - 24 a ) c + (4 b - 76 a b - 88 a b + 392 a b + 616 a b 6 10 7 9 8 8 9 7 10 6 11 5 + 234 a b + 632 a b + 1308 a b + 632 a b + 234 a b + 616 a b 12 4 13 3 14 2 16 8 + 392 a b - 88 a b - 76 a b + 4 a ) c 17 16 3 14 4 13 5 12 6 11 + (8 b + 32 a b - 172 a b - 176 a b + 304 a b + 292 a b 7 10 8 9 9 8 10 7 11 6 12 5 - 88 a b + 632 a b + 632 a b - 88 a b + 292 a b + 304 a b 13 4 14 3 16 17 7 - 176 a b - 172 a b + 32 a b + 8 a ) c 18 17 2 16 3 15 4 14 5 13 + (2 b + 8 a b + 4 a b - 68 a b - 258 a b - 232 a b 6 12 7 11 8 10 9 9 10 8 11 7 + 195 a b + 292 a b + 234 a b + 482 a b + 234 a b + 292 a b 12 6 13 5 14 4 15 3 16 2 17 + 195 a b - 232 a b - 258 a b - 68 a b + 4 a b + 8 a b 18 6 3 16 5 14 6 13 7 12 8 11 + 2 a ) c + (8 a b - 152 a b - 232 a b + 304 a b + 616 a b 9 10 10 9 11 8 12 7 13 6 14 5 + 96 a b + 96 a b + 616 a b + 304 a b - 232 a b - 152 a b 16 3 5 3 17 4 16 6 14 7 13 8 12 + 8 a b ) c + (16 a b + 64 a b - 258 a b - 176 a b + 392 a b 9 11 10 10 11 9 12 8 13 7 14 6 + 288 a b - 140 a b + 288 a b + 392 a b - 176 a b - 258 a b 16 4 17 3 4 3 18 4 17 5 16 6 15 + 64 a b + 16 a b ) c + (4 a b + 16 a b + 8 a b - 68 a b 7 14 8 13 9 12 10 11 11 10 12 9 - 172 a b - 88 a b + 128 a b + 172 a b + 172 a b + 128 a b 13 8 14 7 15 6 16 5 17 4 18 3 3 - 88 a b - 172 a b - 68 a b + 8 a b + 16 a b + 4 a b ) c 6 16 8 14 9 13 10 12 11 11 12 10 + (4 a b - 76 a b - 128 a b + 72 a b + 256 a b + 72 a b 13 9 14 8 16 6 2 - 128 a b - 76 a b + 4 a b ) c 6 17 7 16 9 14 10 13 11 12 12 11 + (8 a b + 32 a b - 120 a b - 80 a b + 160 a b + 160 a b 13 10 14 9 16 7 17 6 6 18 7 17 - 80 a b - 120 a b + 32 a b + 8 a b ) c + 2 a b + 8 a b 8 16 9 15 10 14 11 13 12 12 13 11 + 4 a b - 24 a b - 34 a b + 16 a b + 56 a b + 16 a b 14 10 15 9 16 8 17 7 18 6 - 34 a b - 24 a b + 4 a b + 8 a b + 2 a b > 6 3 3 6 18 7 6 3 4 4 3 6 7 (b + 2 a b + a ) c + (8 b + 8 a b + 16 a b + 16 a b + 8 a b + 8 a ) 17 8 7 2 6 3 5 4 4 5 3 6 2 c + (10 b + 32 a b + 10 a b + 20 a b + 64 a b + 20 a b + 10 a b 7 8 16 9 3 6 6 3 9 15 + 32 a b + 10 a ) c + (- 24 b - 70 a b - 70 a b - 24 a ) c 10 9 2 8 3 7 4 6 5 5 + (- 49 b - 120 a b - 94 a b - 202 a b - 273 a b - 188 a b 6 4 7 3 8 2 9 10 14 - 273 a b - 202 a b - 94 a b - 120 a b - 49 a ) c 11 10 2 9 3 8 4 7 5 6 + (16 b - 80 a b - 128 a b - 76 a b - 176 a b - 220 a b 6 5 7 4 8 3 9 2 10 11 13 - 220 a b - 176 a b - 76 a b - 128 a b - 80 a b + 16 a ) c 12 11 2 10 3 9 4 8 5 7 + (76 b + 160 a b + 84 a b + 168 a b + 404 a b + 328 a b 6 6 7 5 8 4 9 3 10 2 11 + 185 a b + 328 a b + 404 a b + 168 a b + 84 a b + 160 a b 12 12 13 12 2 11 3 10 4 9 + 76 a ) c + (16 b + 160 a b + 256 a b + 142 a b + 288 a b 5 8 6 7 7 6 8 5 9 4 10 3 + 580 a b + 262 a b + 262 a b + 580 a b + 288 a b + 142 a b 11 2 12 13 11 + 256 a b + 160 a b + 16 a ) c 14 13 2 12 3 11 4 10 5 9 + (- 49 b - 80 a b + 84 a b + 142 a b - 134 a b + 120 a b 6 8 7 7 8 6 9 5 10 4 11 3 + 237 a b - 76 a b + 237 a b + 120 a b - 134 a b + 142 a b 12 2 13 14 10 15 14 2 13 + 84 a b - 80 a b - 49 a ) c + (- 24 b - 120 a b - 128 a b 3 12 4 11 5 10 6 9 7 8 8 7 + 168 a b + 288 a b + 120 a b + 424 a b + 656 a b + 656 a b 9 6 10 5 11 4 12 3 13 2 14 + 424 a b + 120 a b + 288 a b + 168 a b - 128 a b - 120 a b 15 9 16 2 14 3 13 4 12 5 11 - 24 a ) c + (10 b - 94 a b - 76 a b + 404 a b + 580 a b 6 10 7 9 8 8 9 7 10 6 11 5 + 237 a b + 656 a b + 1254 a b + 656 a b + 237 a b + 580 a b 12 4 13 3 14 2 16 8 + 404 a b - 76 a b - 94 a b + 10 a ) c 17 16 3 14 4 13 5 12 6 11 + (8 b + 32 a b - 202 a b - 176 a b + 328 a b + 262 a b 7 10 8 9 9 8 10 7 11 6 12 5 - 76 a b + 656 a b + 656 a b - 76 a b + 262 a b + 328 a b 13 4 14 3 16 17 7 - 176 a b - 202 a b + 32 a b + 8 a ) c 18 17 2 16 3 15 4 14 5 13 + (b + 8 a b + 10 a b - 70 a b - 273 a b - 220 a b 6 12 7 11 8 10 9 9 10 8 11 7 + 185 a b + 262 a b + 237 a b + 424 a b + 237 a b + 262 a b 12 6 13 5 14 4 15 3 16 2 17 + 185 a b - 220 a b - 273 a b - 70 a b + 10 a b + 8 a b 18 6 3 16 5 14 6 13 7 12 8 11 + a ) c + (20 a b - 188 a b - 220 a b + 328 a b + 580 a b 9 10 10 9 11 8 12 7 13 6 14 5 + 120 a b + 120 a b + 580 a b + 328 a b - 220 a b - 188 a b 16 3 5 3 17 4 16 6 14 7 13 + 20 a b ) c + (16 a b + 64 a b - 273 a b - 176 a b 8 12 9 11 10 10 11 9 12 8 13 7 + 404 a b + 288 a b - 134 a b + 288 a b + 404 a b - 176 a b 14 6 16 4 17 3 4 - 273 a b + 64 a b + 16 a b ) c 3 18 4 17 5 16 6 15 7 14 8 13 + (2 a b + 16 a b + 20 a b - 70 a b - 202 a b - 76 a b 9 12 10 11 11 10 12 9 13 8 14 7 + 168 a b + 142 a b + 142 a b + 168 a b - 76 a b - 202 a b 15 6 16 5 17 4 18 3 3 - 70 a b + 20 a b + 16 a b + 2 a b ) c 6 16 8 14 9 13 10 12 11 11 12 10 + (10 a b - 94 a b - 128 a b + 84 a b + 256 a b + 84 a b 13 9 14 8 16 6 2 - 128 a b - 94 a b + 10 a b ) c 6 17 7 16 9 14 10 13 11 12 12 11 + (8 a b + 32 a b - 120 a b - 80 a b + 160 a b + 160 a b 13 10 14 9 16 7 17 6 6 18 7 17 - 80 a b - 120 a b + 32 a b + 8 a b ) c + a b + 8 a b 8 16 9 15 10 14 11 13 12 12 13 11 + 10 a b - 24 a b - 49 a b + 16 a b + 76 a b + 16 a b 14 10 15 9 16 8 17 7 18 6 - 49 a b - 24 a b + 10 a b + 8 a b + a b Expanding and collecting terms of the same sign gives: 6 18 3 3 18 6 18 3 6 15 6 3 15 10 14 b c + 2 a b c + a c + 2 a b c + 2 a b c + 15 b c 2 8 14 3 7 14 4 6 14 5 5 14 6 4 14 + 18 a b c + 30 a b c + 15 a b c + 36 a b c + 15 a b c 7 3 14 8 2 14 10 14 6 6 12 3 10 11 + 30 a b c + 18 a b c + 15 a c + 10 a b c + 30 a b c 5 8 11 6 7 11 7 6 11 8 5 11 10 3 11 + 36 a b c + 30 a b c + 30 a b c + 36 a b c + 30 a b c 14 10 3 11 10 11 3 10 14 10 6 9 9 + 15 b c + 30 a b c + 30 a b c + 15 a c + 58 a b c 9 6 9 2 14 8 5 11 8 8 8 8 11 5 8 + 58 a b c + 18 a b c + 36 a b c + 54 a b c + 36 a b c 14 2 8 3 14 7 6 11 7 11 6 7 14 3 7 + 18 a b c + 30 a b c + 30 a b c + 30 a b c + 30 a b c 18 6 3 15 6 4 14 6 6 12 6 7 11 6 + b c + 2 a b c + 15 a b c + 10 a b c + 30 a b c 9 9 6 11 7 6 12 6 6 14 4 6 15 3 6 + 58 a b c + 30 a b c + 10 a b c + 15 a b c + 2 a b c 18 6 5 14 5 8 11 5 11 8 5 14 5 5 + a c + 36 a b c + 36 a b c + 36 a b c + 36 a b c 6 14 4 14 6 4 3 18 3 6 15 3 7 14 3 + 15 a b c + 15 a b c + 2 a b c + 2 a b c + 30 a b c 10 11 3 11 10 3 14 7 3 15 6 3 18 3 3 + 30 a b c + 30 a b c + 30 a b c + 2 a b c + 2 a b c 8 14 2 14 8 2 6 18 10 14 14 10 18 6 + 18 a b c + 18 a b c + a b + 15 a b + 15 a b + a b > 8 16 2 6 16 3 5 16 5 3 16 6 2 16 8 16 6 b c + 6 a b c + 12 a b c + 12 a b c + 6 a b c + 6 a c 3 8 13 5 6 13 6 5 13 8 3 13 12 12 + 12 a b c + 12 a b c + 12 a b c + 12 a b c + 20 b c 2 10 12 3 9 12 4 8 12 5 7 12 7 5 12 + 12 a b c + 40 a b c + 12 a b c + 24 a b c + 24 a b c 8 4 12 9 3 12 10 2 12 12 12 2 12 10 + 12 a b c + 40 a b c + 12 a b c + 20 a c + 12 a b c 4 10 10 5 9 10 6 8 10 7 7 10 8 6 10 + 6 a b c + 24 a b c + 3 a b c + 12 a b c + 3 a b c 9 5 10 10 4 10 12 2 10 3 12 9 5 10 9 + 24 a b c + 6 a b c + 12 a b c + 40 a b c + 24 a b c 7 8 9 8 7 9 10 5 9 12 3 9 16 8 + 24 a b c + 24 a b c + 24 a b c + 40 a b c + 6 b c 3 13 8 4 12 8 6 10 8 7 9 8 9 7 8 + 12 a b c + 12 a b c + 3 a b c + 24 a b c + 24 a b c 10 6 8 12 4 8 13 3 8 16 8 5 12 7 + 3 a b c + 12 a b c + 12 a b c + 6 a c + 24 a b c 7 10 7 8 9 7 9 8 7 10 7 7 12 5 7 + 12 a b c + 24 a b c + 24 a b c + 12 a b c + 24 a b c 2 16 6 5 13 6 8 10 6 10 8 6 13 5 6 + 6 a b c + 12 a b c + 3 a b c + 3 a b c + 12 a b c 16 2 6 3 16 5 6 13 5 7 12 5 9 10 5 + 6 a b c + 12 a b c + 12 a b c + 24 a b c + 24 a b c 10 9 5 12 7 5 13 6 5 16 3 5 8 12 4 + 24 a b c + 24 a b c + 12 a b c + 12 a b c + 12 a b c 10 10 4 12 8 4 5 16 3 8 13 3 9 12 3 + 6 a b c + 12 a b c + 12 a b c + 12 a b c + 40 a b c 12 9 3 13 8 3 16 5 3 6 16 2 10 12 2 + 40 a b c + 12 a b c + 12 a b c + 6 a b c + 12 a b c 12 10 2 16 6 2 8 16 12 12 16 8 + 12 a b c + 6 a b c + 6 a b + 20 a b + 6 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 24 23 2 2 22 (16 z + (192 y + 192 x) z + (1122 y + 2244 x y + 1122 x ) z 3 2 2 3 21 + (4310 y + 12930 x y + 12930 x y + 4310 x ) z 4 3 2 2 3 4 20 + (12378 y + 49434 x y + 74016 x y + 49434 x y + 12378 x ) z 5 4 2 3 3 2 4 + (28650 y + 142086 x y + 282048 x y + 282048 x y + 142086 x y 5 19 6 5 2 4 3 3 + 28650 x ) z + (56137 y + 329640 x y + 808149 x y + 1068268 x y 4 2 5 6 18 + 808149 x y + 329640 x y + 56137 x ) z 7 6 2 5 3 4 4 3 + (96189 y + 646107 x y + 1865223 x y + 3029241 x y + 3029241 x y 5 2 6 7 17 + 1865223 x y + 646107 x y + 96189 x ) z 8 7 2 6 3 5 4 4 + (147072 y + 1102053 x y + 3622914 x y + 6888657 x y + 8435544 x y 5 3 6 2 7 8 16 + 6888657 x y + 3622914 x y + 1102053 x y + 147072 x ) z 9 8 2 7 3 6 4 5 + (202954 y + 1665738 x y + 6090480 x y + 13124608 x y + 18707772 x y 5 4 6 3 7 2 8 9 + 18707772 x y + 13124608 x y + 6090480 x y + 1665738 x y + 202954 x ) 15 10 9 2 8 3 7 z + (254415 y + 2254710 x y + 9014715 x y + 21533664 x y 4 6 5 5 6 4 7 3 + 34552842 x y + 40051836 x y + 34552842 x y + 21533664 x y 8 2 9 10 14 + 9014715 x y + 2254710 x y + 254415 x ) z 11 10 2 9 3 8 + (290871 y + 2750283 x y + 11865855 x y + 30921771 x y 4 7 5 6 6 5 7 4 + 54671562 x y + 70806330 x y + 70806330 x y + 54671562 x y 8 3 9 2 10 11 13 + 30921771 x y + 11865855 x y + 2750283 x y + 290871 x ) z 12 11 2 10 3 9 + (304068 y + 3034719 x y + 13967538 x y + 39212859 x y 4 8 5 7 6 6 7 5 + 75331008 x y + 106645866 x y + 118560860 x y + 106645866 x y 8 4 9 3 10 2 11 + 75331008 x y + 39212859 x y + 13967538 x y + 3034719 x y 12 12 13 12 2 11 + 304068 x ) z + (290871 y + 3034719 x y + 14743836 x y 3 10 4 9 5 8 6 7 + 44116740 x y + 91126077 x y + 139364829 x y + 168062544 x y 7 6 8 5 9 4 10 3 + 168062544 x y + 139364829 x y + 91126077 x y + 44116740 x y 11 2 12 13 11 + 14743836 x y + 3034719 x y + 290871 x ) z 14 13 2 12 3 11 + (254415 y + 2750283 x y + 13967538 x y + 44116740 x y 4 10 5 9 6 8 7 7 + 97073538 x y + 159191637 x y + 206014905 x y + 222488112 x y 8 6 9 5 10 4 11 3 + 206014905 x y + 159191637 x y + 97073538 x y + 44116740 x y 12 2 13 14 10 + 13967538 x y + 2750283 x y + 254415 x ) z 15 14 2 13 3 12 + (202954 y + 2254710 x y + 11865855 x y + 39212859 x y 4 11 5 10 6 9 7 8 + 91126077 x y + 159191637 x y + 220335114 x y + 254194650 x y 8 7 9 6 10 5 11 4 + 254194650 x y + 220335114 x y + 159191637 x y + 91126077 x y 12 3 13 2 14 15 9 + 39212859 x y + 11865855 x y + 2254710 x y + 202954 x ) z 16 15 2 14 3 13 + (147072 y + 1665738 x y + 9014715 x y + 30921771 x y 4 12 5 11 6 10 7 9 + 75331008 x y + 139364829 x y + 206014905 x y + 254194650 x y 8 8 9 7 10 6 11 5 + 271272672 x y + 254194650 x y + 206014905 x y + 139364829 x y 12 4 13 3 14 2 15 + 75331008 x y + 30921771 x y + 9014715 x y + 1665738 x y 16 8 17 16 2 15 + 147072 x ) z + (96189 y + 1102053 x y + 6090480 x y 3 14 4 13 5 12 6 11 + 21533664 x y + 54671562 x y + 106645866 x y + 168062544 x y 7 10 8 9 9 8 10 7 + 222488112 x y + 254194650 x y + 254194650 x y + 222488112 x y 11 6 12 5 13 4 14 3 + 168062544 x y + 106645866 x y + 54671562 x y + 21533664 x y 15 2 16 17 7 + 6090480 x y + 1102053 x y + 96189 x ) z 18 17 2 16 3 15 + (56137 y + 646107 x y + 3622914 x y + 13124608 x y 4 14 5 13 6 12 7 11 + 34552842 x y + 70806330 x y + 118560860 x y + 168062544 x y 8 10 9 9 10 8 11 7 + 206014905 x y + 220335114 x y + 206014905 x y + 168062544 x y 12 6 13 5 14 4 15 3 + 118560860 x y + 70806330 x y + 34552842 x y + 13124608 x y 16 2 17 18 6 + 3622914 x y + 646107 x y + 56137 x ) z 19 18 2 17 3 16 + (28650 y + 329640 x y + 1865223 x y + 6888657 x y 4 15 5 14 6 13 7 12 + 18707772 x y + 40051836 x y + 70806330 x y + 106645866 x y 8 11 9 10 10 9 11 8 + 139364829 x y + 159191637 x y + 159191637 x y + 139364829 x y 12 7 13 6 14 5 15 4 + 106645866 x y + 70806330 x y + 40051836 x y + 18707772 x y 16 3 17 2 18 19 5 + 6888657 x y + 1865223 x y + 329640 x y + 28650 x ) z 20 19 2 18 3 17 4 16 + (12378 y + 142086 x y + 808149 x y + 3029241 x y + 8435544 x y 5 15 6 14 7 13 8 12 + 18707772 x y + 34552842 x y + 54671562 x y + 75331008 x y 9 11 10 10 11 9 12 8 + 91126077 x y + 97073538 x y + 91126077 x y + 75331008 x y 13 7 14 6 15 5 16 4 + 54671562 x y + 34552842 x y + 18707772 x y + 8435544 x y 17 3 18 2 19 20 4 + 3029241 x y + 808149 x y + 142086 x y + 12378 x ) z 21 20 2 19 3 18 4 17 + (4310 y + 49434 x y + 282048 x y + 1068268 x y + 3029241 x y 5 16 6 15 7 14 8 13 + 6888657 x y + 13124608 x y + 21533664 x y + 30921771 x y 9 12 10 11 11 10 12 9 + 39212859 x y + 44116740 x y + 44116740 x y + 39212859 x y 13 8 14 7 15 6 16 5 + 30921771 x y + 21533664 x y + 13124608 x y + 6888657 x y 17 4 18 3 19 2 20 21 3 + 3029241 x y + 1068268 x y + 282048 x y + 49434 x y + 4310 x ) z 22 21 2 20 3 19 4 18 + (1122 y + 12930 x y + 74016 x y + 282048 x y + 808149 x y 5 17 6 16 7 15 8 14 + 1865223 x y + 3622914 x y + 6090480 x y + 9014715 x y 9 13 10 12 11 11 12 10 + 11865855 x y + 13967538 x y + 14743836 x y + 13967538 x y 13 9 14 8 15 7 16 6 + 11865855 x y + 9014715 x y + 6090480 x y + 3622914 x y 17 5 18 4 19 3 20 2 21 + 1865223 x y + 808149 x y + 282048 x y + 74016 x y + 12930 x y 22 2 23 22 2 21 3 20 + 1122 x ) z + (192 y + 2244 x y + 12930 x y + 49434 x y 4 19 5 18 6 17 7 16 + 142086 x y + 329640 x y + 646107 x y + 1102053 x y 8 15 9 14 10 13 11 12 + 1665738 x y + 2254710 x y + 2750283 x y + 3034719 x y 12 11 13 10 14 9 15 8 + 3034719 x y + 2750283 x y + 2254710 x y + 1665738 x y 16 7 17 6 18 5 19 4 + 1102053 x y + 646107 x y + 329640 x y + 142086 x y 20 3 21 2 22 23 24 23 + 49434 x y + 12930 x y + 2244 x y + 192 x ) z + 16 y + 192 x y 2 22 3 21 4 20 5 19 6 18 + 1122 x y + 4310 x y + 12378 x y + 28650 x y + 56137 x y 7 17 8 16 9 15 10 14 + 96189 x y + 147072 x y + 202954 x y + 254415 x y 11 13 12 12 13 11 14 10 + 290871 x y + 304068 x y + 290871 x y + 254415 x y 15 9 16 8 17 7 18 6 19 5 + 202954 x y + 147072 x y + 96189 x y + 56137 x y + 28650 x y 20 4 21 3 22 2 23 24 + 12378 x y + 4310 x y + 1122 x y + 192 x y + 16 x )/8388608 > 24 23 2 2 22 (32 z + (384 y + 384 x) z + (2244 y + 4488 x y + 2244 x ) z 3 2 2 3 21 + (8620 y + 25860 x y + 25860 x y + 8620 x ) z 4 3 2 2 3 4 20 + (24756 y + 98868 x y + 148032 x y + 98868 x y + 24756 x ) z 5 4 2 3 3 2 4 + (57300 y + 284172 x y + 564096 x y + 564096 x y + 284172 x y 5 19 6 5 2 4 3 3 + 57300 x ) z + (112078 y + 658104 x y + 1613358 x y + 2136712 x y 4 2 5 6 18 + 1613358 x y + 658104 x y + 112078 x ) z 7 6 2 5 3 4 4 3 + (190614 y + 1279866 x y + 3693402 x y + 6033606 x y + 6033606 x y 5 2 6 7 17 + 3693402 x y + 1279866 x y + 190614 x ) z 8 7 2 6 3 5 4 4 + (286647 y + 2144130 x y + 7035912 x y + 13504938 x y + 16665786 x y 5 3 6 2 7 8 16 + 13504938 x y + 7035912 x y + 2144130 x y + 286647 x ) z 9 8 2 7 3 6 4 5 + (385720 y + 3149784 x y + 11454192 x y + 24913872 x y + 36149808 x y 5 4 6 3 7 2 8 9 + 36149808 x y + 24913872 x y + 11454192 x y + 3149784 x y + 385720 x ) 15 10 9 2 8 3 7 z + (470022 y + 4120164 x y + 16276014 x y + 39030528 x y 4 6 5 5 6 4 7 3 + 64169460 x y + 75560328 x y + 64169460 x y + 39030528 x y 8 2 9 10 14 + 16276014 x y + 4120164 x y + 470022 x ) z 11 10 2 9 3 8 + (525294 y + 4870818 x y + 20564154 x y + 53261238 x y 4 7 5 6 6 5 7 4 + 96365844 x y + 128896332 x y + 128896332 x y + 96365844 x y 8 3 9 2 10 11 13 + 53261238 x y + 20564154 x y + 4870818 x y + 525294 x ) z 12 11 2 10 3 9 + (544338 y + 5273874 x y + 23475684 x y + 64665498 x y 4 8 5 7 6 6 7 5 + 125929446 x y + 185735772 x y + 211491672 x y + 185735772 x y 8 4 9 3 10 2 11 + 125929446 x y + 64665498 x y + 23475684 x y + 5273874 x y 12 12 13 12 2 11 + 544338 x ) z + (525294 y + 5273874 x y + 24499080 x y 3 10 4 9 5 8 6 7 + 70954728 x y + 146433390 x y + 232551954 x y + 293106000 x y 7 6 8 5 9 4 10 3 + 293106000 x y + 232551954 x y + 146433390 x y + 70954728 x y 11 2 12 13 11 + 24499080 x y + 5273874 x y + 525294 x ) z 14 13 2 12 3 11 + (470022 y + 4870818 x y + 23475684 x y + 70954728 x y 4 10 5 9 6 8 7 7 + 153727836 x y + 258600174 x y + 352154802 x y + 390835968 x y 8 6 9 5 10 4 11 3 + 352154802 x y + 258600174 x y + 153727836 x y + 70954728 x y 12 2 13 14 10 + 23475684 x y + 4870818 x y + 470022 x ) z 15 14 2 13 3 12 + (385720 y + 4120164 x y + 20564154 x y + 64665498 x y 4 11 5 10 6 9 7 8 + 146433390 x y + 258600174 x y + 373537756 x y + 449239608 x y 8 7 9 6 10 5 11 4 + 449239608 x y + 373537756 x y + 258600174 x y + 146433390 x y 12 3 13 2 14 15 9 + 64665498 x y + 20564154 x y + 4120164 x y + 385720 x ) z 16 15 2 14 3 13 + (286647 y + 3149784 x y + 16276014 x y + 53261238 x y 4 12 5 11 6 10 7 9 + 125929446 x y + 232551954 x y + 352154802 x y + 449239608 x y 8 8 9 7 10 6 11 5 + 487124118 x y + 449239608 x y + 352154802 x y + 232551954 x y 12 4 13 3 14 2 15 + 125929446 x y + 53261238 x y + 16276014 x y + 3149784 x y 16 8 17 16 2 15 + 286647 x ) z + (190614 y + 2144130 x y + 11454192 x y 3 14 4 13 5 12 6 11 + 39030528 x y + 96365844 x y + 185735772 x y + 293106000 x y 7 10 8 9 9 8 10 7 + 390835968 x y + 449239608 x y + 449239608 x y + 390835968 x y 11 6 12 5 13 4 14 3 + 293106000 x y + 185735772 x y + 96365844 x y + 39030528 x y 15 2 16 17 7 + 11454192 x y + 2144130 x y + 190614 x ) z 18 17 2 16 3 15 + (112078 y + 1279866 x y + 7035912 x y + 24913872 x y 4 14 5 13 6 12 7 11 + 64169460 x y + 128896332 x y + 211491672 x y + 293106000 x y 8 10 9 9 10 8 11 7 + 352154802 x y + 373537756 x y + 352154802 x y + 293106000 x y 12 6 13 5 14 4 15 3 + 211491672 x y + 128896332 x y + 64169460 x y + 24913872 x y 16 2 17 18 6 + 7035912 x y + 1279866 x y + 112078 x ) z 19 18 2 17 3 16 + (57300 y + 658104 x y + 3693402 x y + 13504938 x y 4 15 5 14 6 13 7 12 + 36149808 x y + 75560328 x y + 128896332 x y + 185735772 x y 8 11 9 10 10 9 11 8 + 232551954 x y + 258600174 x y + 258600174 x y + 232551954 x y 12 7 13 6 14 5 15 4 + 185735772 x y + 128896332 x y + 75560328 x y + 36149808 x y 16 3 17 2 18 19 5 + 13504938 x y + 3693402 x y + 658104 x y + 57300 x ) z 20 19 2 18 3 17 + (24756 y + 284172 x y + 1613358 x y + 6033606 x y 4 16 5 15 6 14 7 13 + 16665786 x y + 36149808 x y + 64169460 x y + 96365844 x y 8 12 9 11 10 10 11 9 + 125929446 x y + 146433390 x y + 153727836 x y + 146433390 x y 12 8 13 7 14 6 15 5 + 125929446 x y + 96365844 x y + 64169460 x y + 36149808 x y 16 4 17 3 18 2 19 + 16665786 x y + 6033606 x y + 1613358 x y + 284172 x y 20 4 21 20 2 19 3 18 + 24756 x ) z + (8620 y + 98868 x y + 564096 x y + 2136712 x y 4 17 5 16 6 15 7 14 + 6033606 x y + 13504938 x y + 24913872 x y + 39030528 x y 8 13 9 12 10 11 11 10 + 53261238 x y + 64665498 x y + 70954728 x y + 70954728 x y 12 9 13 8 14 7 15 6 + 64665498 x y + 53261238 x y + 39030528 x y + 24913872 x y 16 5 17 4 18 3 19 2 + 13504938 x y + 6033606 x y + 2136712 x y + 564096 x y 20 21 3 22 21 2 20 + 98868 x y + 8620 x ) z + (2244 y + 25860 x y + 148032 x y 3 19 4 18 5 17 6 16 + 564096 x y + 1613358 x y + 3693402 x y + 7035912 x y 7 15 8 14 9 13 10 12 + 11454192 x y + 16276014 x y + 20564154 x y + 23475684 x y 11 11 12 10 13 9 14 8 + 24499080 x y + 23475684 x y + 20564154 x y + 16276014 x y 15 7 16 6 17 5 18 4 + 11454192 x y + 7035912 x y + 3693402 x y + 1613358 x y 19 3 20 2 21 22 2 + 564096 x y + 148032 x y + 25860 x y + 2244 x ) z 23 22 2 21 3 20 4 19 + (384 y + 4488 x y + 25860 x y + 98868 x y + 284172 x y 5 18 6 17 7 16 8 15 + 658104 x y + 1279866 x y + 2144130 x y + 3149784 x y 9 14 10 13 11 12 12 11 + 4120164 x y + 4870818 x y + 5273874 x y + 5273874 x y 13 10 14 9 15 8 16 7 + 4870818 x y + 4120164 x y + 3149784 x y + 2144130 x y 17 6 18 5 19 4 20 3 21 2 + 1279866 x y + 658104 x y + 284172 x y + 98868 x y + 25860 x y 22 23 24 23 2 22 3 21 + 4488 x y + 384 x ) z + 32 y + 384 x y + 2244 x y + 8620 x y 4 20 5 19 6 18 7 17 8 16 + 24756 x y + 57300 x y + 112078 x y + 190614 x y + 286647 x y 9 15 10 14 11 13 12 12 + 385720 x y + 470022 x y + 525294 x y + 544338 x y 13 11 14 10 15 9 16 8 + 525294 x y + 470022 x y + 385720 x y + 286647 x y 17 7 18 6 19 5 20 4 21 3 + 190614 x y + 112078 x y + 57300 x y + 24756 x y + 8620 x y 22 2 23 24 + 2244 x y + 384 x y + 32 x )/16777216 Multiplying both sides by 16777216 gives: 24 23 23 2 22 22 2 22 32 z + 384 y z + 384 x z + 2244 y z + 4488 x y z + 2244 x z 3 21 2 21 2 21 3 21 4 20 + 8620 y z + 25860 x y z + 25860 x y z + 8620 x z + 24756 y z 3 20 2 2 20 3 20 4 20 + 98868 x y z + 148032 x y z + 98868 x y z + 24756 x z 5 19 4 19 2 3 19 3 2 19 + 57300 y z + 284172 x y z + 564096 x y z + 564096 x y z 4 19 5 19 6 18 5 18 + 284172 x y z + 57300 x z + 112274 y z + 659280 x y z 2 4 18 3 3 18 4 2 18 5 18 + 1616298 x y z + 2136536 x y z + 1616298 x y z + 659280 x y z 6 18 7 17 6 17 2 5 17 + 112274 x z + 192378 y z + 1292214 x y z + 3730446 x y z 3 4 17 4 3 17 5 2 17 6 17 + 6058482 x y z + 6058482 x y z + 3730446 x y z + 1292214 x y z 7 17 8 16 7 16 2 6 16 + 192378 x z + 294144 y z + 2204106 x y z + 7245828 x y z 3 5 16 4 4 16 5 3 16 + 13777314 x y z + 16871088 x y z + 13777314 x y z 6 2 16 7 16 8 16 9 15 + 7245828 x y z + 2204106 x y z + 294144 x z + 405908 y z 8 15 2 7 15 3 6 15 + 3331476 x y z + 12180960 x y z + 26249216 x y z 4 5 15 5 4 15 6 3 15 + 37415544 x y z + 37415544 x y z + 26249216 x y z 7 2 15 8 15 9 15 10 14 + 12180960 x y z + 3331476 x y z + 405908 x z + 508830 y z 9 14 2 8 14 3 7 14 + 4509420 x y z + 18029430 x y z + 43067328 x y z 4 6 14 5 5 14 6 4 14 + 69105684 x y z + 80103672 x y z + 69105684 x y z 7 3 14 8 2 14 9 14 10 14 + 43067328 x y z + 18029430 x y z + 4509420 x y z + 508830 x z 11 13 10 13 2 9 13 3 8 13 + 581742 y z + 5500566 x y z + 23731710 x y z + 61843542 x y z 4 7 13 5 6 13 6 5 13 + 109343124 x y z + 141612660 x y z + 141612660 x y z 7 4 13 8 3 13 9 2 13 + 109343124 x y z + 61843542 x y z + 23731710 x y z 10 13 11 13 12 12 11 12 + 5500566 x y z + 581742 x z + 608136 y z + 6069438 x y z 2 10 12 3 9 12 4 8 12 + 27935076 x y z + 78425718 x y z + 150662016 x y z 5 7 12 6 6 12 7 5 12 + 213291732 x y z + 237121720 x y z + 213291732 x y z 8 4 12 9 3 12 10 2 12 + 150662016 x y z + 78425718 x y z + 27935076 x y z 11 12 12 12 13 11 12 11 + 6069438 x y z + 608136 x z + 581742 y z + 6069438 x y z 2 11 11 3 10 11 4 9 11 + 29487672 x y z + 88233480 x y z + 182252154 x y z 5 8 11 6 7 11 7 6 11 + 278729658 x y z + 336125088 x y z + 336125088 x y z 8 5 11 9 4 11 10 3 11 + 278729658 x y z + 182252154 x y z + 88233480 x y z 11 2 11 12 11 13 11 14 10 + 29487672 x y z + 6069438 x y z + 581742 x z + 508830 y z 13 10 2 12 10 3 11 10 + 5500566 x y z + 27935076 x y z + 88233480 x y z 4 10 10 5 9 10 6 8 10 + 194147076 x y z + 318383274 x y z + 412029810 x y z 7 7 10 8 6 10 9 5 10 + 444976224 x y z + 412029810 x y z + 318383274 x y z 10 4 10 11 3 10 12 2 10 + 194147076 x y z + 88233480 x y z + 27935076 x y z 13 10 14 10 15 9 14 9 + 5500566 x y z + 508830 x z + 405908 y z + 4509420 x y z 2 13 9 3 12 9 4 11 9 + 23731710 x y z + 78425718 x y z + 182252154 x y z 5 10 9 6 9 9 7 8 9 + 318383274 x y z + 440670228 x y z + 508389300 x y z 8 7 9 9 6 9 10 5 9 + 508389300 x y z + 440670228 x y z + 318383274 x y z 11 4 9 12 3 9 13 2 9 + 182252154 x y z + 78425718 x y z + 23731710 x y z 14 9 15 9 16 8 15 8 + 4509420 x y z + 405908 x z + 294144 y z + 3331476 x y z 2 14 8 3 13 8 4 12 8 + 18029430 x y z + 61843542 x y z + 150662016 x y z 5 11 8 6 10 8 7 9 8 + 278729658 x y z + 412029810 x y z + 508389300 x y z 8 8 8 9 7 8 10 6 8 + 542545344 x y z + 508389300 x y z + 412029810 x y z 11 5 8 12 4 8 13 3 8 + 278729658 x y z + 150662016 x y z + 61843542 x y z 14 2 8 15 8 16 8 17 7 + 18029430 x y z + 3331476 x y z + 294144 x z + 192378 y z 16 7 2 15 7 3 14 7 + 2204106 x y z + 12180960 x y z + 43067328 x y z 4 13 7 5 12 7 6 11 7 + 109343124 x y z + 213291732 x y z + 336125088 x y z 7 10 7 8 9 7 9 8 7 + 444976224 x y z + 508389300 x y z + 508389300 x y z 10 7 7 11 6 7 12 5 7 + 444976224 x y z + 336125088 x y z + 213291732 x y z 13 4 7 14 3 7 15 2 7 + 109343124 x y z + 43067328 x y z + 12180960 x y z 16 7 17 7 18 6 17 6 + 2204106 x y z + 192378 x z + 112274 y z + 1292214 x y z 2 16 6 3 15 6 4 14 6 + 7245828 x y z + 26249216 x y z + 69105684 x y z 5 13 6 6 12 6 7 11 6 + 141612660 x y z + 237121720 x y z + 336125088 x y z 8 10 6 9 9 6 10 8 6 + 412029810 x y z + 440670228 x y z + 412029810 x y z 11 7 6 12 6 6 13 5 6 + 336125088 x y z + 237121720 x y z + 141612660 x y z 14 4 6 15 3 6 16 2 6 + 69105684 x y z + 26249216 x y z + 7245828 x y z 17 6 18 6 19 5 18 5 + 1292214 x y z + 112274 x z + 57300 y z + 659280 x y z 2 17 5 3 16 5 4 15 5 + 3730446 x y z + 13777314 x y z + 37415544 x y z 5 14 5 6 13 5 7 12 5 + 80103672 x y z + 141612660 x y z + 213291732 x y z 8 11 5 9 10 5 10 9 5 + 278729658 x y z + 318383274 x y z + 318383274 x y z 11 8 5 12 7 5 13 6 5 + 278729658 x y z + 213291732 x y z + 141612660 x y z 14 5 5 15 4 5 16 3 5 + 80103672 x y z + 37415544 x y z + 13777314 x y z 17 2 5 18 5 19 5 20 4 + 3730446 x y z + 659280 x y z + 57300 x z + 24756 y z 19 4 2 18 4 3 17 4 4 16 4 + 284172 x y z + 1616298 x y z + 6058482 x y z + 16871088 x y z 5 15 4 6 14 4 7 13 4 + 37415544 x y z + 69105684 x y z + 109343124 x y z 8 12 4 9 11 4 10 10 4 + 150662016 x y z + 182252154 x y z + 194147076 x y z 11 9 4 12 8 4 13 7 4 + 182252154 x y z + 150662016 x y z + 109343124 x y z 14 6 4 15 5 4 16 4 4 + 69105684 x y z + 37415544 x y z + 16871088 x y z 17 3 4 18 2 4 19 4 20 4 + 6058482 x y z + 1616298 x y z + 284172 x y z + 24756 x z 21 3 20 3 2 19 3 3 18 3 + 8620 y z + 98868 x y z + 564096 x y z + 2136536 x y z 4 17 3 5 16 3 6 15 3 + 6058482 x y z + 13777314 x y z + 26249216 x y z 7 14 3 8 13 3 9 12 3 + 43067328 x y z + 61843542 x y z + 78425718 x y z 10 11 3 11 10 3 12 9 3 + 88233480 x y z + 88233480 x y z + 78425718 x y z 13 8 3 14 7 3 15 6 3 + 61843542 x y z + 43067328 x y z + 26249216 x y z 16 5 3 17 4 3 18 3 3 + 13777314 x y z + 6058482 x y z + 2136536 x y z 19 2 3 20 3 21 3 22 2 + 564096 x y z + 98868 x y z + 8620 x z + 2244 y z 21 2 2 20 2 3 19 2 4 18 2 + 25860 x y z + 148032 x y z + 564096 x y z + 1616298 x y z 5 17 2 6 16 2 7 15 2 + 3730446 x y z + 7245828 x y z + 12180960 x y z 8 14 2 9 13 2 10 12 2 + 18029430 x y z + 23731710 x y z + 27935076 x y z 11 11 2 12 10 2 13 9 2 + 29487672 x y z + 27935076 x y z + 23731710 x y z 14 8 2 15 7 2 16 6 2 + 18029430 x y z + 12180960 x y z + 7245828 x y z 17 5 2 18 4 2 19 3 2 20 2 2 + 3730446 x y z + 1616298 x y z + 564096 x y z + 148032 x y z 21 2 22 2 23 22 2 21 + 25860 x y z + 2244 x z + 384 y z + 4488 x y z + 25860 x y z 3 20 4 19 5 18 6 17 + 98868 x y z + 284172 x y z + 659280 x y z + 1292214 x y z 7 16 8 15 9 14 10 13 + 2204106 x y z + 3331476 x y z + 4509420 x y z + 5500566 x y z 11 12 12 11 13 10 14 9 + 6069438 x y z + 6069438 x y z + 5500566 x y z + 4509420 x y z 15 8 16 7 17 6 18 5 + 3331476 x y z + 2204106 x y z + 1292214 x y z + 659280 x y z 19 4 20 3 21 2 22 23 + 284172 x y z + 98868 x y z + 25860 x y z + 4488 x y z + 384 x z 24 23 2 22 3 21 4 20 5 19 + 32 y + 384 x y + 2244 x y + 8620 x y + 24756 x y + 57300 x y 6 18 7 17 8 16 9 15 + 112274 x y + 192378 x y + 294144 x y + 405908 x y 10 14 11 13 12 12 13 11 + 508830 x y + 581742 x y + 608136 x y + 581742 x y 14 10 15 9 16 8 17 7 + 508830 x y + 405908 x y + 294144 x y + 192378 x y 18 6 19 5 20 4 21 3 22 2 + 112274 x y + 57300 x y + 24756 x y + 8620 x y + 2244 x y 23 24 24 23 23 2 22 + 384 x y + 32 x > 32 z + 384 y z + 384 x z + 2244 y z 22 2 22 3 21 2 21 2 21 + 4488 x y z + 2244 x z + 8620 y z + 25860 x y z + 25860 x y z 3 21 4 20 3 20 2 2 20 + 8620 x z + 24756 y z + 98868 x y z + 148032 x y z 3 20 4 20 5 19 4 19 + 98868 x y z + 24756 x z + 57300 y z + 284172 x y z 2 3 19 3 2 19 4 19 5 19 + 564096 x y z + 564096 x y z + 284172 x y z + 57300 x z 6 18 5 18 2 4 18 3 3 18 + 112078 y z + 658104 x y z + 1613358 x y z + 2136712 x y z 4 2 18 5 18 6 18 7 17 + 1613358 x y z + 658104 x y z + 112078 x z + 190614 y z 6 17 2 5 17 3 4 17 4 3 17 + 1279866 x y z + 3693402 x y z + 6033606 x y z + 6033606 x y z 5 2 17 6 17 7 17 8 16 + 3693402 x y z + 1279866 x y z + 190614 x z + 286647 y z 7 16 2 6 16 3 5 16 + 2144130 x y z + 7035912 x y z + 13504938 x y z 4 4 16 5 3 16 6 2 16 + 16665786 x y z + 13504938 x y z + 7035912 x y z 7 16 8 16 9 15 8 15 + 2144130 x y z + 286647 x z + 385720 y z + 3149784 x y z 2 7 15 3 6 15 4 5 15 + 11454192 x y z + 24913872 x y z + 36149808 x y z 5 4 15 6 3 15 7 2 15 + 36149808 x y z + 24913872 x y z + 11454192 x y z 8 15 9 15 10 14 9 14 + 3149784 x y z + 385720 x z + 470022 y z + 4120164 x y z 2 8 14 3 7 14 4 6 14 + 16276014 x y z + 39030528 x y z + 64169460 x y z 5 5 14 6 4 14 7 3 14 + 75560328 x y z + 64169460 x y z + 39030528 x y z 8 2 14 9 14 10 14 11 13 + 16276014 x y z + 4120164 x y z + 470022 x z + 525294 y z 10 13 2 9 13 3 8 13 + 4870818 x y z + 20564154 x y z + 53261238 x y z 4 7 13 5 6 13 6 5 13 + 96365844 x y z + 128896332 x y z + 128896332 x y z 7 4 13 8 3 13 9 2 13 + 96365844 x y z + 53261238 x y z + 20564154 x y z 10 13 11 13 12 12 11 12 + 4870818 x y z + 525294 x z + 544338 y z + 5273874 x y z 2 10 12 3 9 12 4 8 12 + 23475684 x y z + 64665498 x y z + 125929446 x y z 5 7 12 6 6 12 7 5 12 + 185735772 x y z + 211491672 x y z + 185735772 x y z 8 4 12 9 3 12 10 2 12 + 125929446 x y z + 64665498 x y z + 23475684 x y z 11 12 12 12 13 11 12 11 + 5273874 x y z + 544338 x z + 525294 y z + 5273874 x y z 2 11 11 3 10 11 4 9 11 + 24499080 x y z + 70954728 x y z + 146433390 x y z 5 8 11 6 7 11 7 6 11 + 232551954 x y z + 293106000 x y z + 293106000 x y z 8 5 11 9 4 11 10 3 11 + 232551954 x y z + 146433390 x y z + 70954728 x y z 11 2 11 12 11 13 11 14 10 + 24499080 x y z + 5273874 x y z + 525294 x z + 470022 y z 13 10 2 12 10 3 11 10 + 4870818 x y z + 23475684 x y z + 70954728 x y z 4 10 10 5 9 10 6 8 10 + 153727836 x y z + 258600174 x y z + 352154802 x y z 7 7 10 8 6 10 9 5 10 + 390835968 x y z + 352154802 x y z + 258600174 x y z 10 4 10 11 3 10 12 2 10 + 153727836 x y z + 70954728 x y z + 23475684 x y z 13 10 14 10 15 9 14 9 + 4870818 x y z + 470022 x z + 385720 y z + 4120164 x y z 2 13 9 3 12 9 4 11 9 + 20564154 x y z + 64665498 x y z + 146433390 x y z 5 10 9 6 9 9 7 8 9 + 258600174 x y z + 373537756 x y z + 449239608 x y z 8 7 9 9 6 9 10 5 9 + 449239608 x y z + 373537756 x y z + 258600174 x y z 11 4 9 12 3 9 13 2 9 + 146433390 x y z + 64665498 x y z + 20564154 x y z 14 9 15 9 16 8 15 8 + 4120164 x y z + 385720 x z + 286647 y z + 3149784 x y z 2 14 8 3 13 8 4 12 8 + 16276014 x y z + 53261238 x y z + 125929446 x y z 5 11 8 6 10 8 7 9 8 + 232551954 x y z + 352154802 x y z + 449239608 x y z 8 8 8 9 7 8 10 6 8 + 487124118 x y z + 449239608 x y z + 352154802 x y z 11 5 8 12 4 8 13 3 8 + 232551954 x y z + 125929446 x y z + 53261238 x y z 14 2 8 15 8 16 8 17 7 + 16276014 x y z + 3149784 x y z + 286647 x z + 190614 y z 16 7 2 15 7 3 14 7 + 2144130 x y z + 11454192 x y z + 39030528 x y z 4 13 7 5 12 7 6 11 7 + 96365844 x y z + 185735772 x y z + 293106000 x y z 7 10 7 8 9 7 9 8 7 + 390835968 x y z + 449239608 x y z + 449239608 x y z 10 7 7 11 6 7 12 5 7 + 390835968 x y z + 293106000 x y z + 185735772 x y z 13 4 7 14 3 7 15 2 7 + 96365844 x y z + 39030528 x y z + 11454192 x y z 16 7 17 7 18 6 17 6 + 2144130 x y z + 190614 x z + 112078 y z + 1279866 x y z 2 16 6 3 15 6 4 14 6 + 7035912 x y z + 24913872 x y z + 64169460 x y z 5 13 6 6 12 6 7 11 6 + 128896332 x y z + 211491672 x y z + 293106000 x y z 8 10 6 9 9 6 10 8 6 + 352154802 x y z + 373537756 x y z + 352154802 x y z 11 7 6 12 6 6 13 5 6 + 293106000 x y z + 211491672 x y z + 128896332 x y z 14 4 6 15 3 6 16 2 6 + 64169460 x y z + 24913872 x y z + 7035912 x y z 17 6 18 6 19 5 18 5 + 1279866 x y z + 112078 x z + 57300 y z + 658104 x y z 2 17 5 3 16 5 4 15 5 + 3693402 x y z + 13504938 x y z + 36149808 x y z 5 14 5 6 13 5 7 12 5 + 75560328 x y z + 128896332 x y z + 185735772 x y z 8 11 5 9 10 5 10 9 5 + 232551954 x y z + 258600174 x y z + 258600174 x y z 11 8 5 12 7 5 13 6 5 + 232551954 x y z + 185735772 x y z + 128896332 x y z 14 5 5 15 4 5 16 3 5 + 75560328 x y z + 36149808 x y z + 13504938 x y z 17 2 5 18 5 19 5 20 4 + 3693402 x y z + 658104 x y z + 57300 x z + 24756 y z 19 4 2 18 4 3 17 4 4 16 4 + 284172 x y z + 1613358 x y z + 6033606 x y z + 16665786 x y z 5 15 4 6 14 4 7 13 4 + 36149808 x y z + 64169460 x y z + 96365844 x y z 8 12 4 9 11 4 10 10 4 + 125929446 x y z + 146433390 x y z + 153727836 x y z 11 9 4 12 8 4 13 7 4 + 146433390 x y z + 125929446 x y z + 96365844 x y z 14 6 4 15 5 4 16 4 4 + 64169460 x y z + 36149808 x y z + 16665786 x y z 17 3 4 18 2 4 19 4 20 4 + 6033606 x y z + 1613358 x y z + 284172 x y z + 24756 x z 21 3 20 3 2 19 3 3 18 3 + 8620 y z + 98868 x y z + 564096 x y z + 2136712 x y z 4 17 3 5 16 3 6 15 3 + 6033606 x y z + 13504938 x y z + 24913872 x y z 7 14 3 8 13 3 9 12 3 + 39030528 x y z + 53261238 x y z + 64665498 x y z 10 11 3 11 10 3 12 9 3 + 70954728 x y z + 70954728 x y z + 64665498 x y z 13 8 3 14 7 3 15 6 3 + 53261238 x y z + 39030528 x y z + 24913872 x y z 16 5 3 17 4 3 18 3 3 + 13504938 x y z + 6033606 x y z + 2136712 x y z 19 2 3 20 3 21 3 22 2 + 564096 x y z + 98868 x y z + 8620 x z + 2244 y z 21 2 2 20 2 3 19 2 4 18 2 + 25860 x y z + 148032 x y z + 564096 x y z + 1613358 x y z 5 17 2 6 16 2 7 15 2 + 3693402 x y z + 7035912 x y z + 11454192 x y z 8 14 2 9 13 2 10 12 2 + 16276014 x y z + 20564154 x y z + 23475684 x y z 11 11 2 12 10 2 13 9 2 + 24499080 x y z + 23475684 x y z + 20564154 x y z 14 8 2 15 7 2 16 6 2 + 16276014 x y z + 11454192 x y z + 7035912 x y z 17 5 2 18 4 2 19 3 2 20 2 2 + 3693402 x y z + 1613358 x y z + 564096 x y z + 148032 x y z 21 2 22 2 23 22 2 21 + 25860 x y z + 2244 x z + 384 y z + 4488 x y z + 25860 x y z 3 20 4 19 5 18 6 17 + 98868 x y z + 284172 x y z + 658104 x y z + 1279866 x y z 7 16 8 15 9 14 10 13 + 2144130 x y z + 3149784 x y z + 4120164 x y z + 4870818 x y z 11 12 12 11 13 10 14 9 + 5273874 x y z + 5273874 x y z + 4870818 x y z + 4120164 x y z 15 8 16 7 17 6 18 5 + 3149784 x y z + 2144130 x y z + 1279866 x y z + 658104 x y z 19 4 20 3 21 2 22 23 + 284172 x y z + 98868 x y z + 25860 x y z + 4488 x y z + 384 x z 24 23 2 22 3 21 4 20 5 19 + 32 y + 384 x y + 2244 x y + 8620 x y + 24756 x y + 57300 x y 6 18 7 17 8 16 9 15 + 112078 x y + 190614 x y + 286647 x y + 385720 x y 10 14 11 13 12 12 13 11 + 470022 x y + 525294 x y + 544338 x y + 525294 x y 14 10 15 9 16 8 17 7 + 470022 x y + 385720 x y + 286647 x y + 190614 x y 18 6 19 5 20 4 21 3 22 2 + 112078 x y + 57300 x y + 24756 x y + 8620 x y + 2244 x y 23 24 + 384 x y + 32 x Expanding and collecting terms of the same sign gives: 6 18 5 18 2 4 18 4 2 18 5 18 196 y z + 1176 x y z + 2940 x y z + 2940 x y z + 1176 x y z 6 18 7 17 6 17 2 5 17 + 196 x z + 1764 y z + 12348 x y z + 37044 x y z 3 4 17 4 3 17 5 2 17 6 17 + 24876 x y z + 24876 x y z + 37044 x y z + 12348 x y z 7 17 8 16 7 16 2 6 16 + 1764 x z + 7497 y z + 59976 x y z + 209916 x y z 3 5 16 4 4 16 5 3 16 6 2 16 + 272376 x y z + 205302 x y z + 272376 x y z + 209916 x y z 7 16 8 16 9 15 8 15 + 59976 x y z + 7497 x z + 20188 y z + 181692 x y z 2 7 15 3 6 15 4 5 15 5 4 15 + 726768 x y z + 1335344 x y z + 1265736 x y z + 1265736 x y z 6 3 15 7 2 15 8 15 9 15 + 1335344 x y z + 726768 x y z + 181692 x y z + 20188 x z 10 14 9 14 2 8 14 3 7 14 + 38808 y z + 389256 x y z + 1753416 x y z + 4036800 x y z 4 6 14 5 5 14 6 4 14 + 4936224 x y z + 4543344 x y z + 4936224 x y z 7 3 14 8 2 14 9 14 10 14 + 4036800 x y z + 1753416 x y z + 389256 x y z + 38808 x z 11 13 10 13 2 9 13 3 8 13 + 56448 y z + 629748 x y z + 3167556 x y z + 8582304 x y z 4 7 13 5 6 13 6 5 13 + 12977280 x y z + 12716328 x y z + 12716328 x y z 7 4 13 8 3 13 9 2 13 + 12977280 x y z + 8582304 x y z + 3167556 x y z 10 13 11 13 12 12 11 12 + 629748 x y z + 56448 x z + 63798 y z + 795564 x y z 2 10 12 3 9 12 4 8 12 + 4459392 x y z + 13760220 x y z + 24732570 x y z 5 7 12 6 6 12 7 5 12 + 27555960 x y z + 25630048 x y z + 27555960 x y z 8 4 12 9 3 12 10 2 12 + 24732570 x y z + 13760220 x y z + 4459392 x y z 11 12 12 12 13 11 12 11 + 795564 x y z + 63798 x z + 56448 y z + 795564 x y z 2 11 11 3 10 11 4 9 11 + 4988592 x y z + 17278752 x y z + 35818764 x y z 5 8 11 6 7 11 7 6 11 + 46177704 x y z + 43019088 x y z + 43019088 x y z 8 5 11 9 4 11 10 3 11 + 46177704 x y z + 35818764 x y z + 17278752 x y z 11 2 11 12 11 13 11 14 10 + 4988592 x y z + 795564 x y z + 56448 x z + 38808 y z 13 10 2 12 10 3 11 10 + 629748 x y z + 4459392 x y z + 17278752 x y z 4 10 10 5 9 10 6 8 10 + 40419240 x y z + 59783100 x y z + 59875008 x y z 7 7 10 8 6 10 9 5 10 + 54140256 x y z + 59875008 x y z + 59783100 x y z 10 4 10 11 3 10 12 2 10 + 40419240 x y z + 17278752 x y z + 4459392 x y z 13 10 14 10 15 9 14 9 + 629748 x y z + 38808 x z + 20188 y z + 389256 x y z 2 13 9 3 12 9 4 11 9 + 3167556 x y z + 13760220 x y z + 35818764 x y z 5 10 9 6 9 9 7 8 9 + 59783100 x y z + 67132472 x y z + 59149692 x y z 8 7 9 9 6 9 10 5 9 + 59149692 x y z + 67132472 x y z + 59783100 x y z 11 4 9 12 3 9 13 2 9 + 35818764 x y z + 13760220 x y z + 3167556 x y z 14 9 15 9 16 8 15 8 + 389256 x y z + 20188 x z + 7497 y z + 181692 x y z 2 14 8 3 13 8 4 12 8 + 1753416 x y z + 8582304 x y z + 24732570 x y z 5 11 8 6 10 8 7 9 8 + 46177704 x y z + 59875008 x y z + 59149692 x y z 8 8 8 9 7 8 10 6 8 + 55421226 x y z + 59149692 x y z + 59875008 x y z 11 5 8 12 4 8 13 3 8 + 46177704 x y z + 24732570 x y z + 8582304 x y z 14 2 8 15 8 16 8 17 7 + 1753416 x y z + 181692 x y z + 7497 x z + 1764 y z 16 7 2 15 7 3 14 7 4 13 7 + 59976 x y z + 726768 x y z + 4036800 x y z + 12977280 x y z 5 12 7 6 11 7 7 10 7 + 27555960 x y z + 43019088 x y z + 54140256 x y z 8 9 7 9 8 7 10 7 7 + 59149692 x y z + 59149692 x y z + 54140256 x y z 11 6 7 12 5 7 13 4 7 + 43019088 x y z + 27555960 x y z + 12977280 x y z 14 3 7 15 2 7 16 7 17 7 + 4036800 x y z + 726768 x y z + 59976 x y z + 1764 x z 18 6 17 6 2 16 6 3 15 6 + 196 y z + 12348 x y z + 209916 x y z + 1335344 x y z 4 14 6 5 13 6 6 12 6 + 4936224 x y z + 12716328 x y z + 25630048 x y z 7 11 6 8 10 6 9 9 6 + 43019088 x y z + 59875008 x y z + 67132472 x y z 10 8 6 11 7 6 12 6 6 + 59875008 x y z + 43019088 x y z + 25630048 x y z 13 5 6 14 4 6 15 3 6 + 12716328 x y z + 4936224 x y z + 1335344 x y z 16 2 6 17 6 18 6 18 5 + 209916 x y z + 12348 x y z + 196 x z + 1176 x y z 2 17 5 3 16 5 4 15 5 5 14 5 + 37044 x y z + 272376 x y z + 1265736 x y z + 4543344 x y z 6 13 5 7 12 5 8 11 5 + 12716328 x y z + 27555960 x y z + 46177704 x y z 9 10 5 10 9 5 11 8 5 + 59783100 x y z + 59783100 x y z + 46177704 x y z 12 7 5 13 6 5 14 5 5 + 27555960 x y z + 12716328 x y z + 4543344 x y z 15 4 5 16 3 5 17 2 5 18 5 + 1265736 x y z + 272376 x y z + 37044 x y z + 1176 x y z 2 18 4 3 17 4 4 16 4 5 15 4 + 2940 x y z + 24876 x y z + 205302 x y z + 1265736 x y z 6 14 4 7 13 4 8 12 4 + 4936224 x y z + 12977280 x y z + 24732570 x y z 9 11 4 10 10 4 11 9 4 + 35818764 x y z + 40419240 x y z + 35818764 x y z 12 8 4 13 7 4 14 6 4 + 24732570 x y z + 12977280 x y z + 4936224 x y z 15 5 4 16 4 4 17 3 4 18 2 4 + 1265736 x y z + 205302 x y z + 24876 x y z + 2940 x y z 4 17 3 5 16 3 6 15 3 7 14 3 + 24876 x y z + 272376 x y z + 1335344 x y z + 4036800 x y z 8 13 3 9 12 3 10 11 3 + 8582304 x y z + 13760220 x y z + 17278752 x y z 11 10 3 12 9 3 13 8 3 + 17278752 x y z + 13760220 x y z + 8582304 x y z 14 7 3 15 6 3 16 5 3 17 4 3 + 4036800 x y z + 1335344 x y z + 272376 x y z + 24876 x y z 4 18 2 5 17 2 6 16 2 7 15 2 + 2940 x y z + 37044 x y z + 209916 x y z + 726768 x y z 8 14 2 9 13 2 10 12 2 + 1753416 x y z + 3167556 x y z + 4459392 x y z 11 11 2 12 10 2 13 9 2 + 4988592 x y z + 4459392 x y z + 3167556 x y z 14 8 2 15 7 2 16 6 2 17 5 2 + 1753416 x y z + 726768 x y z + 209916 x y z + 37044 x y z 18 4 2 5 18 6 17 7 16 + 2940 x y z + 1176 x y z + 12348 x y z + 59976 x y z 8 15 9 14 10 13 11 12 + 181692 x y z + 389256 x y z + 629748 x y z + 795564 x y z 12 11 13 10 14 9 15 8 + 795564 x y z + 629748 x y z + 389256 x y z + 181692 x y z 16 7 17 6 18 5 6 18 7 17 + 59976 x y z + 12348 x y z + 1176 x y z + 196 x y + 1764 x y 8 16 9 15 10 14 11 13 12 12 + 7497 x y + 20188 x y + 38808 x y + 56448 x y + 63798 x y 13 11 14 10 15 9 16 8 17 7 + 56448 x y + 38808 x y + 20188 x y + 7497 x y + 1764 x y 18 6 3 3 18 3 18 3 18 3 3 + 196 x y > 176 x y z + 176 x y z + 176 x y z Expressing in terms of symmetric polynomials gives: 196 {18, 6, 0} + 1176 {18, 5, 1} + 2940 {18, 4, 2} + 1764 {17, 7, 0} + 12348 {17, 6, 1} + 37044 {17, 5, 2} + 24876 {17, 4, 3} + 7497 {16, 8, 0} + 59976 {16, 7, 1} + 209916 {16, 6, 2} + 272376 {16, 5, 3} + 102651 {16, 4, 4} + 20188 {15, 9, 0} + 181692 {15, 8, 1} + 726768 {15, 7, 2} + 1335344 {15, 6, 3} + 1265736 {15, 5, 4} + 38808 {14, 10, 0} + 389256 {14, 9, 1} + 1753416 {14, 8, 2} + 4036800 {14, 7, 3} + 4936224 {14, 6, 4} + 2271672 {14, 5, 5} + 56448 {13, 11, 0} + 629748 {13, 10, 1} + 3167556 {13, 9, 2} + 8582304 {13, 8, 3} + 12977280 {13, 7, 4} + 12716328 {13, 6, 5} + 31899 {12, 12, 0} + 795564 {12, 11, 1} + 4459392 {12, 10, 2} + 13760220 {12, 9, 3} + 24732570 {12, 8, 4} + 27555960 {12, 7, 5} + 12815024 {12, 6, 6} + 2494296 {11, 11, 2} + 17278752 {11, 10, 3} + 35818764 {11, 9, 4} + 46177704 {11, 8, 5} + 43019088 {11, 7, 6} + 20209620 {10, 10, 4} + 59783100 {10, 9, 5} + 59875008 {10, 8, 6} + 27070128 {10, 7, 7} + 33566236 {9, 9, 6} + 59149692 {9, 8, 7} + 9236871 {8, 8, 8} > 88 {18, 3, 3} This follows from the following majorizations: 88 {18, 4, 2} >= 88 {18, 3, 3} (d6) true (c7) /* 6.7 */ trineq(csum(a^2/(h(b)^2+h(c)^2))>=2); 2 2 2 c a b To prove: ----------- + ----------- + ----------- >= 2 2 2 2 2 2 2 4 K 4 K 4 K 4 K 4 K 4 K ---- + ---- ---- + ---- ---- + ---- 2 2 2 2 2 2 b a c b c a 2 2 2 2 2 2 2 Multiplying both sides by 4 K (b + a ) (c + a ) (c + b ) gives: 2 2 6 2 4 4 4 2 4 2 6 2 4 4 2 6 2 2 a b c + 3 a b c + 3 a b c + a b c + 3 a b c + a b c >= 2 2 4 2 2 4 2 4 2 2 2 2 2 2 4 2 2 2 4 8 K b c + 8 K a c + 8 K b c + 16 K a b c + 8 K a c + 8 K a b 2 4 2 + 8 K a b Replacing K^2 by F^2 gives: 2 2 6 2 4 4 2 4 2 6 4 4 6 2 2 a b c + (3 a b + 3 a b ) c + (a b + 3 a b + a b ) c >= 2 2 2 2 4 2 4 2 2 2 2 4 2 2 2 4 (8 F b + 8 F a ) c + (8 F b + 16 F a b + 8 F a ) c + 8 F a b 2 4 2 + 8 F a b Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 6 2 4 4 2 4 2 6 4 4 6 2 2 a b c + (3 a b + 3 a b ) c + (a b + 3 a b + a b ) c >= 2 2 8 4 2 2 4 6 6 2 4 4 2 6 4 - ((b + a ) c + (- b - 2 a b - a ) c + (- b - 6 a b - 6 a b - a ) c 8 2 6 4 4 6 2 8 2 2 8 4 6 6 4 8 2 + (b - 2 a b - 6 a b - 2 a b + a ) c + a b - a b - a b + a b ) /2 Multiplying both sides by 2 gives: 2 2 6 2 4 4 4 2 4 2 6 2 4 4 2 6 2 2 2 a b c + 6 a b c + 6 a b c + 2 a b c + 6 a b c + 2 a b c >= 2 8 2 8 4 6 2 2 6 4 6 6 4 2 4 4 4 2 4 - b c - a c + b c + 2 a b c + a c + b c + 6 a b c + 6 a b c 6 4 8 2 2 6 2 4 4 2 6 2 2 8 2 2 8 4 6 + a c - b c + 2 a b c + 6 a b c + 2 a b c - a c - a b + a b 6 4 8 2 + a b - a b Expanding and collecting terms of the same sign gives: 2 8 2 8 8 2 8 2 2 8 8 2 b c + a c + b c + a c + a b + a b >= 4 6 4 6 6 4 6 4 4 6 6 4 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: 10 9 2 2 8 (2 z + (10 y + 10 x) z + (31 y + 36 x y + 31 x ) z 3 2 2 3 7 + (64 y + 88 x y + 88 x y + 64 x ) z 4 3 2 2 3 4 6 + (98 y + 168 x y + 112 x y + 168 x y + 98 x ) z 5 4 2 3 3 2 4 5 5 + (112 y + 252 x y + 112 x y + 112 x y + 252 x y + 112 x ) z 6 5 2 4 4 2 5 6 4 + (98 y + 252 x y + 140 x y + 140 x y + 252 x y + 98 x ) z 7 6 2 5 5 2 6 7 3 + (64 y + 168 x y + 112 x y + 112 x y + 168 x y + 64 x ) z 8 7 2 6 3 5 4 4 5 3 6 2 + (31 y + 88 x y + 112 x y + 112 x y + 140 x y + 112 x y + 112 x y 7 8 2 9 8 2 7 3 6 4 5 + 88 x y + 31 x ) z + (10 y + 36 x y + 88 x y + 168 x y + 252 x y 5 4 6 3 7 2 8 9 10 9 + 252 x y + 168 x y + 88 x y + 36 x y + 10 x ) z + 2 y + 10 x y 2 8 3 7 4 6 5 5 6 4 7 3 8 2 + 31 x y + 64 x y + 98 x y + 112 x y + 98 x y + 64 x y + 31 x y 9 10 10 9 + 10 x y + 2 x )/1024 >= (2 z + (10 y + 10 x) z 2 2 8 3 2 2 3 7 + (21 y + 48 x y + 21 x ) z + (24 y + 96 x y + 96 x y + 24 x ) z 4 3 2 2 3 4 6 + (18 y + 112 x y + 192 x y + 112 x y + 18 x ) z 5 4 2 3 3 2 4 5 5 + (12 y + 96 x y + 240 x y + 240 x y + 96 x y + 12 x ) z 6 5 2 4 3 3 4 2 5 6 4 + (18 y + 96 x y + 240 x y + 320 x y + 240 x y + 96 x y + 18 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (24 y + 112 x y + 240 x y + 320 x y + 320 x y + 240 x y + 112 x y 7 3 8 7 2 6 3 5 4 4 5 3 + 24 x ) z + (21 y + 96 x y + 192 x y + 240 x y + 240 x y + 240 x y 6 2 7 8 2 9 8 2 7 3 6 + 192 x y + 96 x y + 21 x ) z + (10 y + 48 x y + 96 x y + 112 x y 4 5 5 4 6 3 7 2 8 9 10 + 96 x y + 96 x y + 112 x y + 96 x y + 48 x y + 10 x ) z + 2 y 9 2 8 3 7 4 6 5 5 6 4 7 3 + 10 x y + 21 x y + 24 x y + 18 x y + 12 x y + 18 x y + 24 x y 8 2 9 10 + 21 x y + 10 x y + 2 x )/1024 Multiplying both sides by 1024 gives: 10 9 9 2 8 8 2 8 3 7 2 z + 10 y z + 10 x z + 31 y z + 36 x y z + 31 x z + 64 y z 2 7 2 7 3 7 4 6 3 6 2 2 6 + 88 x y z + 88 x y z + 64 x z + 98 y z + 168 x y z + 112 x y z 3 6 4 6 5 5 4 5 2 3 5 + 168 x y z + 98 x z + 112 y z + 252 x y z + 112 x y z 3 2 5 4 5 5 5 6 4 5 4 + 112 x y z + 252 x y z + 112 x z + 98 y z + 252 x y z 2 4 4 4 2 4 5 4 6 4 7 3 + 140 x y z + 140 x y z + 252 x y z + 98 x z + 64 y z 6 3 2 5 3 5 2 3 6 3 7 3 + 168 x y z + 112 x y z + 112 x y z + 168 x y z + 64 x z 8 2 7 2 2 6 2 3 5 2 4 4 2 + 31 y z + 88 x y z + 112 x y z + 112 x y z + 140 x y z 5 3 2 6 2 2 7 2 8 2 9 8 + 112 x y z + 112 x y z + 88 x y z + 31 x z + 10 y z + 36 x y z 2 7 3 6 4 5 5 4 6 3 + 88 x y z + 168 x y z + 252 x y z + 252 x y z + 168 x y z 7 2 8 9 10 9 2 8 3 7 + 88 x y z + 36 x y z + 10 x z + 2 y + 10 x y + 31 x y + 64 x y 4 6 5 5 6 4 7 3 8 2 9 10 + 98 x y + 112 x y + 98 x y + 64 x y + 31 x y + 10 x y + 2 x >= 10 9 9 2 8 8 2 8 3 7 2 z + 10 y z + 10 x z + 21 y z + 48 x y z + 21 x z + 24 y z 2 7 2 7 3 7 4 6 3 6 2 2 6 + 96 x y z + 96 x y z + 24 x z + 18 y z + 112 x y z + 192 x y z 3 6 4 6 5 5 4 5 2 3 5 3 2 5 + 112 x y z + 18 x z + 12 y z + 96 x y z + 240 x y z + 240 x y z 4 5 5 5 6 4 5 4 2 4 4 3 3 4 + 96 x y z + 12 x z + 18 y z + 96 x y z + 240 x y z + 320 x y z 4 2 4 5 4 6 4 7 3 6 3 2 5 3 + 240 x y z + 96 x y z + 18 x z + 24 y z + 112 x y z + 240 x y z 3 4 3 4 3 3 5 2 3 6 3 7 3 + 320 x y z + 320 x y z + 240 x y z + 112 x y z + 24 x z 8 2 7 2 2 6 2 3 5 2 4 4 2 + 21 y z + 96 x y z + 192 x y z + 240 x y z + 240 x y z 5 3 2 6 2 2 7 2 8 2 9 8 + 240 x y z + 192 x y z + 96 x y z + 21 x z + 10 y z + 48 x y z 2 7 3 6 4 5 5 4 6 3 + 96 x y z + 112 x y z + 96 x y z + 96 x y z + 112 x y z 7 2 8 9 10 9 2 8 3 7 + 96 x y z + 48 x y z + 10 x z + 2 y + 10 x y + 21 x y + 24 x y 4 6 5 5 6 4 7 3 8 2 9 10 + 18 x y + 12 x y + 18 x y + 24 x y + 21 x y + 10 x y + 2 x Expanding and collecting terms of the same sign gives: 2 8 2 8 3 7 3 7 4 6 3 6 3 6 10 y z + 10 x z + 40 y z + 40 x z + 80 y z + 56 x y z + 56 x y z 4 6 5 5 4 5 4 5 5 5 6 4 + 80 x z + 100 y z + 156 x y z + 156 x y z + 100 x z + 80 y z 5 4 5 4 6 4 7 3 6 3 6 3 + 156 x y z + 156 x y z + 80 x z + 40 y z + 56 x y z + 56 x y z 7 3 8 2 8 2 3 6 4 5 5 4 + 40 x z + 10 y z + 10 x z + 56 x y z + 156 x y z + 156 x y z 6 3 2 8 3 7 4 6 5 5 6 4 + 56 x y z + 10 x y + 40 x y + 80 x y + 100 x y + 80 x y 7 3 8 2 8 2 7 2 7 2 2 6 + 40 x y + 10 x y >= 12 x y z + 8 x y z + 8 x y z + 80 x y z 2 3 5 3 2 5 2 4 4 3 3 4 4 2 4 + 128 x y z + 128 x y z + 100 x y z + 320 x y z + 100 x y z 2 5 3 3 4 3 4 3 3 5 2 3 7 2 + 128 x y z + 320 x y z + 320 x y z + 128 x y z + 8 x y z 2 6 2 3 5 2 4 4 2 5 3 2 6 2 2 + 80 x y z + 128 x y z + 100 x y z + 128 x y z + 80 x y z 7 2 8 2 7 7 2 8 + 8 x y z + 12 x y z + 8 x y z + 8 x y z + 12 x y z Dividing both sides by 2 gives: 2 8 2 8 3 7 3 7 4 6 3 6 3 6 5 y z + 5 x z + 20 y z + 20 x z + 40 y z + 28 x y z + 28 x y z 4 6 5 5 4 5 4 5 5 5 6 4 + 40 x z + 50 y z + 78 x y z + 78 x y z + 50 x z + 40 y z 5 4 5 4 6 4 7 3 6 3 6 3 + 78 x y z + 78 x y z + 40 x z + 20 y z + 28 x y z + 28 x y z 7 3 8 2 8 2 3 6 4 5 5 4 + 20 x z + 5 y z + 5 x z + 28 x y z + 78 x y z + 78 x y z 6 3 2 8 3 7 4 6 5 5 6 4 7 3 + 28 x y z + 5 x y + 20 x y + 40 x y + 50 x y + 40 x y + 20 x y 8 2 8 2 7 2 7 2 2 6 2 3 5 + 5 x y >= 6 x y z + 4 x y z + 4 x y z + 40 x y z + 64 x y z 3 2 5 2 4 4 3 3 4 4 2 4 2 5 3 + 64 x y z + 50 x y z + 160 x y z + 50 x y z + 64 x y z 3 4 3 4 3 3 5 2 3 7 2 2 6 2 + 160 x y z + 160 x y z + 64 x y z + 4 x y z + 40 x y z 3 5 2 4 4 2 5 3 2 6 2 2 7 2 8 + 64 x y z + 50 x y z + 64 x y z + 40 x y z + 4 x y z + 6 x y z 2 7 7 2 8 + 4 x y z + 4 x y z + 6 x y z Expressing in terms of symmetric polynomials gives: 5 {8, 2, 0} + 20 {7, 3, 0} + 40 {6, 4, 0} + 28 {6, 3, 1} + 25 {5, 5, 0} + 78 {5, 4, 1} >= 3 {8, 1, 1} + 4 {7, 2, 1} + 20 {6, 2, 2} + 64 {5, 3, 2} + 25 {4, 4, 2} + 80 {4, 3, 3} This follows from the following majorizations: 3 {8, 2, 0} >= 3 {8, 1, 1} left side: [78 {5, 4, 1}, 25 {5, 5, 0}, 28 {6, 3, 1}, 40 {6, 4, 0}, 20 {7, 3, 0}, 5 {8, 2, 0}] right side: [80 {4, 3, 3}, 25 {4, 4, 2}, 64 {5, 3, 2}, 20 {6, 2, 2}, 4 {7, 2, 1}, 3 {8, 1, 1}] (d7) notsure (c8) /* 6.8 */ trineq(csum(h(a))>=9*r); 2 K 2 K 2 K To prove: --- + --- + --- >= 9 r c b a Let r = K/s . We get: (2 K b + 2 K a) c + 2 K a b 9 K --------------------------- >= --- a b c s Multiplying both sides by a b c s gives: 2 K b c s + 2 K a c s + 2 K a b s >= 9 K a b c left side: [{2, 1, 0}] right side: [{3, 0, 0}] Bringing all terms involving K to the left side yields: K ((2 b + 2 a) c + 2 a b) s - 9 K a b c >= 0 Since ((2 b + 2 a) c + 2 a b) s - 9 a b c is positive, and since 0 is positive, we can square both sides to get: 2 2 2 2 2 2 2 6 ((4 b + 8 a b + 4 a ) c + (8 a b + 8 a b) c + 4 a b ) s 2 2 3 3 2 2 3 2 + ((- 4 b - 8 a b - 4 a ) c + (- 4 b - 56 a b - 56 a b - 4 a ) c 3 2 2 3 2 3 3 2 5 + (- 8 a b - 56 a b - 8 a b) c - 4 a b - 4 a b ) s 3 2 2 3 3 3 2 2 3 2 + ((4 b + 48 a b + 48 a b + 4 a ) c + (48 a b + 213 a b + 48 a b) c 2 3 3 2 3 3 4 + (48 a b + 48 a b ) c + 4 a b ) s 3 2 2 3 3 2 3 3 2 2 + ((- 40 a b - 161 a b - 40 a b) c + (- 161 a b - 161 a b ) c 3 3 3 2 3 3 2 3 3 3 2 2 - 40 a b c) s + ((117 a b + 117 a b ) c + 117 a b c ) s 3 3 3 - 81 a b c s >= 0 Expanding and collecting terms of the same sign gives: 2 2 6 2 6 2 2 6 2 6 2 6 2 2 6 4 b c s + 8 a b c s + 4 a c s + 8 a b c s + 8 a b c s + 4 a b s 3 3 4 2 3 4 2 3 4 3 3 4 3 2 4 + 4 b c s + 48 a b c s + 48 a b c s + 4 a c s + 48 a b c s 2 2 2 4 3 2 4 2 3 4 3 2 4 3 3 4 + 213 a b c s + 48 a b c s + 48 a b c s + 48 a b c s + 4 a b s 2 3 3 2 3 2 3 2 3 3 2 2 + 117 a b c s + 117 a b c s + 117 a b c s >= 2 3 5 3 5 2 3 5 3 2 5 2 2 5 4 b c s + 8 a b c s + 4 a c s + 4 b c s + 56 a b c s 2 2 5 3 2 5 3 5 2 2 5 3 5 + 56 a b c s + 4 a c s + 8 a b c s + 56 a b c s + 8 a b c s 2 3 5 3 2 5 3 3 3 2 2 3 3 3 3 3 + 4 a b s + 4 a b s + 40 a b c s + 161 a b c s + 40 a b c s 2 3 2 3 3 2 2 3 3 3 3 3 3 3 + 161 a b c s + 161 a b c s + 40 a b c s + 81 a b c s Dividing both sides by s gives: 2 2 5 2 5 2 2 5 2 5 2 5 2 2 5 4 b c s + 8 a b c s + 4 a c s + 8 a b c s + 8 a b c s + 4 a b s 3 3 3 2 3 3 2 3 3 3 3 3 3 2 3 + 4 b c s + 48 a b c s + 48 a b c s + 4 a c s + 48 a b c s 2 2 2 3 3 2 3 2 3 3 3 2 3 3 3 3 + 213 a b c s + 48 a b c s + 48 a b c s + 48 a b c s + 4 a b s 2 3 3 3 2 3 3 3 2 + 117 a b c s + 117 a b c s + 117 a b c s >= 2 3 4 3 4 2 3 4 3 2 4 2 2 4 4 b c s + 8 a b c s + 4 a c s + 4 b c s + 56 a b c s 2 2 4 3 2 4 3 4 2 2 4 3 4 + 56 a b c s + 4 a c s + 8 a b c s + 56 a b c s + 8 a b c s 2 3 4 3 2 4 3 3 2 2 2 3 2 3 3 2 + 4 a b s + 4 a b s + 40 a b c s + 161 a b c s + 40 a b c s 2 3 2 2 3 2 2 2 3 3 2 3 3 3 + 161 a b c s + 161 a b c s + 40 a b c s + 81 a b c Let s = (c+b+a)/2 . We get: 2 2 7 3 2 2 3 6 ((b + 2 a b + a ) c + (9 b + 65 a b + 65 a b + 9 a ) c 4 3 2 2 3 4 5 + (22 b + 254 a b + 582 a b + 254 a b + 22 a ) c 5 4 2 3 3 2 4 5 4 + (22 b + 382 a b + 1908 a b + 1908 a b + 382 a b + 22 a ) c 6 5 2 4 3 3 4 2 5 6 + (9 b + 254 a b + 1908 a b + 3798 a b + 1908 a b + 254 a b + 9 a ) 3 7 6 2 5 3 4 4 3 5 2 6 c + (b + 65 a b + 582 a b + 1908 a b + 1908 a b + 582 a b + 65 a b 7 2 7 2 6 3 5 4 4 5 3 6 2 + a ) c + (2 a b + 65 a b + 254 a b + 382 a b + 254 a b + 65 a b 7 2 7 3 6 4 5 5 4 6 3 7 2 + 2 a b) c + a b + 9 a b + 22 a b + 22 a b + 9 a b + a b )/8 >= 2 2 7 3 2 2 3 6 ((b + 2 a b + a ) c + (5 b + 26 a b + 26 a b + 5 a ) c 4 3 2 2 3 4 5 + (10 b + 126 a b + 323 a b + 126 a b + 10 a ) c 5 4 2 3 3 2 4 5 4 + (10 b + 204 a b + 926 a b + 926 a b + 204 a b + 10 a ) c 6 5 2 4 3 3 4 2 5 6 3 + (5 b + 126 a b + 926 a b + 1974 a b + 926 a b + 126 a b + 5 a ) c 7 6 2 5 3 4 4 3 5 2 6 + (b + 26 a b + 323 a b + 926 a b + 926 a b + 323 a b + 26 a b 7 2 7 2 6 3 5 4 4 5 3 6 2 + a ) c + (2 a b + 26 a b + 126 a b + 204 a b + 126 a b + 26 a b 7 2 7 3 6 4 5 5 4 6 3 7 2 + 2 a b) c + a b + 5 a b + 10 a b + 10 a b + 5 a b + a b )/4 Multiplying both sides by 8 gives: 2 7 7 2 7 3 6 2 6 2 6 3 6 b c + 2 a b c + a c + 9 b c + 65 a b c + 65 a b c + 9 a c 4 5 3 5 2 2 5 3 5 4 5 5 4 + 22 b c + 254 a b c + 582 a b c + 254 a b c + 22 a c + 22 b c 4 4 2 3 4 3 2 4 4 4 5 4 + 382 a b c + 1908 a b c + 1908 a b c + 382 a b c + 22 a c 6 3 5 3 2 4 3 3 3 3 4 2 3 + 9 b c + 254 a b c + 1908 a b c + 3798 a b c + 1908 a b c 5 3 6 3 7 2 6 2 2 5 2 3 4 2 + 254 a b c + 9 a c + b c + 65 a b c + 582 a b c + 1908 a b c 4 3 2 5 2 2 6 2 7 2 7 2 6 + 1908 a b c + 582 a b c + 65 a b c + a c + 2 a b c + 65 a b c 3 5 4 4 5 3 6 2 7 2 7 + 254 a b c + 382 a b c + 254 a b c + 65 a b c + 2 a b c + a b 3 6 4 5 5 4 6 3 7 2 + 9 a b + 22 a b + 22 a b + 9 a b + a b >= 2 7 7 2 7 3 6 2 6 2 6 3 6 2 b c + 4 a b c + 2 a c + 10 b c + 52 a b c + 52 a b c + 10 a c 4 5 3 5 2 2 5 3 5 4 5 5 4 + 20 b c + 252 a b c + 646 a b c + 252 a b c + 20 a c + 20 b c 4 4 2 3 4 3 2 4 4 4 5 4 + 408 a b c + 1852 a b c + 1852 a b c + 408 a b c + 20 a c 6 3 5 3 2 4 3 3 3 3 4 2 3 + 10 b c + 252 a b c + 1852 a b c + 3948 a b c + 1852 a b c 5 3 6 3 7 2 6 2 2 5 2 3 4 2 + 252 a b c + 10 a c + 2 b c + 52 a b c + 646 a b c + 1852 a b c 4 3 2 5 2 2 6 2 7 2 7 2 6 + 1852 a b c + 646 a b c + 52 a b c + 2 a c + 4 a b c + 52 a b c 3 5 4 4 5 3 6 2 7 2 7 + 252 a b c + 408 a b c + 252 a b c + 52 a b c + 4 a b c + 2 a b 3 6 4 5 5 4 6 3 7 2 + 10 a b + 20 a b + 20 a b + 10 a b + 2 a b Expanding and collecting terms of the same sign gives: 2 6 2 6 4 5 3 5 3 5 4 5 5 4 13 a b c + 13 a b c + 2 b c + 2 a b c + 2 a b c + 2 a c + 2 b c 2 3 4 3 2 4 5 4 5 3 2 4 3 4 2 3 + 56 a b c + 56 a b c + 2 a c + 2 a b c + 56 a b c + 56 a b c 5 3 6 2 3 4 2 4 3 2 6 2 2 6 + 2 a b c + 13 a b c + 56 a b c + 56 a b c + 13 a b c + 13 a b c 3 5 5 3 6 2 4 5 5 4 + 2 a b c + 2 a b c + 13 a b c + 2 a b + 2 a b >= 2 7 7 2 7 3 6 3 6 2 2 5 4 4 b c + 2 a b c + a c + b c + a c + 64 a b c + 26 a b c 4 4 6 3 3 3 3 6 3 7 2 2 5 2 + 26 a b c + b c + 150 a b c + a c + b c + 64 a b c 5 2 2 7 2 7 4 4 7 2 7 3 6 + 64 a b c + a c + 2 a b c + 26 a b c + 2 a b c + a b + a b 6 3 7 2 + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 9 8 2 2 7 (4 z + (48 y + 48 x) z + (290 y + 596 x y + 290 x ) z 3 2 2 3 6 + (861 y + 2543 x y + 2543 x y + 861 x ) z 4 3 2 2 3 4 5 + (1457 y + 5714 x y + 8538 x y + 5714 x y + 1457 x ) z 5 4 2 3 3 2 4 5 4 + (1457 y + 7442 x y + 14841 x y + 14841 x y + 7442 x y + 1457 x ) z 6 5 2 4 3 3 4 2 5 + (861 y + 5714 x y + 14841 x y + 19992 x y + 14841 x y + 5714 x y 6 3 7 6 2 5 3 4 4 3 + 861 x ) z + (290 y + 2543 x y + 8538 x y + 14841 x y + 14841 x y 5 2 6 7 2 8 7 2 6 + 8538 x y + 2543 x y + 290 x ) z + (48 y + 596 x y + 2543 x y 3 5 4 4 5 3 6 2 7 8 + 5714 x y + 7442 x y + 5714 x y + 2543 x y + 596 x y + 48 x ) z 9 8 2 7 3 6 4 5 5 4 6 3 + 4 y + 48 x y + 290 x y + 861 x y + 1457 x y + 1457 x y + 861 x y 7 2 8 9 9 8 + 290 x y + 48 x y + 4 x )/512 >= (4 z + (48 y + 48 x) z 2 2 7 3 2 2 3 + (290 y + 564 x y + 290 x ) z + (861 y + 2575 x y + 2575 x y + 861 x ) 6 4 3 2 2 3 4 5 z + (1457 y + 5738 x y + 8522 x y + 5738 x y + 1457 x ) z 5 4 2 3 3 2 4 5 4 + (1457 y + 7362 x y + 14857 x y + 14857 x y + 7362 x y + 1457 x ) z 6 5 2 4 3 3 4 2 5 + (861 y + 5738 x y + 14857 x y + 19944 x y + 14857 x y + 5738 x y 6 3 7 6 2 5 3 4 4 3 + 861 x ) z + (290 y + 2575 x y + 8522 x y + 14857 x y + 14857 x y 5 2 6 7 2 8 7 2 6 + 8522 x y + 2575 x y + 290 x ) z + (48 y + 564 x y + 2575 x y 3 5 4 4 5 3 6 2 7 8 + 5738 x y + 7362 x y + 5738 x y + 2575 x y + 564 x y + 48 x ) z 9 8 2 7 3 6 4 5 5 4 6 3 + 4 y + 48 x y + 290 x y + 861 x y + 1457 x y + 1457 x y + 861 x y 7 2 8 9 + 290 x y + 48 x y + 4 x )/512 Multiplying both sides by 512 gives: 9 8 8 2 7 7 2 7 3 6 4 z + 48 y z + 48 x z + 290 y z + 596 x y z + 290 x z + 861 y z 2 6 2 6 3 6 4 5 3 5 + 2543 x y z + 2543 x y z + 861 x z + 1457 y z + 5714 x y z 2 2 5 3 5 4 5 5 4 4 4 + 8538 x y z + 5714 x y z + 1457 x z + 1457 y z + 7442 x y z 2 3 4 3 2 4 4 4 5 4 6 3 + 14841 x y z + 14841 x y z + 7442 x y z + 1457 x z + 861 y z 5 3 2 4 3 3 3 3 4 2 3 + 5714 x y z + 14841 x y z + 19992 x y z + 14841 x y z 5 3 6 3 7 2 6 2 2 5 2 + 5714 x y z + 861 x z + 290 y z + 2543 x y z + 8538 x y z 3 4 2 4 3 2 5 2 2 6 2 7 2 + 14841 x y z + 14841 x y z + 8538 x y z + 2543 x y z + 290 x z 8 7 2 6 3 5 4 4 + 48 y z + 596 x y z + 2543 x y z + 5714 x y z + 7442 x y z 5 3 6 2 7 8 9 8 + 5714 x y z + 2543 x y z + 596 x y z + 48 x z + 4 y + 48 x y 2 7 3 6 4 5 5 4 6 3 7 2 + 290 x y + 861 x y + 1457 x y + 1457 x y + 861 x y + 290 x y 8 9 9 8 8 2 7 7 + 48 x y + 4 x >= 4 z + 48 y z + 48 x z + 290 y z + 564 x y z 2 7 3 6 2 6 2 6 3 6 4 5 + 290 x z + 861 y z + 2575 x y z + 2575 x y z + 861 x z + 1457 y z 3 5 2 2 5 3 5 4 5 5 4 + 5738 x y z + 8522 x y z + 5738 x y z + 1457 x z + 1457 y z 4 4 2 3 4 3 2 4 4 4 5 4 + 7362 x y z + 14857 x y z + 14857 x y z + 7362 x y z + 1457 x z 6 3 5 3 2 4 3 3 3 3 4 2 3 + 861 y z + 5738 x y z + 14857 x y z + 19944 x y z + 14857 x y z 5 3 6 3 7 2 6 2 2 5 2 + 5738 x y z + 861 x z + 290 y z + 2575 x y z + 8522 x y z 3 4 2 4 3 2 5 2 2 6 2 7 2 + 14857 x y z + 14857 x y z + 8522 x y z + 2575 x y z + 290 x z 8 7 2 6 3 5 4 4 + 48 y z + 564 x y z + 2575 x y z + 5738 x y z + 7362 x y z 5 3 6 2 7 8 9 8 + 5738 x y z + 2575 x y z + 564 x y z + 48 x z + 4 y + 48 x y 2 7 3 6 4 5 5 4 6 3 7 2 + 290 x y + 861 x y + 1457 x y + 1457 x y + 861 x y + 290 x y 8 9 + 48 x y + 4 x Expanding and collecting terms of the same sign gives: 7 2 2 5 4 4 4 4 3 3 3 2 5 2 32 x y z + 16 x y z + 80 x y z + 80 x y z + 48 x y z + 16 x y z 5 2 2 7 4 4 7 + 16 x y z + 32 x y z + 80 x y z + 32 x y z >= 2 6 2 6 3 5 3 5 2 3 4 3 2 4 32 x y z + 32 x y z + 24 x y z + 24 x y z + 16 x y z + 16 x y z 5 3 2 4 3 4 2 3 5 3 6 2 + 24 x y z + 16 x y z + 16 x y z + 24 x y z + 32 x y z 3 4 2 4 3 2 6 2 2 6 3 5 + 16 x y z + 16 x y z + 32 x y z + 32 x y z + 24 x y z 5 3 6 2 + 24 x y z + 32 x y z Dividing both sides by 8 x y z gives: 6 4 3 3 3 3 2 2 2 4 4 6 4 z + 2 x y z + 10 y z + 10 x z + 6 x y z + 2 x y z + 2 x y z + 4 y 3 3 6 5 5 2 4 2 4 2 3 + 10 x y + 4 x >= 4 y z + 4 x z + 3 y z + 3 x z + 2 x y z 2 3 4 2 3 2 3 2 4 2 5 2 3 + 2 x y z + 3 y z + 2 x y z + 2 x y z + 3 x z + 4 y z + 2 x y z 3 2 5 5 2 4 4 2 5 + 2 x y z + 4 x z + 4 x y + 3 x y + 3 x y + 4 x y Expressing in terms of symmetric polynomials gives: 2 {6, 0, 0} + {4, 1, 1} + 5 {3, 3, 0} + {2, 2, 2} >= 4 {5, 1, 0} + 3 {4, 2, 0} + 2 {3, 2, 1} This follows from the following majorizations: {6, 0, 0} + {2, 2, 2} >= 2 {4, 2, 0} {6, 0, 0} >= {5, 1, 0} left side: [{2, 2, 2}, 5 {3, 3, 0}, {4, 1, 1}, 2 {6, 0, 0}] right side: [2 {3, 2, 1}, 3 {4, 2, 0}, 4 {5, 1, 0}] (d8) notsure (c9) /* 6.11 */ trineq(csum(h(a))<=3*(R+r)); 2 K 2 K 2 K To prove: 3 (r + R) >= --- + --- + --- c b a Let r = K/s . Let R = a*b*c/(4*K) . We get: 2 3 a b c s + 12 K (2 K b + 2 K a) c + 2 K a b ----------------- >= --------------------------- 4 K s a b c Multiplying both sides by 4 K a b c s gives: 2 2 2 2 2 2 2 3 a b c s + 12 K a b c >= 8 K b c s + 8 K a c s + 8 K a b s Replacing K^2 by F^2 gives: 2 2 2 2 2 2 2 3 a b c s + 12 F a b c >= ((8 F b + 8 F a) c + 8 F a b) s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 5 3 2 2 3 3 2 3 3 2 2 - (3 a b c + (- 6 a b - 6 a b - 6 a b) c + (- 6 a b - 6 a b ) c 5 3 3 5 + (3 a b - 6 a b + 3 a b) c)/4 >= 6 2 2 5 3 2 2 3 4 - ((b + a) c + (b + 3 a b + a ) c + (- 2 b - a b - a b - 2 a ) c 4 3 2 2 3 4 3 + (- 2 b - 6 a b - 4 a b - 6 a b - 2 a ) c 5 4 2 3 3 2 4 5 2 + (b - a b - 4 a b - 4 a b - a b + a ) c 6 5 2 4 3 3 4 2 5 6 6 2 5 + (b + 3 a b - a b - 6 a b - a b + 3 a b + a ) c + a b + a b 3 4 4 3 5 2 6 - 2 a b - 2 a b + a b + a b)/4 Multiplying both sides by 4 gives: 5 3 3 2 2 3 3 3 2 3 2 3 2 2 - 3 a b c + 6 a b c + 6 a b c + 6 a b c + 6 a b c + 6 a b c 5 3 3 5 6 6 2 5 5 2 5 - 3 a b c + 6 a b c - 3 a b c >= - b c - a c - b c - 3 a b c - a c 3 4 2 4 2 4 3 4 4 3 3 3 2 2 3 + 2 b c + a b c + a b c + 2 a c + 2 b c + 6 a b c + 4 a b c 3 3 4 3 5 2 4 2 2 3 2 3 2 2 4 2 + 6 a b c + 2 a c - b c + a b c + 4 a b c + 4 a b c + a b c 5 2 6 5 2 4 3 3 4 2 5 6 - a c - b c - 3 a b c + a b c + 6 a b c + a b c - 3 a b c - a c 6 2 5 3 4 4 3 5 2 6 - a b - a b + 2 a b + 2 a b - a b - a b Expanding and collecting terms of the same sign gives: 6 6 2 5 2 5 2 2 3 5 2 2 3 2 3 2 2 b c + a c + b c + a c + 2 a b c + b c + 2 a b c + 2 a b c 5 2 6 6 6 2 5 5 2 6 + a c + b c + a c + a b + a b + a b + a b >= 3 4 2 4 2 4 3 4 4 3 4 3 4 2 4 2 2 b c + a b c + a b c + 2 a c + 2 b c + 2 a c + a b c + a b c 2 4 4 2 3 4 4 3 + a b c + a b c + 2 a b + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 7 6 2 2 5 (2 z + (8 y + 8 x) z + (19 y + 28 x y + 19 x ) z 3 2 2 3 4 + (31 y + 53 x y + 53 x y + 31 x ) z 4 3 2 2 3 4 3 + (31 y + 68 x y + 64 x y + 68 x y + 31 x ) z 5 4 2 3 3 2 4 5 2 + (19 y + 53 x y + 64 x y + 64 x y + 53 x y + 19 x ) z 6 5 2 4 3 3 4 2 5 6 7 + (8 y + 28 x y + 53 x y + 68 x y + 53 x y + 28 x y + 8 x ) z + 2 y 6 2 5 3 4 4 3 5 2 6 7 + 8 x y + 19 x y + 31 x y + 31 x y + 19 x y + 8 x y + 2 x )/64 >= 7 6 2 2 5 (2 z + (8 y + 8 x) z + (13 y + 32 x y + 13 x ) z 3 2 2 3 4 + (13 y + 55 x y + 55 x y + 13 x ) z 4 3 2 2 3 4 3 + (13 y + 64 x y + 108 x y + 64 x y + 13 x ) z 5 4 2 3 3 2 4 5 2 + (13 y + 55 x y + 108 x y + 108 x y + 55 x y + 13 x ) z 6 5 2 4 3 3 4 2 5 6 7 + (8 y + 32 x y + 55 x y + 64 x y + 55 x y + 32 x y + 8 x ) z + 2 y 6 2 5 3 4 4 3 5 2 6 7 + 8 x y + 13 x y + 13 x y + 13 x y + 13 x y + 8 x y + 2 x )/64 Multiplying both sides by 64 gives: 7 6 6 2 5 5 2 5 3 4 2 z + 8 y z + 8 x z + 19 y z + 28 x y z + 19 x z + 31 y z 2 4 2 4 3 4 4 3 3 3 2 2 3 + 53 x y z + 53 x y z + 31 x z + 31 y z + 68 x y z + 64 x y z 3 3 4 3 5 2 4 2 2 3 2 3 2 2 + 68 x y z + 31 x z + 19 y z + 53 x y z + 64 x y z + 64 x y z 4 2 5 2 6 5 2 4 3 3 + 53 x y z + 19 x z + 8 y z + 28 x y z + 53 x y z + 68 x y z 4 2 5 6 7 6 2 5 3 4 + 53 x y z + 28 x y z + 8 x z + 2 y + 8 x y + 19 x y + 31 x y 4 3 5 2 6 7 + 31 x y + 19 x y + 8 x y + 2 x >= 7 6 6 2 5 5 2 5 3 4 2 z + 8 y z + 8 x z + 13 y z + 32 x y z + 13 x z + 13 y z 2 4 2 4 3 4 4 3 3 3 2 2 3 + 55 x y z + 55 x y z + 13 x z + 13 y z + 64 x y z + 108 x y z 3 3 4 3 5 2 4 2 2 3 2 3 2 2 + 64 x y z + 13 x z + 13 y z + 55 x y z + 108 x y z + 108 x y z 4 2 5 2 6 5 2 4 3 3 + 55 x y z + 13 x z + 8 y z + 32 x y z + 55 x y z + 64 x y z 4 2 5 6 7 6 2 5 3 4 + 55 x y z + 32 x y z + 8 x z + 2 y + 8 x y + 13 x y + 13 x y 4 3 5 2 6 7 + 13 x y + 13 x y + 8 x y + 2 x Expanding and collecting terms of the same sign gives: 2 5 2 5 3 4 3 4 4 3 3 3 3 3 6 y z + 6 x z + 18 y z + 18 x z + 18 y z + 4 x y z + 4 x y z 4 3 5 2 5 2 3 3 2 5 3 4 4 3 + 18 x z + 6 y z + 6 x z + 4 x y z + 6 x y + 18 x y + 18 x y 5 2 5 2 4 2 4 2 2 3 4 2 + 6 x y >= 4 x y z + 2 x y z + 2 x y z + 44 x y z + 2 x y z 2 3 2 3 2 2 4 2 5 2 4 4 2 + 44 x y z + 44 x y z + 2 x y z + 4 x y z + 2 x y z + 2 x y z 5 + 4 x y z Dividing both sides by 2 gives: 2 5 2 5 3 4 3 4 4 3 3 3 3 3 3 y z + 3 x z + 9 y z + 9 x z + 9 y z + 2 x y z + 2 x y z 4 3 5 2 5 2 3 3 2 5 3 4 4 3 + 9 x z + 3 y z + 3 x z + 2 x y z + 3 x y + 9 x y + 9 x y 5 2 5 2 4 2 4 2 2 3 4 2 + 3 x y >= 2 x y z + x y z + x y z + 22 x y z + x y z 2 3 2 3 2 2 4 2 5 2 4 4 2 + 22 x y z + 22 x y z + x y z + 2 x y z + x y z + x y z 5 + 2 x y z Expressing in terms of symmetric polynomials gives: 3 {5, 2, 0} + 9 {4, 3, 0} + {3, 3, 1} >= {5, 1, 1} + {4, 2, 1} + 11 {3, 2, 2} This follows from the following majorizations: {5, 2, 0} >= {5, 1, 1} left side: [{3, 3, 1}, 9 {4, 3, 0}, 3 {5, 2, 0}] right side: [11 {3, 2, 2}, {4, 2, 1}, {5, 1, 1}] (d9) notsure (c10) /* 6.12 */ trineq(csum(h(a))<=2*R+5*r); 2 K 2 K 2 K To prove: 5 r + 2 R >= --- + --- + --- c b a Let r = K/s . Let R = a*b*c/(4*K) . We get: 2 a b c s + 10 K (2 K b + 2 K a) c + 2 K a b --------------- >= --------------------------- 2 K s a b c Multiplying both sides by 2 K a b c s gives: 2 2 2 2 2 2 2 a b c s + 10 K a b c >= 4 K b c s + 4 K a c s + 4 K a b s Replacing K^2 by F^2 gives: 2 2 2 2 2 2 2 a b c s + 10 F a b c >= ((4 F b + 4 F a) c + 4 F a b) s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 5 3 2 2 3 3 2 3 3 2 2 - (5 a b c + (- 10 a b - 4 a b - 10 a b) c + (- 4 a b - 4 a b ) c 5 3 3 5 + (5 a b - 10 a b + 5 a b) c)/8 >= 6 2 2 5 3 2 2 3 4 - ((b + a) c + (b + 3 a b + a ) c + (- 2 b - a b - a b - 2 a ) c 4 3 2 2 3 4 3 + (- 2 b - 6 a b - 4 a b - 6 a b - 2 a ) c 5 4 2 3 3 2 4 5 2 + (b - a b - 4 a b - 4 a b - a b + a ) c 6 5 2 4 3 3 4 2 5 6 6 2 5 + (b + 3 a b - a b - 6 a b - a b + 3 a b + a ) c + a b + a b 3 4 4 3 5 2 6 - 2 a b - 2 a b + a b + a b)/8 Multiplying both sides by 8 gives: 5 3 3 2 2 3 3 3 2 3 2 3 2 2 - 5 a b c + 10 a b c + 4 a b c + 10 a b c + 4 a b c + 4 a b c 5 3 3 5 - 5 a b c + 10 a b c - 5 a b c >= 6 6 2 5 5 2 5 3 4 2 4 2 4 - b c - a c - b c - 3 a b c - a c + 2 b c + a b c + a b c 3 4 4 3 3 3 2 2 3 3 3 4 3 5 2 + 2 a c + 2 b c + 6 a b c + 4 a b c + 6 a b c + 2 a c - b c 4 2 2 3 2 3 2 2 4 2 5 2 6 5 + a b c + 4 a b c + 4 a b c + a b c - a c - b c - 3 a b c 2 4 3 3 4 2 5 6 6 2 5 3 4 + a b c + 6 a b c + a b c - 3 a b c - a c - a b - a b + 2 a b 4 3 5 2 6 + 2 a b - a b - a b Expanding and collecting terms of the same sign gives: 6 6 2 5 2 5 3 3 3 3 5 2 5 2 6 b c + a c + b c + a c + 4 a b c + 4 a b c + b c + a c + b c 3 3 6 6 2 5 5 2 6 + 4 a b c + a c + a b + a b + a b + a b >= 5 3 4 2 4 2 4 3 4 4 3 4 3 4 2 2 a b c + 2 b c + a b c + a b c + 2 a c + 2 b c + 2 a c + a b c 4 2 5 2 4 4 2 5 3 4 4 3 + a b c + 2 a b c + a b c + a b c + 2 a b c + 2 a b + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 7 6 2 2 5 (2 z + (10 y + 10 x) z + (23 y + 36 x y + 23 x ) z 3 2 2 3 4 + (35 y + 71 x y + 71 x y + 35 x ) z 4 3 2 2 3 4 3 + (35 y + 92 x y + 104 x y + 92 x y + 35 x ) z 5 4 2 3 3 2 4 5 2 + (23 y + 71 x y + 104 x y + 104 x y + 71 x y + 23 x ) z 6 5 2 4 3 3 4 2 5 6 + (10 y + 36 x y + 71 x y + 92 x y + 71 x y + 36 x y + 10 x ) z 7 6 2 5 3 4 4 3 5 2 6 7 + 2 y + 10 x y + 23 x y + 35 x y + 35 x y + 23 x y + 10 x y + 2 x ) 7 6 2 2 5 /64 >= (2 z + (10 y + 10 x) z + (19 y + 44 x y + 19 x ) z 3 2 2 3 4 + (23 y + 75 x y + 75 x y + 23 x ) z 4 3 2 2 3 4 3 + (23 y + 84 x y + 128 x y + 84 x y + 23 x ) z 5 4 2 3 3 2 4 5 2 + (19 y + 75 x y + 128 x y + 128 x y + 75 x y + 19 x ) z 6 5 2 4 3 3 4 2 5 6 + (10 y + 44 x y + 75 x y + 84 x y + 75 x y + 44 x y + 10 x ) z 7 6 2 5 3 4 4 3 5 2 6 7 + 2 y + 10 x y + 19 x y + 23 x y + 23 x y + 19 x y + 10 x y + 2 x ) /64 Multiplying both sides by 64 gives: 7 6 6 2 5 5 2 5 3 4 2 z + 10 y z + 10 x z + 23 y z + 36 x y z + 23 x z + 35 y z 2 4 2 4 3 4 4 3 3 3 2 2 3 + 71 x y z + 71 x y z + 35 x z + 35 y z + 92 x y z + 104 x y z 3 3 4 3 5 2 4 2 2 3 2 3 2 2 + 92 x y z + 35 x z + 23 y z + 71 x y z + 104 x y z + 104 x y z 4 2 5 2 6 5 2 4 3 3 + 71 x y z + 23 x z + 10 y z + 36 x y z + 71 x y z + 92 x y z 4 2 5 6 7 6 2 5 3 4 + 71 x y z + 36 x y z + 10 x z + 2 y + 10 x y + 23 x y + 35 x y 4 3 5 2 6 7 + 35 x y + 23 x y + 10 x y + 2 x >= 7 6 6 2 5 5 2 5 3 4 2 z + 10 y z + 10 x z + 19 y z + 44 x y z + 19 x z + 23 y z 2 4 2 4 3 4 4 3 3 3 2 2 3 + 75 x y z + 75 x y z + 23 x z + 23 y z + 84 x y z + 128 x y z 3 3 4 3 5 2 4 2 2 3 2 3 2 2 + 84 x y z + 23 x z + 19 y z + 75 x y z + 128 x y z + 128 x y z 4 2 5 2 6 5 2 4 3 3 + 75 x y z + 19 x z + 10 y z + 44 x y z + 75 x y z + 84 x y z 4 2 5 6 7 6 2 5 3 4 + 75 x y z + 44 x y z + 10 x z + 2 y + 10 x y + 19 x y + 23 x y 4 3 5 2 6 7 + 23 x y + 19 x y + 10 x y + 2 x Expanding and collecting terms of the same sign gives: 2 5 2 5 3 4 3 4 4 3 3 3 3 3 4 y z + 4 x z + 12 y z + 12 x z + 12 y z + 8 x y z + 8 x y z 4 3 5 2 5 2 3 3 2 5 3 4 4 3 + 12 x z + 4 y z + 4 x z + 8 x y z + 4 x y + 12 x y + 12 x y 5 2 5 2 4 2 4 2 2 3 4 2 + 4 x y >= 8 x y z + 4 x y z + 4 x y z + 24 x y z + 4 x y z 2 3 2 3 2 2 4 2 5 2 4 4 2 + 24 x y z + 24 x y z + 4 x y z + 8 x y z + 4 x y z + 4 x y z 5 + 8 x y z Dividing both sides by 4 gives: 2 5 2 5 3 4 3 4 4 3 3 3 3 3 4 3 y z + x z + 3 y z + 3 x z + 3 y z + 2 x y z + 2 x y z + 3 x z 5 2 5 2 3 3 2 5 3 4 4 3 5 2 + y z + x z + 2 x y z + x y + 3 x y + 3 x y + x y >= 5 2 4 2 4 2 2 3 4 2 2 3 2 3 2 2 2 x y z + x y z + x y z + 6 x y z + x y z + 6 x y z + 6 x y z 4 2 5 2 4 4 2 5 + x y z + 2 x y z + x y z + x y z + 2 x y z Expressing in terms of symmetric polynomials gives: {5, 2, 0} + 3 {4, 3, 0} + {3, 3, 1} >= {5, 1, 1} + {4, 2, 1} + 3 {3, 2, 2} This follows from the following majorizations: {5, 2, 0} >= {5, 1, 1} {4, 3, 0} >= {4, 2, 1} 2 {4, 3, 0} >= 2 {3, 2, 2} {3, 3, 1} >= {3, 2, 2} (d10) true (c11) /* 6.13 */ trineq(2*r*(5*R-r)/R<=csum(h(a))); 2 K 2 K 2 K 2 (5 R - r) r To prove: --- + --- + --- >= ------------- c b a R Expanding and collecting terms of the same sign gives: 2 2 r 2 K 2 K 2 K ---- + --- + --- + --- >= 10 r R c b a Let r = K/s . Let R = a*b*c/(4*K) . We get: 2 3 ((2 K b + 2 K a) c + 2 K a b) s + 8 K 10 K --------------------------------------- >= ---- 2 s a b c s 2 Multiplying both sides by a b c s gives: 2 2 2 3 2 K b c s + 2 K a c s + 2 K a b s + 8 K >= 10 K a b c s Replacing K^2 by F^2 gives: 2 2 ((2 K b + 2 K a) c + 2 K a b) s + 8 F K >= 10 K a b c s left side: [2 {2, 2, 0}] right side: [{2, 1, 1}, {4, 0, 0}] left side: [{2, 1, 1}, {4, 0, 0}] right side: [2 {2, 2, 0}] 2 2 Cannot determine sign of: ((2 b + 2 a) c + 2 a b) s - 10 a b c s + 8 F 2 2 2 2 2 2 2 8 ((4 b + 8 a b + 4 a ) c + (8 a b + 8 a b) c + 4 a b ) s 2 2 3 3 2 2 3 2 + ((- 4 b - 8 a b - 4 a ) c + (- 4 b - 60 a b - 60 a b - 4 a ) c 3 2 2 3 2 3 3 2 7 + (- 8 a b - 60 a b - 8 a b) c - 4 a b - 4 a b ) s 3 2 2 3 3 3 2 2 3 2 + ((4 b + 52 a b + 52 a b + 4 a ) c + (52 a b + 244 a b + 52 a b) c 2 3 3 2 2 2 3 3 2 6 + (52 a b + 52 a b + 32 F b + 32 F a) c + 4 a b + 32 F a b) s 3 2 2 3 3 + ((- 44 a b - 188 a b - 44 a b) c 2 3 3 2 2 2 2 + (- 188 a b - 188 a b - 32 F b - 32 F a) c 3 3 2 2 2 2 2 2 2 2 2 + (- 44 a b - 32 F b - 256 F a b - 32 F a ) c - 32 F a b - 32 F a b) 5 2 3 3 2 3 3 3 2 2 2 s + ((140 a b + 140 a b ) c + (140 a b + 32 F b + 224 F a b 2 2 2 2 2 2 2 2 2 2 4 4 + 32 F a ) c + (224 F a b + 224 F a b) c + 32 F a b + 64 F ) s 3 3 3 2 2 2 2 2 + (- 100 a b c + (- 192 F a b - 192 F a b) c 2 2 2 4 4 4 3 + (- 192 F a b - 64 F ) c - 64 F b - 64 F a) s 2 2 2 2 4 4 4 2 4 + (160 F a b c + (64 F b + 64 F a) c + 64 F a b) s - 64 F a b c s >= 0 Expanding and collecting terms of the same sign gives: 2 2 8 2 8 2 2 8 2 8 2 8 2 2 8 4 b c s + 8 a b c s + 4 a c s + 8 a b c s + 8 a b c s + 4 a b s 3 3 6 2 3 6 2 3 6 3 3 6 3 2 6 + 4 b c s + 52 a b c s + 52 a b c s + 4 a c s + 52 a b c s 2 2 2 6 3 2 6 2 3 6 3 2 6 + 244 a b c s + 52 a b c s + 52 a b c s + 52 a b c s 2 6 2 6 3 3 6 2 6 2 3 3 4 + 32 F b c s + 32 F a c s + 4 a b s + 32 F a b s + 140 a b c s 3 2 3 4 3 3 2 4 2 2 2 4 2 2 4 + 140 a b c s + 140 a b c s + 32 F b c s + 224 F a b c s 2 2 2 4 2 2 4 2 2 4 2 2 2 4 + 32 F a c s + 224 F a b c s + 224 F a b c s + 32 F a b s 4 4 2 2 2 2 2 4 2 4 2 + 64 F s + 160 F a b c s + 64 F b c s + 64 F a c s 4 2 2 3 7 3 7 2 3 7 3 2 7 + 64 F a b s >= 4 b c s + 8 a b c s + 4 a c s + 4 b c s 2 2 7 2 2 7 3 2 7 3 7 2 2 7 + 60 a b c s + 60 a b c s + 4 a c s + 8 a b c s + 60 a b c s 3 7 2 3 7 3 2 7 3 3 5 2 2 3 5 + 8 a b c s + 4 a b s + 4 a b s + 44 a b c s + 188 a b c s 3 3 5 2 3 2 5 3 2 2 5 2 2 5 + 44 a b c s + 188 a b c s + 188 a b c s + 32 F b c s 2 2 5 3 3 5 2 2 5 2 5 + 32 F a c s + 44 a b c s + 32 F b c s + 256 F a b c s 2 2 5 2 2 5 2 2 5 3 3 3 3 + 32 F a c s + 32 F a b s + 32 F a b s + 100 a b c s 2 2 2 3 2 2 2 3 2 2 2 3 4 3 + 192 F a b c s + 192 F a b c s + 192 F a b c s + 64 F c s 4 3 4 3 4 + 64 F b s + 64 F a s + 64 F a b c s Dividing both sides by 4 s gives: 2 2 7 2 7 2 2 7 2 7 2 7 2 2 7 b c s + 2 a b c s + a c s + 2 a b c s + 2 a b c s + a b s 3 3 5 2 3 5 2 3 5 3 3 5 3 2 5 + b c s + 13 a b c s + 13 a b c s + a c s + 13 a b c s 2 2 2 5 3 2 5 2 3 5 3 2 5 2 5 + 61 a b c s + 13 a b c s + 13 a b c s + 13 a b c s + 8 F b c s 2 5 3 3 5 2 5 2 3 3 3 3 2 3 3 + 8 F a c s + a b s + 8 F a b s + 35 a b c s + 35 a b c s 3 3 2 3 2 2 2 3 2 2 3 2 2 2 3 + 35 a b c s + 8 F b c s + 56 F a b c s + 8 F a c s 2 2 3 2 2 3 2 2 2 3 4 3 + 56 F a b c s + 56 F a b c s + 8 F a b s + 16 F s 2 2 2 2 4 4 4 + 40 F a b c s + 16 F b c s + 16 F a c s + 16 F a b s >= 2 3 6 3 6 2 3 6 3 2 6 2 2 6 2 2 6 b c s + 2 a b c s + a c s + b c s + 15 a b c s + 15 a b c s 3 2 6 3 6 2 2 6 3 6 2 3 6 3 2 6 + a c s + 2 a b c s + 15 a b c s + 2 a b c s + a b s + a b s 3 3 4 2 2 3 4 3 3 4 2 3 2 4 + 11 a b c s + 47 a b c s + 11 a b c s + 47 a b c s 3 2 2 4 2 2 4 2 2 4 3 3 4 2 2 4 + 47 a b c s + 8 F b c s + 8 F a c s + 11 a b c s + 8 F b c s 2 4 2 2 4 2 2 4 2 2 4 3 3 3 2 + 64 F a b c s + 8 F a c s + 8 F a b s + 8 F a b s + 25 a b c s 2 2 2 2 2 2 2 2 2 2 2 2 4 2 + 48 F a b c s + 48 F a b c s + 48 F a b c s + 16 F c s 4 2 4 2 4 + 16 F b s + 16 F a s + 16 F a b c Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 11 10 2 2 9 (c + (5 b + 5 a) c + (- 14 b - 58 a b - 14 a ) c 3 2 2 3 8 + (- 56 b - 260 a b - 260 a b - 56 a ) c 4 3 2 2 3 4 7 + (11 b + 30 a b - 109 a b + 30 a b + 11 a ) c 5 4 2 3 3 2 4 5 6 + (181 b + 1407 a b + 3851 a b + 3851 a b + 1407 a b + 181 a ) c 6 5 2 4 3 3 4 2 5 + (181 b + 2360 a b + 10404 a b + 16406 a b + 10404 a b + 2360 a b 6 5 7 6 2 5 3 4 4 3 + 181 a ) c + (11 b + 1407 a b + 10404 a b + 25282 a b + 25282 a b 5 2 6 7 4 8 7 2 6 + 10404 a b + 1407 a b + 11 a ) c + (- 56 b + 30 a b + 3851 a b 3 5 4 4 5 3 6 2 7 8 3 + 16406 a b + 25282 a b + 16406 a b + 3851 a b + 30 a b - 56 a ) c 9 8 2 7 3 6 4 5 5 4 + (- 14 b - 260 a b - 109 a b + 3851 a b + 10404 a b + 10404 a b 6 3 7 2 8 9 2 + 3851 a b - 109 a b - 260 a b - 14 a ) c 10 9 2 8 3 7 4 6 5 5 + (5 b - 58 a b - 260 a b + 30 a b + 1407 a b + 2360 a b 6 4 7 3 8 2 9 10 11 10 + 1407 a b + 30 a b - 260 a b - 58 a b + 5 a ) c + b + 5 a b 2 9 3 8 4 7 5 6 6 5 7 4 8 3 - 14 a b - 56 a b + 11 a b + 181 a b + 181 a b + 11 a b - 56 a b 9 2 10 11 11 10 - 14 a b + 5 a b + a )/128 >= (c + (b + a) c 2 2 9 3 2 2 3 8 + (- 10 b - 20 a b - 10 a ) c + (- 20 b - 130 a b - 130 a b - 20 a ) c 4 3 2 2 3 4 7 + (15 b - 30 a b - 27 a b - 30 a b + 15 a ) c 5 4 2 3 3 2 4 5 6 + (77 b + 705 a b + 1945 a b + 1945 a b + 705 a b + 77 a ) c 6 5 2 4 3 3 4 2 5 + (77 b + 1252 a b + 5150 a b + 8266 a b + 5150 a b + 1252 a b 6 5 7 6 2 5 3 4 4 3 + 77 a ) c + (15 b + 705 a b + 5150 a b + 12622 a b + 12622 a b 5 2 6 7 4 8 7 2 6 + 5150 a b + 705 a b + 15 a ) c + (- 20 b - 30 a b + 1945 a b 3 5 4 4 5 3 6 2 7 8 3 + 8266 a b + 12622 a b + 8266 a b + 1945 a b - 30 a b - 20 a ) c 9 8 2 7 3 6 4 5 5 4 + (- 10 b - 130 a b - 27 a b + 1945 a b + 5150 a b + 5150 a b 6 3 7 2 8 9 2 + 1945 a b - 27 a b - 130 a b - 10 a ) c 10 9 2 8 3 7 4 6 5 5 6 4 + (b - 20 a b - 130 a b - 30 a b + 705 a b + 1252 a b + 705 a b 7 3 8 2 9 10 11 10 2 9 3 8 - 30 a b - 130 a b - 20 a b + a ) c + b + a b - 10 a b - 20 a b 4 7 5 6 6 5 7 4 8 3 9 2 10 + 15 a b + 77 a b + 77 a b + 15 a b - 20 a b - 10 a b + a b 11 + a )/64 Multiplying both sides by 128 gives: 11 10 10 2 9 9 2 9 3 8 c + 5 b c + 5 a c - 14 b c - 58 a b c - 14 a c - 56 b c 2 8 2 8 3 8 4 7 3 7 2 2 7 - 260 a b c - 260 a b c - 56 a c + 11 b c + 30 a b c - 109 a b c 3 7 4 7 5 6 4 6 2 3 6 + 30 a b c + 11 a c + 181 b c + 1407 a b c + 3851 a b c 3 2 6 4 6 5 6 6 5 5 5 + 3851 a b c + 1407 a b c + 181 a c + 181 b c + 2360 a b c 2 4 5 3 3 5 4 2 5 5 5 6 5 + 10404 a b c + 16406 a b c + 10404 a b c + 2360 a b c + 181 a c 7 4 6 4 2 5 4 3 4 4 4 3 4 + 11 b c + 1407 a b c + 10404 a b c + 25282 a b c + 25282 a b c 5 2 4 6 4 7 4 8 3 7 3 + 10404 a b c + 1407 a b c + 11 a c - 56 b c + 30 a b c 2 6 3 3 5 3 4 4 3 5 3 3 + 3851 a b c + 16406 a b c + 25282 a b c + 16406 a b c 6 2 3 7 3 8 3 9 2 8 2 + 3851 a b c + 30 a b c - 56 a c - 14 b c - 260 a b c 2 7 2 3 6 2 4 5 2 5 4 2 - 109 a b c + 3851 a b c + 10404 a b c + 10404 a b c 6 3 2 7 2 2 8 2 9 2 10 9 + 3851 a b c - 109 a b c - 260 a b c - 14 a c + 5 b c - 58 a b c 2 8 3 7 4 6 5 5 6 4 - 260 a b c + 30 a b c + 1407 a b c + 2360 a b c + 1407 a b c 7 3 8 2 9 10 11 10 2 9 + 30 a b c - 260 a b c - 58 a b c + 5 a c + b + 5 a b - 14 a b 3 8 4 7 5 6 6 5 7 4 8 3 9 2 - 56 a b + 11 a b + 181 a b + 181 a b + 11 a b - 56 a b - 14 a b 10 11 11 10 10 2 9 9 2 9 + 5 a b + a >= 2 c + 2 b c + 2 a c - 20 b c - 40 a b c - 20 a c 3 8 2 8 2 8 3 8 4 7 3 7 - 40 b c - 260 a b c - 260 a b c - 40 a c + 30 b c - 60 a b c 2 2 7 3 7 4 7 5 6 4 6 - 54 a b c - 60 a b c + 30 a c + 154 b c + 1410 a b c 2 3 6 3 2 6 4 6 5 6 6 5 + 3890 a b c + 3890 a b c + 1410 a b c + 154 a c + 154 b c 5 5 2 4 5 3 3 5 4 2 5 + 2504 a b c + 10300 a b c + 16532 a b c + 10300 a b c 5 5 6 5 7 4 6 4 2 5 4 + 2504 a b c + 154 a c + 30 b c + 1410 a b c + 10300 a b c 3 4 4 4 3 4 5 2 4 6 4 7 4 + 25244 a b c + 25244 a b c + 10300 a b c + 1410 a b c + 30 a c 8 3 7 3 2 6 3 3 5 3 4 4 3 - 40 b c - 60 a b c + 3890 a b c + 16532 a b c + 25244 a b c 5 3 3 6 2 3 7 3 8 3 9 2 + 16532 a b c + 3890 a b c - 60 a b c - 40 a c - 20 b c 8 2 2 7 2 3 6 2 4 5 2 5 4 2 - 260 a b c - 54 a b c + 3890 a b c + 10300 a b c + 10300 a b c 6 3 2 7 2 2 8 2 9 2 10 9 + 3890 a b c - 54 a b c - 260 a b c - 20 a c + 2 b c - 40 a b c 2 8 3 7 4 6 5 5 6 4 - 260 a b c - 60 a b c + 1410 a b c + 2504 a b c + 1410 a b c 7 3 8 2 9 10 11 10 2 9 - 60 a b c - 260 a b c - 40 a b c + 2 a c + 2 b + 2 a b - 20 a b 3 8 4 7 5 6 6 5 7 4 8 3 9 2 - 40 a b + 30 a b + 154 a b + 154 a b + 30 a b - 40 a b - 20 a b 10 11 + 2 a b + 2 a Expanding and collecting terms of the same sign gives: 10 10 2 9 2 9 3 7 3 7 5 6 3 b c + 3 a c + 6 b c + 6 a c + 90 a b c + 90 a b c + 27 b c 5 6 6 5 2 4 5 4 2 5 6 5 2 5 4 + 27 a c + 27 b c + 104 a b c + 104 a b c + 27 a c + 104 a b c 3 4 4 4 3 4 5 2 4 7 3 4 4 3 + 38 a b c + 38 a b c + 104 a b c + 90 a b c + 38 a b c 7 3 9 2 4 5 2 5 4 2 9 2 10 + 90 a b c + 6 b c + 104 a b c + 104 a b c + 6 a c + 3 b c 3 7 7 3 10 10 2 9 5 6 6 5 + 90 a b c + 90 a b c + 3 a c + 3 a b + 6 a b + 27 a b + 27 a b 9 2 10 11 9 3 8 3 8 4 7 + 6 a b + 3 a b >= c + 18 a b c + 16 b c + 16 a c + 19 b c 2 2 7 4 7 4 6 2 3 6 3 2 6 4 6 + 55 a b c + 19 a c + 3 a b c + 39 a b c + 39 a b c + 3 a b c 5 5 3 3 5 5 5 7 4 6 4 6 4 + 144 a b c + 126 a b c + 144 a b c + 19 b c + 3 a b c + 3 a b c 7 4 8 3 2 6 3 3 5 3 5 3 3 + 19 a c + 16 b c + 39 a b c + 126 a b c + 126 a b c 6 2 3 8 3 2 7 2 3 6 2 6 3 2 + 39 a b c + 16 a c + 55 a b c + 39 a b c + 39 a b c 7 2 2 9 4 6 5 5 6 4 9 + 55 a b c + 18 a b c + 3 a b c + 144 a b c + 3 a b c + 18 a b c 11 3 8 4 7 7 4 8 3 11 + b + 16 a b + 19 a b + 19 a b + 16 a b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 11 10 2 2 9 (72 z + (582 y + 582 x) z + (2182 y + 4196 x y + 2182 x ) z 3 2 2 3 8 + (5177 y + 13965 x y + 13965 x y + 5177 x ) z 4 3 2 2 3 4 7 + (8562 y + 29392 x y + 42668 x y + 29392 x y + 8562 x ) z 5 4 2 3 3 2 4 5 + (10815 y + 44539 x y + 81810 x y + 81810 x y + 44539 x y + 10815 x ) 6 6 5 2 4 3 3 4 2 z + (10815 y + 51020 x y + 110045 x y + 140976 x y + 110045 x y 5 6 5 7 6 2 5 + 51020 x y + 10815 x ) z + (8562 y + 44539 x y + 110045 x y 3 4 4 3 5 2 6 7 4 + 166834 x y + 166834 x y + 110045 x y + 44539 x y + 8562 x ) z 8 7 2 6 3 5 4 4 + (5177 y + 29392 x y + 81810 x y + 140976 x y + 166834 x y 5 3 6 2 7 8 3 + 140976 x y + 81810 x y + 29392 x y + 5177 x ) z 9 8 2 7 3 6 4 5 + (2182 y + 13965 x y + 42668 x y + 81810 x y + 110045 x y 5 4 6 3 7 2 8 9 2 + 110045 x y + 81810 x y + 42668 x y + 13965 x y + 2182 x ) z 10 9 2 8 3 7 4 6 5 5 + (582 y + 4196 x y + 13965 x y + 29392 x y + 44539 x y + 51020 x y 6 4 7 3 8 2 9 10 11 + 44539 x y + 29392 x y + 13965 x y + 4196 x y + 582 x ) z + 72 y 10 2 9 3 8 4 7 5 6 6 5 + 582 x y + 2182 x y + 5177 x y + 8562 x y + 10815 x y + 10815 x y 7 4 8 3 9 2 10 11 + 8562 x y + 5177 x y + 2182 x y + 582 x y + 72 x )/2048 >= 11 10 2 2 9 (72 z + (582 y + 582 x) z + (2182 y + 4068 x y + 2182 x ) z 3 2 2 3 8 + (5177 y + 13965 x y + 13965 x y + 5177 x ) z 4 3 2 2 3 4 7 + (8562 y + 29904 x y + 42412 x y + 29904 x y + 8562 x ) z 5 4 2 3 3 2 4 5 + (10815 y + 44539 x y + 81554 x y + 81554 x y + 44539 x y + 10815 x ) 6 6 5 2 4 3 3 4 2 z + (10815 y + 50252 x y + 110557 x y + 140336 x y + 110557 x y 5 6 5 7 6 2 5 + 50252 x y + 10815 x ) z + (8562 y + 44539 x y + 110557 x y 3 4 4 3 5 2 6 7 4 + 167090 x y + 167090 x y + 110557 x y + 44539 x y + 8562 x ) z 8 7 2 6 3 5 4 4 + (5177 y + 29904 x y + 81554 x y + 140336 x y + 167090 x y 5 3 6 2 7 8 3 + 140336 x y + 81554 x y + 29904 x y + 5177 x ) z 9 8 2 7 3 6 4 5 + (2182 y + 13965 x y + 42412 x y + 81554 x y + 110557 x y 5 4 6 3 7 2 8 9 2 + 110557 x y + 81554 x y + 42412 x y + 13965 x y + 2182 x ) z 10 9 2 8 3 7 4 6 5 5 + (582 y + 4068 x y + 13965 x y + 29904 x y + 44539 x y + 50252 x y 6 4 7 3 8 2 9 10 11 + 44539 x y + 29904 x y + 13965 x y + 4068 x y + 582 x ) z + 72 y 10 2 9 3 8 4 7 5 6 6 5 + 582 x y + 2182 x y + 5177 x y + 8562 x y + 10815 x y + 10815 x y 7 4 8 3 9 2 10 11 + 8562 x y + 5177 x y + 2182 x y + 582 x y + 72 x )/2048 Multiplying both sides by 2048 gives: 11 10 10 2 9 9 2 9 72 z + 582 y z + 582 x z + 2182 y z + 4196 x y z + 2182 x z 3 8 2 8 2 8 3 8 4 7 + 5177 y z + 13965 x y z + 13965 x y z + 5177 x z + 8562 y z 3 7 2 2 7 3 7 4 7 5 6 + 29392 x y z + 42668 x y z + 29392 x y z + 8562 x z + 10815 y z 4 6 2 3 6 3 2 6 4 6 + 44539 x y z + 81810 x y z + 81810 x y z + 44539 x y z 5 6 6 5 5 5 2 4 5 + 10815 x z + 10815 y z + 51020 x y z + 110045 x y z 3 3 5 4 2 5 5 5 6 5 7 4 + 140976 x y z + 110045 x y z + 51020 x y z + 10815 x z + 8562 y z 6 4 2 5 4 3 4 4 4 3 4 + 44539 x y z + 110045 x y z + 166834 x y z + 166834 x y z 5 2 4 6 4 7 4 8 3 7 3 + 110045 x y z + 44539 x y z + 8562 x z + 5177 y z + 29392 x y z 2 6 3 3 5 3 4 4 3 5 3 3 + 81810 x y z + 140976 x y z + 166834 x y z + 140976 x y z 6 2 3 7 3 8 3 9 2 8 2 + 81810 x y z + 29392 x y z + 5177 x z + 2182 y z + 13965 x y z 2 7 2 3 6 2 4 5 2 5 4 2 + 42668 x y z + 81810 x y z + 110045 x y z + 110045 x y z 6 3 2 7 2 2 8 2 9 2 10 + 81810 x y z + 42668 x y z + 13965 x y z + 2182 x z + 582 y z 9 2 8 3 7 4 6 5 5 + 4196 x y z + 13965 x y z + 29392 x y z + 44539 x y z + 51020 x y z 6 4 7 3 8 2 9 10 + 44539 x y z + 29392 x y z + 13965 x y z + 4196 x y z + 582 x z 11 10 2 9 3 8 4 7 5 6 + 72 y + 582 x y + 2182 x y + 5177 x y + 8562 x y + 10815 x y 6 5 7 4 8 3 9 2 10 11 + 10815 x y + 8562 x y + 5177 x y + 2182 x y + 582 x y + 72 x >= 11 10 10 2 9 9 2 9 72 z + 582 y z + 582 x z + 2182 y z + 4068 x y z + 2182 x z 3 8 2 8 2 8 3 8 4 7 + 5177 y z + 13965 x y z + 13965 x y z + 5177 x z + 8562 y z 3 7 2 2 7 3 7 4 7 5 6 + 29904 x y z + 42412 x y z + 29904 x y z + 8562 x z + 10815 y z 4 6 2 3 6 3 2 6 4 6 + 44539 x y z + 81554 x y z + 81554 x y z + 44539 x y z 5 6 6 5 5 5 2 4 5 + 10815 x z + 10815 y z + 50252 x y z + 110557 x y z 3 3 5 4 2 5 5 5 6 5 7 4 + 140336 x y z + 110557 x y z + 50252 x y z + 10815 x z + 8562 y z 6 4 2 5 4 3 4 4 4 3 4 + 44539 x y z + 110557 x y z + 167090 x y z + 167090 x y z 5 2 4 6 4 7 4 8 3 7 3 + 110557 x y z + 44539 x y z + 8562 x z + 5177 y z + 29904 x y z 2 6 3 3 5 3 4 4 3 5 3 3 + 81554 x y z + 140336 x y z + 167090 x y z + 140336 x y z 6 2 3 7 3 8 3 9 2 8 2 + 81554 x y z + 29904 x y z + 5177 x z + 2182 y z + 13965 x y z 2 7 2 3 6 2 4 5 2 5 4 2 + 42412 x y z + 81554 x y z + 110557 x y z + 110557 x y z 6 3 2 7 2 2 8 2 9 2 10 + 81554 x y z + 42412 x y z + 13965 x y z + 2182 x z + 582 y z 9 2 8 3 7 4 6 5 5 + 4068 x y z + 13965 x y z + 29904 x y z + 44539 x y z + 50252 x y z 6 4 7 3 8 2 9 10 + 44539 x y z + 29904 x y z + 13965 x y z + 4068 x y z + 582 x z 11 10 2 9 3 8 4 7 5 6 + 72 y + 582 x y + 2182 x y + 5177 x y + 8562 x y + 10815 x y 6 5 7 4 8 3 9 2 10 11 + 10815 x y + 8562 x y + 5177 x y + 2182 x y + 582 x y + 72 x Expanding and collecting terms of the same sign gives: 9 2 2 7 2 3 6 3 2 6 5 5 128 x y z + 256 x y z + 256 x y z + 256 x y z + 768 x y z 3 3 5 5 5 2 6 3 3 5 3 5 3 3 + 640 x y z + 768 x y z + 256 x y z + 640 x y z + 640 x y z 6 2 3 2 7 2 3 6 2 6 3 2 7 2 2 + 256 x y z + 256 x y z + 256 x y z + 256 x y z + 256 x y z 9 5 5 9 + 128 x y z + 768 x y z + 128 x y z >= 3 7 3 7 2 4 5 4 2 5 2 5 4 512 x y z + 512 x y z + 512 x y z + 512 x y z + 512 x y z 3 4 4 4 3 4 5 2 4 7 3 4 4 3 + 256 x y z + 256 x y z + 512 x y z + 512 x y z + 256 x y z 7 3 4 5 2 5 4 2 3 7 7 3 + 512 x y z + 512 x y z + 512 x y z + 512 x y z + 512 x y z Dividing both sides by 128 x y z gives: 8 6 2 5 2 5 4 4 2 2 4 4 4 z + 2 x y z + 2 x y z + 2 x y z + 6 y z + 5 x y z + 6 x z 5 2 2 4 2 4 2 2 5 2 6 2 5 + 2 x y z + 5 x y z + 5 x y z + 2 x y z + 2 x y z + 2 x y z 5 2 6 8 4 4 8 + 2 x y z + 2 x y z + y + 6 x y + x >= 2 6 2 6 3 4 3 4 4 3 2 3 3 3 2 3 4 y z + 4 x z + 4 x y z + 4 x y z + 4 x y z + 2 x y z + 2 x y z 4 3 6 2 3 3 2 6 2 3 4 4 3 2 6 + 4 x y z + 4 y z + 2 x y z + 4 x z + 4 x y z + 4 x y z + 4 x y 6 2 + 4 x y Expressing in terms of symmetric polynomials gives: {8, 0, 0} + 2 {6, 1, 1} + 4 {5, 2, 1} + 6 {4, 4, 0} + 5 {4, 2, 2} >= 8 {6, 2, 0} + 8 {4, 3, 1} + 2 {3, 3, 2} This follows from the following majorizations: {8, 0, 0} >= {6, 2, 0} left side: [5 {4, 2, 2}, 6 {4, 4, 0}, 4 {5, 2, 1}, 2 {6, 1, 1}, {8, 0, 0}] right side: [2 {3, 3, 2}, 8 {4, 3, 1}, 8 {6, 2, 0}] (d11) notsure (c12) trineq(csum(h(a))<=2*(R+r)^2/R); 2 2 (r + R) 2 K 2 K 2 K To prove: ---------- >= --- + --- + --- R c b a Let r = K/s . Let R = a*b*c/(4*K) . We get: 2 2 2 2 2 4 a b c s + 8 K a b c s + 16 K (2 K b + 2 K a) c + 2 K a b ---------------------------------- >= --------------------------- 2 a b c 2 K a b c s 2 Multiplying both sides by 2 K a b c s gives: 2 2 2 2 2 4 2 2 2 2 2 2 a b c s + 8 K a b c s + 16 K >= 4 K b c s + 4 K a c s + 4 K a b s Replacing K^2 by F^2 gives: 2 2 2 2 2 4 2 2 2 2 a b c s + 8 F a b c s + 16 F >= ((4 F b + 4 F a) c + 4 F a b) s Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 8 2 2 6 2 2 5 (c + (- 4 b - 4 a b - 4 a ) c + (- 4 a b - 4 a b) c 4 3 2 2 3 4 4 + (6 b + 8 a b + 8 a b + 8 a b + 6 a ) c 4 2 3 3 2 4 3 + (8 a b + 16 a b + 16 a b + 8 a b) c 6 5 2 4 3 3 4 2 5 6 2 + (- 4 b - 4 a b + 8 a b + 16 a b + 8 a b - 4 a b - 4 a ) c 6 2 5 3 4 4 3 5 2 6 8 2 6 + (- 4 a b - 4 a b + 8 a b + 8 a b - 4 a b - 4 a b) c + b - 4 a b 4 4 6 2 8 7 2 2 6 + 6 a b - 4 a b + a )/16 >= - ((b + a) c + (2 b + 5 a b + 2 a ) c 3 2 2 3 5 4 3 2 2 3 + (- b + 3 a b + 3 a b - a ) c + (- 4 b - 9 a b - 6 a b - 9 a b 4 4 5 4 2 3 3 2 4 5 3 - 4 a ) c + (- b - 9 a b - 14 a b - 14 a b - 9 a b - a ) c 6 5 2 4 3 3 4 2 5 6 2 + (2 b + 3 a b - 6 a b - 14 a b - 6 a b + 3 a b + 2 a ) c 7 6 2 5 3 4 4 3 5 2 6 7 7 + (b + 5 a b + 3 a b - 9 a b - 9 a b + 3 a b + 5 a b + a ) c + a b 2 6 3 5 4 4 5 3 6 2 7 + 2 a b - a b - 4 a b - a b + 2 a b + a b)/16 Multiplying both sides by 16 gives: 8 2 6 6 2 6 2 5 2 5 4 4 3 4 c - 4 b c - 4 a b c - 4 a c - 4 a b c - 4 a b c + 6 b c + 8 a b c 2 2 4 3 4 4 4 4 3 2 3 3 3 2 3 + 8 a b c + 8 a b c + 6 a c + 8 a b c + 16 a b c + 16 a b c 4 3 6 2 5 2 2 4 2 3 3 2 4 2 2 + 8 a b c - 4 b c - 4 a b c + 8 a b c + 16 a b c + 8 a b c 5 2 6 2 6 2 5 3 4 4 3 - 4 a b c - 4 a c - 4 a b c - 4 a b c + 8 a b c + 8 a b c 5 2 6 8 2 6 4 4 6 2 8 - 4 a b c - 4 a b c + b - 4 a b + 6 a b - 4 a b + a >= 7 7 2 6 6 2 6 3 5 2 5 2 5 - b c - a c - 2 b c - 5 a b c - 2 a c + b c - 3 a b c - 3 a b c 3 5 4 4 3 4 2 2 4 3 4 4 4 5 3 + a c + 4 b c + 9 a b c + 6 a b c + 9 a b c + 4 a c + b c 4 3 2 3 3 3 2 3 4 3 5 3 6 2 + 9 a b c + 14 a b c + 14 a b c + 9 a b c + a c - 2 b c 5 2 2 4 2 3 3 2 4 2 2 5 2 6 2 - 3 a b c + 6 a b c + 14 a b c + 6 a b c - 3 a b c - 2 a c 7 6 2 5 3 4 4 3 5 2 6 - b c - 5 a b c - 3 a b c + 9 a b c + 9 a b c - 3 a b c - 5 a b c 7 7 2 6 3 5 4 4 5 3 6 2 7 - a c - a b - 2 a b + a b + 4 a b + a b - 2 a b - a b Expanding and collecting terms of the same sign gives: 8 7 7 6 4 4 2 2 4 4 4 2 3 3 c + b c + a c + a b c + 2 b c + 2 a b c + 2 a c + 2 a b c 3 2 3 2 4 2 3 3 2 4 2 2 7 6 6 + 2 a b c + 2 a b c + 2 a b c + 2 a b c + b c + a b c + a b c 7 8 7 4 4 7 8 + a c + b + a b + 2 a b + a b + a >= 2 6 2 6 3 5 2 5 2 5 3 5 3 4 3 4 2 b c + 2 a c + b c + a b c + a b c + a c + a b c + a b c 5 3 4 3 4 3 5 3 6 2 5 2 5 2 6 2 + b c + a b c + a b c + a c + 2 b c + a b c + a b c + 2 a c 2 5 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 c + 2 a b + a b + a b + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 8 7 2 2 6 (6 z + (28 y + 28 x) z + (81 y + 86 x y + 81 x ) z 3 2 2 3 5 + (157 y + 183 x y + 183 x y + 157 x ) z 4 3 2 2 3 4 4 + (198 y + 291 x y + 338 x y + 291 x y + 198 x ) z 5 4 2 3 3 2 4 5 3 + (157 y + 291 x y + 452 x y + 452 x y + 291 x y + 157 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (81 y + 183 x y + 338 x y + 452 x y + 338 x y + 183 x y + 81 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (28 y + 86 x y + 183 x y + 291 x y + 291 x y + 183 x y + 86 x y 7 8 7 2 6 3 5 4 4 5 3 + 28 x ) z + 6 y + 28 x y + 81 x y + 157 x y + 198 x y + 157 x y 6 2 7 8 8 7 + 81 x y + 28 x y + 6 x )/256 >= (6 z + (28 y + 28 x) z 2 2 6 3 2 2 3 5 + (65 y + 118 x y + 65 x ) z + (93 y + 247 x y + 247 x y + 93 x ) z 4 3 2 2 3 4 4 + (102 y + 323 x y + 402 x y + 323 x y + 102 x ) z 5 4 2 3 3 2 4 5 3 + (93 y + 323 x y + 420 x y + 420 x y + 323 x y + 93 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (65 y + 247 x y + 402 x y + 420 x y + 402 x y + 247 x y + 65 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (28 y + 118 x y + 247 x y + 323 x y + 323 x y + 247 x y + 118 x y 7 8 7 2 6 3 5 4 4 5 3 + 28 x ) z + 6 y + 28 x y + 65 x y + 93 x y + 102 x y + 93 x y 6 2 7 8 + 65 x y + 28 x y + 6 x )/256 Multiplying both sides by 256 gives: 8 7 7 2 6 6 2 6 3 5 6 z + 28 y z + 28 x z + 81 y z + 86 x y z + 81 x z + 157 y z 2 5 2 5 3 5 4 4 3 4 + 183 x y z + 183 x y z + 157 x z + 198 y z + 291 x y z 2 2 4 3 4 4 4 5 3 4 3 + 338 x y z + 291 x y z + 198 x z + 157 y z + 291 x y z 2 3 3 3 2 3 4 3 5 3 6 2 + 452 x y z + 452 x y z + 291 x y z + 157 x z + 81 y z 5 2 2 4 2 3 3 2 4 2 2 5 2 + 183 x y z + 338 x y z + 452 x y z + 338 x y z + 183 x y z 6 2 7 6 2 5 3 4 4 3 + 81 x z + 28 y z + 86 x y z + 183 x y z + 291 x y z + 291 x y z 5 2 6 7 8 7 2 6 3 5 + 183 x y z + 86 x y z + 28 x z + 6 y + 28 x y + 81 x y + 157 x y 4 4 5 3 6 2 7 8 + 198 x y + 157 x y + 81 x y + 28 x y + 6 x >= 8 7 7 2 6 6 2 6 3 5 6 z + 28 y z + 28 x z + 65 y z + 118 x y z + 65 x z + 93 y z 2 5 2 5 3 5 4 4 3 4 + 247 x y z + 247 x y z + 93 x z + 102 y z + 323 x y z 2 2 4 3 4 4 4 5 3 4 3 + 402 x y z + 323 x y z + 102 x z + 93 y z + 323 x y z 2 3 3 3 2 3 4 3 5 3 6 2 + 420 x y z + 420 x y z + 323 x y z + 93 x z + 65 y z 5 2 2 4 2 3 3 2 4 2 2 5 2 + 247 x y z + 402 x y z + 420 x y z + 402 x y z + 247 x y z 6 2 7 6 2 5 3 4 4 3 + 65 x z + 28 y z + 118 x y z + 247 x y z + 323 x y z + 323 x y z 5 2 6 7 8 7 2 6 3 5 + 247 x y z + 118 x y z + 28 x z + 6 y + 28 x y + 65 x y + 93 x y 4 4 5 3 6 2 7 8 + 102 x y + 93 x y + 65 x y + 28 x y + 6 x Expanding and collecting terms of the same sign gives: 2 6 2 6 3 5 3 5 4 4 4 4 5 3 16 y z + 16 x z + 64 y z + 64 x z + 96 y z + 96 x z + 64 y z 2 3 3 3 2 3 5 3 6 2 3 3 2 6 2 + 32 x y z + 32 x y z + 64 x z + 16 y z + 32 x y z + 16 x z 2 6 3 5 4 4 5 3 6 2 + 16 x y + 64 x y + 96 x y + 64 x y + 16 x y >= 6 2 5 2 5 3 4 2 2 4 3 4 32 x y z + 64 x y z + 64 x y z + 32 x y z + 64 x y z + 32 x y z 4 3 4 3 5 2 2 4 2 4 2 2 + 32 x y z + 32 x y z + 64 x y z + 64 x y z + 64 x y z 5 2 6 2 5 3 4 4 3 5 2 + 64 x y z + 32 x y z + 64 x y z + 32 x y z + 32 x y z + 64 x y z 6 + 32 x y z 2 Dividing both sides by 16 (z + y + x) gives: 2 4 2 4 3 3 2 3 2 3 3 3 4 2 3 2 y z + x z + 2 y z - 2 x y z - 2 x y z + 2 x z + y z - 2 x y z 2 2 2 3 2 4 2 2 3 3 2 2 4 3 3 + 6 x y z - 2 x y z + x z - 2 x y z - 2 x y z + x y + 2 x y 4 2 4 4 4 + x y >= 2 x y z + 2 x y z + 2 x y z Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 2 2 2 4 2 2 4 y z + x z + 2 y z + 2 x z + y z + 6 x y z + x z + x y 3 3 4 2 4 2 3 2 3 3 2 3 2 + 2 x y + x y >= 2 x y z + 2 x y z + 2 x y z + 2 x y z + 2 x y z 4 2 3 3 2 4 + 2 x y z + 2 x y z + 2 x y z + 2 x y z Expressing in terms of symmetric polynomials gives: {4, 2, 0} + {3, 3, 0} + {2, 2, 2} >= {4, 1, 1} + 2 {3, 2, 1} This follows from the following majorizations: {3, 3, 0} + {2, 2, 2} >= 2 {3, 2, 1} {4, 2, 0} >= {4, 1, 1} (d12) true (c13) /* 6.15 */ trineq(2*csum(h(a)*h(b))<=6*K*sqrt(3)); 2 2 2 4 K 4 K 4 K To prove: 6 sqrt(3) K >= 2 (---- + ---- + ----) b c a c a b Multiplying both sides by a b c gives: 2 2 2 6 sqrt(3) K a b c >= 8 K c + 8 K b + 8 K a Replacing K^2 by F^2 gives: 2 2 2 6 sqrt(3) K a b c >= 8 F c + 8 F b + 8 F a Since 6 sqrt(3) a b c is positive, and since 2 2 2 8 F c + 8 F b + 8 F a is positive, we can square both sides to get: 2 2 2 4 2 3 3 2 2 2 2 3 3 108 a b c s + ((- 108 a b - 108 a b ) c - 108 a b c ) s 2 3 3 2 3 3 3 2 2 3 3 3 + ((108 a b + 108 a b ) c + 108 a b c ) s - 108 a b c s >= 4 2 4 4 4 2 4 4 2 64 F c + (128 F b + 128 F a) c + 64 F b + 128 F a b + 64 F a Expanding and collecting terms of the same sign gives: 2 2 2 4 2 3 3 2 3 2 3 2 3 3 2 2 108 a b c s + 108 a b c s + 108 a b c s + 108 a b c s >= 2 2 3 3 2 3 2 3 3 2 2 3 3 3 3 4 2 108 a b c s + 108 a b c s + 108 a b c s + 108 a b c s + 64 F c 4 4 4 2 4 4 2 + 128 F b c + 128 F a c + 64 F b + 128 F a b + 64 F a Dividing both sides by 4 gives: 2 2 2 4 2 3 3 2 3 2 3 2 3 3 2 2 27 a b c s + 27 a b c s + 27 a b c s + 27 a b c s >= 2 2 3 3 2 3 2 3 3 2 2 3 3 3 3 4 2 27 a b c s + 27 a b c s + 27 a b c s + 27 a b c s + 16 F c 4 4 4 2 4 4 2 + 32 F b c + 32 F a c + 16 F b + 32 F a b + 16 F a Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 6 2 3 3 2 5 (27 a b c + (216 a b + 216 a b ) c 2 4 3 3 4 2 4 + (378 a b + 864 a b + 378 a b ) c 2 5 3 4 4 3 5 2 3 + (216 a b + 864 a b + 864 a b + 216 a b ) c 2 6 3 5 4 4 5 3 6 2 2 + (27 a b + 216 a b + 378 a b + 216 a b + 27 a b ) c )/16 >= 10 9 2 2 8 (c + (2 b + 2 a) c + (- 3 b + 2 a b - 3 a ) c 3 2 2 3 7 + (- 8 b - 8 a b - 8 a b - 8 a ) c 4 3 2 2 3 4 6 + (2 b - 8 a b + 50 a b - 8 a b + 2 a ) c 5 4 2 3 3 2 4 5 5 + (12 b + 12 a b + 224 a b + 224 a b + 12 a b + 12 a ) c 6 5 2 4 3 3 4 2 5 6 4 + (2 b + 12 a b + 338 a b + 872 a b + 338 a b + 12 a b + 2 a ) c 7 6 2 5 3 4 4 3 5 2 6 + (- 8 b - 8 a b + 224 a b + 872 a b + 872 a b + 224 a b - 8 a b 7 3 8 7 2 6 3 5 4 4 5 3 - 8 a ) c + (- 3 b - 8 a b + 50 a b + 224 a b + 338 a b + 224 a b 6 2 7 8 2 9 8 2 7 3 6 4 5 + 50 a b - 8 a b - 3 a ) c + (2 b + 2 a b - 8 a b - 8 a b + 12 a b 5 4 6 3 7 2 8 9 10 9 2 8 + 12 a b - 8 a b - 8 a b + 2 a b + 2 a ) c + b + 2 a b - 3 a b 3 7 4 6 5 5 6 4 7 3 8 2 9 10 - 8 a b + 2 a b + 12 a b + 2 a b - 8 a b - 3 a b + 2 a b + a ) /16 Multiplying both sides by 16 gives: 2 2 6 2 3 5 3 2 5 2 4 4 3 3 4 27 a b c + 216 a b c + 216 a b c + 378 a b c + 864 a b c 4 2 4 2 5 3 3 4 3 4 3 3 5 2 3 + 378 a b c + 216 a b c + 864 a b c + 864 a b c + 216 a b c 2 6 2 3 5 2 4 4 2 5 3 2 6 2 2 + 27 a b c + 216 a b c + 378 a b c + 216 a b c + 27 a b c >= 10 9 9 2 8 8 2 8 3 7 2 7 c + 2 b c + 2 a c - 3 b c + 2 a b c - 3 a c - 8 b c - 8 a b c 2 7 3 7 4 6 3 6 2 2 6 3 6 - 8 a b c - 8 a c + 2 b c - 8 a b c + 50 a b c - 8 a b c 4 6 5 5 4 5 2 3 5 3 2 5 4 5 + 2 a c + 12 b c + 12 a b c + 224 a b c + 224 a b c + 12 a b c 5 5 6 4 5 4 2 4 4 3 3 4 4 2 4 + 12 a c + 2 b c + 12 a b c + 338 a b c + 872 a b c + 338 a b c 5 4 6 4 7 3 6 3 2 5 3 3 4 3 + 12 a b c + 2 a c - 8 b c - 8 a b c + 224 a b c + 872 a b c 4 3 3 5 2 3 6 3 7 3 8 2 7 2 + 872 a b c + 224 a b c - 8 a b c - 8 a c - 3 b c - 8 a b c 2 6 2 3 5 2 4 4 2 5 3 2 6 2 2 + 50 a b c + 224 a b c + 338 a b c + 224 a b c + 50 a b c 7 2 8 2 9 8 2 7 3 6 4 5 - 8 a b c - 3 a c + 2 b c + 2 a b c - 8 a b c - 8 a b c + 12 a b c 5 4 6 3 7 2 8 9 10 9 + 12 a b c - 8 a b c - 8 a b c + 2 a b c + 2 a c + b + 2 a b 2 8 3 7 4 6 5 5 6 4 7 3 8 2 - 3 a b - 8 a b + 2 a b + 12 a b + 2 a b - 8 a b - 3 a b 9 10 + 2 a b + a Expanding and collecting terms of the same sign gives: 2 8 2 8 3 7 2 7 2 7 3 7 3 6 3 b c + 3 a c + 8 b c + 8 a b c + 8 a b c + 8 a c + 8 a b c 3 6 2 4 4 4 2 4 7 3 6 3 6 3 + 8 a b c + 40 a b c + 40 a b c + 8 b c + 8 a b c + 8 a b c 7 3 8 2 7 2 4 4 2 7 2 8 2 + 8 a c + 3 b c + 8 a b c + 40 a b c + 8 a b c + 3 a c 2 7 3 6 6 3 7 2 2 8 3 7 7 3 + 8 a b c + 8 a b c + 8 a b c + 8 a b c + 3 a b + 8 a b + 8 a b 8 2 10 9 9 8 4 6 2 2 6 + 3 a b >= c + 2 b c + 2 a c + 2 a b c + 2 b c + 23 a b c 4 6 5 5 4 5 2 3 5 3 2 5 4 5 + 2 a c + 12 b c + 12 a b c + 8 a b c + 8 a b c + 12 a b c 5 5 6 4 5 4 3 3 4 5 4 6 4 + 12 a c + 2 b c + 12 a b c + 8 a b c + 12 a b c + 2 a c 2 5 3 3 4 3 4 3 3 5 2 3 2 6 2 3 5 2 + 8 a b c + 8 a b c + 8 a b c + 8 a b c + 23 a b c + 8 a b c 5 3 2 6 2 2 9 8 4 5 5 4 + 8 a b c + 23 a b c + 2 b c + 2 a b c + 12 a b c + 12 a b c 8 9 10 9 4 6 5 5 6 4 9 + 2 a b c + 2 a c + b + 2 a b + 2 a b + 12 a b + 2 a b + 2 a b 10 + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 10 9 2 2 8 (22 z + (142 y + 142 x) z + (485 y + 844 x y + 485 x ) z 3 2 2 3 7 + (1056 y + 2536 x y + 2536 x y + 1056 x ) z 4 3 2 2 3 4 6 + (1622 y + 5080 x y + 6608 x y + 5080 x y + 1622 x ) z 5 4 2 3 3 2 4 5 5 + (1872 y + 7252 x y + 11152 x y + 11152 x y + 7252 x y + 1872 x ) z 6 5 2 4 3 3 4 2 5 + (1622 y + 7252 x y + 13220 x y + 15040 x y + 13220 x y + 7252 x y 6 4 7 6 2 5 3 4 4 3 + 1622 x ) z + (1056 y + 5080 x y + 11152 x y + 15040 x y + 15040 x y 5 2 6 7 3 + 11152 x y + 5080 x y + 1056 x ) z 8 7 2 6 3 5 4 4 5 3 + (485 y + 2536 x y + 6608 x y + 11152 x y + 13220 x y + 11152 x y 6 2 7 8 2 9 8 2 7 + 6608 x y + 2536 x y + 485 x ) z + (142 y + 844 x y + 2536 x y 3 6 4 5 5 4 6 3 7 2 8 + 5080 x y + 7252 x y + 7252 x y + 5080 x y + 2536 x y + 844 x y 9 10 9 2 8 3 7 4 6 + 142 x ) z + 22 y + 142 x y + 485 x y + 1056 x y + 1622 x y 5 5 6 4 7 3 8 2 9 10 + 1872 x y + 1622 x y + 1056 x y + 485 x y + 142 x y + 22 x ) 10 9 2 2 8 /1024 >= (22 z + (142 y + 142 x) z + (485 y + 844 x y + 485 x ) z 3 2 2 3 7 + (1056 y + 2536 x y + 2536 x y + 1056 x ) z 4 3 2 2 3 4 6 + (1622 y + 4648 x y + 6768 x y + 4648 x y + 1622 x ) z 5 4 2 3 3 2 4 5 5 + (1872 y + 5956 x y + 11360 x y + 11360 x y + 5956 x y + 1872 x ) z 6 5 2 4 3 3 4 2 5 + (1622 y + 5956 x y + 13316 x y + 17824 x y + 13316 x y + 5956 x y 6 4 7 6 2 5 3 4 4 3 + 1622 x ) z + (1056 y + 4648 x y + 11360 x y + 17824 x y + 17824 x y 5 2 6 7 3 + 11360 x y + 4648 x y + 1056 x ) z 8 7 2 6 3 5 4 4 5 3 + (485 y + 2536 x y + 6768 x y + 11360 x y + 13316 x y + 11360 x y 6 2 7 8 2 9 8 2 7 + 6768 x y + 2536 x y + 485 x ) z + (142 y + 844 x y + 2536 x y 3 6 4 5 5 4 6 3 7 2 8 + 4648 x y + 5956 x y + 5956 x y + 4648 x y + 2536 x y + 844 x y 9 10 9 2 8 3 7 4 6 + 142 x ) z + 22 y + 142 x y + 485 x y + 1056 x y + 1622 x y 5 5 6 4 7 3 8 2 9 10 + 1872 x y + 1622 x y + 1056 x y + 485 x y + 142 x y + 22 x )/1024 Multiplying both sides by 1024 gives: 10 9 9 2 8 8 2 8 3 7 22 z + 142 y z + 142 x z + 485 y z + 844 x y z + 485 x z + 1056 y z 2 7 2 7 3 7 4 6 3 6 + 2536 x y z + 2536 x y z + 1056 x z + 1622 y z + 5080 x y z 2 2 6 3 6 4 6 5 5 4 5 + 6608 x y z + 5080 x y z + 1622 x z + 1872 y z + 7252 x y z 2 3 5 3 2 5 4 5 5 5 6 4 + 11152 x y z + 11152 x y z + 7252 x y z + 1872 x z + 1622 y z 5 4 2 4 4 3 3 4 4 2 4 + 7252 x y z + 13220 x y z + 15040 x y z + 13220 x y z 5 4 6 4 7 3 6 3 2 5 3 + 7252 x y z + 1622 x z + 1056 y z + 5080 x y z + 11152 x y z 3 4 3 4 3 3 5 2 3 6 3 7 3 + 15040 x y z + 15040 x y z + 11152 x y z + 5080 x y z + 1056 x z 8 2 7 2 2 6 2 3 5 2 4 4 2 + 485 y z + 2536 x y z + 6608 x y z + 11152 x y z + 13220 x y z 5 3 2 6 2 2 7 2 8 2 9 + 11152 x y z + 6608 x y z + 2536 x y z + 485 x z + 142 y z 8 2 7 3 6 4 5 5 4 + 844 x y z + 2536 x y z + 5080 x y z + 7252 x y z + 7252 x y z 6 3 7 2 8 9 10 9 + 5080 x y z + 2536 x y z + 844 x y z + 142 x z + 22 y + 142 x y 2 8 3 7 4 6 5 5 6 4 7 3 + 485 x y + 1056 x y + 1622 x y + 1872 x y + 1622 x y + 1056 x y 8 2 9 10 10 9 9 2 8 + 485 x y + 142 x y + 22 x >= 22 z + 142 y z + 142 x z + 485 y z 8 2 8 3 7 2 7 2 7 + 844 x y z + 485 x z + 1056 y z + 2536 x y z + 2536 x y z 3 7 4 6 3 6 2 2 6 3 6 + 1056 x z + 1622 y z + 4648 x y z + 6768 x y z + 4648 x y z 4 6 5 5 4 5 2 3 5 3 2 5 + 1622 x z + 1872 y z + 5956 x y z + 11360 x y z + 11360 x y z 4 5 5 5 6 4 5 4 2 4 4 + 5956 x y z + 1872 x z + 1622 y z + 5956 x y z + 13316 x y z 3 3 4 4 2 4 5 4 6 4 7 3 + 17824 x y z + 13316 x y z + 5956 x y z + 1622 x z + 1056 y z 6 3 2 5 3 3 4 3 4 3 3 + 4648 x y z + 11360 x y z + 17824 x y z + 17824 x y z 5 2 3 6 3 7 3 8 2 7 2 + 11360 x y z + 4648 x y z + 1056 x z + 485 y z + 2536 x y z 2 6 2 3 5 2 4 4 2 5 3 2 + 6768 x y z + 11360 x y z + 13316 x y z + 11360 x y z 6 2 2 7 2 8 2 9 8 + 6768 x y z + 2536 x y z + 485 x z + 142 y z + 844 x y z 2 7 3 6 4 5 5 4 6 3 + 2536 x y z + 4648 x y z + 5956 x y z + 5956 x y z + 4648 x y z 7 2 8 9 10 9 2 8 + 2536 x y z + 844 x y z + 142 x z + 22 y + 142 x y + 485 x y 3 7 4 6 5 5 6 4 7 3 8 2 + 1056 x y + 1622 x y + 1872 x y + 1622 x y + 1056 x y + 485 x y 9 10 + 142 x y + 22 x Expanding and collecting terms of the same sign gives: 3 6 3 6 4 5 4 5 5 4 432 x y z + 432 x y z + 1296 x y z + 1296 x y z + 1296 x y z 5 4 6 3 6 3 3 6 4 5 + 1296 x y z + 432 x y z + 432 x y z + 432 x y z + 1296 x y z 5 4 6 3 2 2 6 2 3 5 3 2 5 + 1296 x y z + 432 x y z >= 160 x y z + 208 x y z + 208 x y z 2 4 4 3 3 4 4 2 4 2 5 3 3 4 3 + 96 x y z + 2784 x y z + 96 x y z + 208 x y z + 2784 x y z 4 3 3 5 2 3 2 6 2 3 5 2 4 4 2 + 2784 x y z + 208 x y z + 160 x y z + 208 x y z + 96 x y z 5 3 2 6 2 2 + 208 x y z + 160 x y z Dividing both sides by 16 x y z (z + y + x) gives: 2 4 2 4 3 3 2 3 2 3 3 3 4 2 27 y z + 27 x z + 54 y z - 27 x y z - 27 x y z + 54 x z + 27 y z 3 2 2 2 2 3 2 4 2 2 3 3 2 - 27 x y z + 54 x y z - 27 x y z + 27 x z - 27 x y z - 27 x y z 2 4 3 3 4 2 4 2 3 2 3 + 27 x y + 54 x y + 27 x y >= 10 x y z + 3 x y z + 3 x y z 3 2 2 2 2 3 2 4 2 3 3 2 + 3 x y z + 168 x y z + 3 x y z + 10 x y z + 3 x y z + 3 x y z 4 + 10 x y z 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} (d13) true (c14) trineq(6*K*sqrt(3)<=27*R*r); To prove: 27 R r >= 6 sqrt(3) K Let r = K/s . Let R = a*b*c/(4*K) . We get: 27 a b c -------- >= 6 sqrt(3) K 4 s Multiplying both sides by 4 s gives: 27 a b c >= 24 sqrt(3) K s Since 24 sqrt(3) s is positive, and since 27 a b c is positive, we can square both sides to get: 2 2 2 6 5 729 a b c >= 1728 s + (- 1728 c - 1728 b - 1728 a) s 4 3 + ((1728 b + 1728 a) c + 1728 a b) s - 1728 a b c s Expanding and collecting terms of the same sign gives: 5 5 5 3 2 2 2 1728 c s + 1728 b s + 1728 a s + 1728 a b c s + 729 a b c >= 6 4 4 4 1728 s + 1728 b c s + 1728 a c s + 1728 a b s Dividing both sides by 27 gives: 5 5 5 3 2 2 2 64 c s + 64 b s + 64 a s + 64 a b c s + 27 a b c >= 6 4 4 4 64 s + 64 b c s + 64 a c s + 64 a b s Let s = (c+b+a)/2 . We get: 6 5 2 2 4 2 c + (12 b + 12 a) c + (30 b + 68 a b + 30 a ) c 3 2 2 3 3 + (40 b + 144 a b + 144 a b + 40 a ) c 4 3 2 2 3 4 2 + (30 b + 144 a b + 255 a b + 144 a b + 30 a ) c 5 4 2 3 3 2 4 5 6 + (12 b + 68 a b + 144 a b + 144 a b + 68 a b + 12 a ) c + 2 b 5 2 4 3 3 4 2 5 6 + 12 a b + 30 a b + 40 a b + 30 a b + 12 a b + 2 a >= 6 5 2 2 4 c + (10 b + 10 a) c + (31 b + 66 a b + 31 a ) c 3 2 2 3 3 + (44 b + 148 a b + 148 a b + 44 a ) c 4 3 2 2 3 4 2 + (31 b + 148 a b + 234 a b + 148 a b + 31 a ) c 5 4 2 3 3 2 4 5 6 5 + (10 b + 66 a b + 148 a b + 148 a b + 66 a b + 10 a ) c + b + 10 a b 2 4 3 3 4 2 5 6 + 31 a b + 44 a b + 31 a b + 10 a b + a Expanding and collecting terms of the same sign gives: 6 5 5 4 2 2 2 5 4 4 c + 2 b c + 2 a c + 2 a b c + 21 a b c + 2 b c + 2 a b c + 2 a b c 5 6 5 5 6 + 2 a c + b + 2 a b + 2 a b + a >= 2 4 2 4 3 3 2 3 2 3 3 3 4 2 3 2 b c + a c + 4 b c + 4 a b c + 4 a b c + 4 a c + b c + 4 a b c 3 2 4 2 2 3 3 2 2 4 3 3 4 2 + 4 a b c + a c + 4 a b c + 4 a b c + a b + 4 a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 6 5 2 2 4 (3 z + (13 y + 13 x) z + (38 y + 51 x y + 38 x ) z 3 2 2 3 3 + (57 y + 97 x y + 97 x y + 57 x ) z 4 3 2 2 3 4 2 + (38 y + 97 x y + 123 x y + 97 x y + 38 x ) z 5 4 2 3 3 2 4 5 6 5 + (13 y + 51 x y + 97 x y + 97 x y + 51 x y + 13 x ) z + 3 y + 13 x y 2 4 3 3 4 2 5 6 + 38 x y + 57 x y + 38 x y + 13 x y + 3 x )/32 >= 6 5 2 2 4 (6 z + (26 y + 26 x) z + (49 y + 112 x y + 49 x ) z 3 2 2 3 3 + (60 y + 224 x y + 224 x y + 60 x ) z 4 3 2 2 3 4 2 + (49 y + 224 x y + 360 x y + 224 x y + 49 x ) z 5 4 2 3 3 2 4 5 6 + (26 y + 112 x y + 224 x y + 224 x y + 112 x y + 26 x ) z + 6 y 5 2 4 3 3 4 2 5 6 + 26 x y + 49 x y + 60 x y + 49 x y + 26 x y + 6 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 6 z + 26 y z + 26 x z + 76 y z + 102 x y z + 76 x z + 114 y z 2 3 2 3 3 3 4 2 3 2 + 194 x y z + 194 x y z + 114 x z + 76 y z + 194 x y z 2 2 2 3 2 4 2 5 4 2 3 + 246 x y z + 194 x y z + 76 x z + 26 y z + 102 x y z + 194 x y z 3 2 4 5 6 5 2 4 3 3 + 194 x y z + 102 x y z + 26 x z + 6 y + 26 x y + 76 x y + 114 x y 4 2 5 6 6 5 5 2 4 + 76 x y + 26 x y + 6 x >= 6 z + 26 y z + 26 x z + 49 y z 4 2 4 3 3 2 3 2 3 3 3 + 112 x y z + 49 x z + 60 y z + 224 x y z + 224 x y z + 60 x z 4 2 3 2 2 2 2 3 2 4 2 5 + 49 y z + 224 x y z + 360 x y z + 224 x y z + 49 x z + 26 y z 4 2 3 3 2 4 5 6 + 112 x y z + 224 x y z + 224 x y z + 112 x y z + 26 x z + 6 y 5 2 4 3 3 4 2 5 6 + 26 x y + 49 x y + 60 x y + 49 x y + 26 x y + 6 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 27 y z + 27 x z + 54 y z + 54 x z + 27 y z + 27 x z + 27 x y 3 3 4 2 4 2 3 2 3 3 2 + 54 x y + 27 x y >= 10 x y z + 30 x y z + 30 x y z + 30 x y z 2 2 2 3 2 4 2 3 3 2 4 + 114 x y z + 30 x y z + 10 x y z + 30 x y z + 30 x y z + 10 x y z Expressing in terms of symmetric polynomials gives: 27 {4, 2, 0} + 27 {3, 3, 0} >= 5 {4, 1, 1} + 30 {3, 2, 1} + 19 {2, 2, 2} This follows from the following majorizations: 5 {4, 2, 0} >= 5 {4, 1, 1} 22 {4, 2, 0} >= 22 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} 19 {3, 3, 0} >= 19 {2, 2, 2} (d14) true (c15) /* 6.16 */ trineq(cprod(h(a))>=27*r^3); 3 8 K 3 To prove: ----- >= 27 r a b c Let r = K/s . We get: 3 3 8 K 27 K ----- >= ----- a b c 3 s 3 Multiplying both sides by a b c s gives: 3 3 3 8 K s >= 27 K a b c Replacing K^2 by F^2 gives: 2 3 2 8 F K s >= 27 F K a b c left side: [6 {2, 1, 1}, 3 {2, 2, 0}] right side: [5 {3, 1, 0}, 4 {4, 0, 0}] Bringing all terms involving K to the left side yields: 2 3 2 8 F K s - 27 F K a b c >= 0 2 3 2 Since 8 F s - 27 F a b c is positive, and since 0 is positive, we can square both sides to get: 4 10 4 4 4 9 64 F s + (- 64 F c - 64 F b - 64 F a) s 4 4 4 8 4 7 + ((64 F b + 64 F a) c + 64 F a b) s - 496 F a b c s 4 2 4 2 4 2 6 + (432 F a b c + (432 F a b + 432 F a b) c) s 4 2 4 2 2 4 2 2 5 4 2 2 2 4 + ((- 432 F a b - 432 F a b) c - 432 F a b c) s + 1161 F a b c s 4 2 3 4 3 2 2 4 2 2 3 3 + ((- 729 F a b - 729 F a b ) c - 729 F a b c ) s 4 2 3 4 3 2 3 4 3 3 2 2 + ((729 F a b + 729 F a b ) c + 729 F a b c ) s 4 3 3 3 - 729 F a b c s >= 0 Expanding and collecting terms of the same sign gives: 4 10 4 8 4 8 4 8 4 2 6 64 F s + 64 F b c s + 64 F a c s + 64 F a b s + 432 F a b c s 4 2 6 4 2 6 4 2 2 2 4 + 432 F a b c s + 432 F a b c s + 1161 F a b c s 4 2 3 3 2 4 3 2 3 2 4 3 3 2 2 + 729 F a b c s + 729 F a b c s + 729 F a b c s >= 4 9 4 9 4 9 4 7 4 2 2 5 64 F c s + 64 F b s + 64 F a s + 496 F a b c s + 432 F a b c s 4 2 2 5 4 2 2 5 4 2 2 3 3 + 432 F a b c s + 432 F a b c s + 729 F a b c s 4 2 3 2 3 4 3 2 2 3 4 3 3 3 + 729 F a b c s + 729 F a b c s + 729 F a b c s 4 Dividing both sides by F s gives: 9 7 7 7 2 5 2 5 64 s + 64 b c s + 64 a c s + 64 a b s + 432 a b c s + 432 a b c s 2 5 2 2 2 3 2 3 3 3 2 3 + 432 a b c s + 1161 a b c s + 729 a b c s + 729 a b c s 3 3 2 8 8 8 6 + 729 a b c s >= 64 c s + 64 b s + 64 a s + 496 a b c s 2 2 4 2 2 4 2 2 4 2 2 3 2 + 432 a b c s + 432 a b c s + 432 a b c s + 729 a b c s 2 3 2 2 3 2 2 2 3 3 3 + 729 a b c s + 729 a b c s + 729 a b c Let s = (c+b+a)/2 . We get: 9 8 2 2 7 (c + (13 b + 13 a) c + (64 b + 240 a b + 64 a ) c 3 2 2 3 6 + (168 b + 1180 a b + 1180 a b + 168 a ) c 4 3 2 2 3 4 5 + (266 b + 2768 a b + 6165 a b + 2768 a b + 266 a ) c 5 4 2 3 3 2 4 5 4 + (266 b + 3630 a b + 15959 a b + 15959 a b + 3630 a b + 266 a ) c 6 5 2 4 3 3 4 2 5 + (168 b + 2768 a b + 15959 a b + 29634 a b + 15959 a b + 2768 a b 6 3 7 6 2 5 3 4 4 3 + 168 a ) c + (64 b + 1180 a b + 6165 a b + 15959 a b + 15959 a b 5 2 6 7 2 8 7 2 6 + 6165 a b + 1180 a b + 64 a ) c + (13 b + 240 a b + 1180 a b 3 5 4 4 5 3 6 2 7 8 9 + 2768 a b + 3630 a b + 2768 a b + 1180 a b + 240 a b + 13 a ) c + b 8 2 7 3 6 4 5 5 4 6 3 + 13 a b + 64 a b + 168 a b + 266 a b + 266 a b + 168 a b 7 2 8 9 9 8 + 64 a b + 13 a b + a )/8 >= (c + (9 b + 9 a) c 2 2 7 3 2 2 3 6 + (36 b + 103 a b + 36 a ) c + (84 b + 546 a b + 546 a b + 84 a ) c 4 3 2 2 3 4 5 + (126 b + 1401 a b + 3387 a b + 1401 a b + 126 a ) c 5 4 2 3 3 2 4 5 4 + (126 b + 1898 a b + 7683 a b + 7683 a b + 1898 a b + 126 a ) c 6 5 2 4 3 3 4 2 5 + (84 b + 1401 a b + 7683 a b + 15648 a b + 7683 a b + 1401 a b 6 3 7 6 2 5 3 4 4 3 + 84 a ) c + (36 b + 546 a b + 3387 a b + 7683 a b + 7683 a b 5 2 6 7 2 8 7 2 6 + 3387 a b + 546 a b + 36 a ) c + (9 b + 103 a b + 546 a b 3 5 4 4 5 3 6 2 7 8 9 + 1401 a b + 1898 a b + 1401 a b + 546 a b + 103 a b + 9 a ) c + b 8 2 7 3 6 4 5 5 4 6 3 7 2 + 9 a b + 36 a b + 84 a b + 126 a b + 126 a b + 84 a b + 36 a b 8 9 + 9 a b + a )/4 Multiplying both sides by 8 gives: 9 8 8 2 7 7 2 7 3 6 c + 13 b c + 13 a c + 64 b c + 240 a b c + 64 a c + 168 b c 2 6 2 6 3 6 4 5 3 5 + 1180 a b c + 1180 a b c + 168 a c + 266 b c + 2768 a b c 2 2 5 3 5 4 5 5 4 4 4 + 6165 a b c + 2768 a b c + 266 a c + 266 b c + 3630 a b c 2 3 4 3 2 4 4 4 5 4 6 3 + 15959 a b c + 15959 a b c + 3630 a b c + 266 a c + 168 b c 5 3 2 4 3 3 3 3 4 2 3 + 2768 a b c + 15959 a b c + 29634 a b c + 15959 a b c 5 3 6 3 7 2 6 2 2 5 2 + 2768 a b c + 168 a c + 64 b c + 1180 a b c + 6165 a b c 3 4 2 4 3 2 5 2 2 6 2 7 2 + 15959 a b c + 15959 a b c + 6165 a b c + 1180 a b c + 64 a c 8 7 2 6 3 5 4 4 + 13 b c + 240 a b c + 1180 a b c + 2768 a b c + 3630 a b c 5 3 6 2 7 8 9 8 2 7 + 2768 a b c + 1180 a b c + 240 a b c + 13 a c + b + 13 a b + 64 a b 3 6 4 5 5 4 6 3 7 2 8 9 + 168 a b + 266 a b + 266 a b + 168 a b + 64 a b + 13 a b + a >= 9 8 8 2 7 7 2 7 3 6 2 c + 18 b c + 18 a c + 72 b c + 206 a b c + 72 a c + 168 b c 2 6 2 6 3 6 4 5 3 5 + 1092 a b c + 1092 a b c + 168 a c + 252 b c + 2802 a b c 2 2 5 3 5 4 5 5 4 4 4 + 6774 a b c + 2802 a b c + 252 a c + 252 b c + 3796 a b c 2 3 4 3 2 4 4 4 5 4 6 3 + 15366 a b c + 15366 a b c + 3796 a b c + 252 a c + 168 b c 5 3 2 4 3 3 3 3 4 2 3 + 2802 a b c + 15366 a b c + 31296 a b c + 15366 a b c 5 3 6 3 7 2 6 2 2 5 2 + 2802 a b c + 168 a c + 72 b c + 1092 a b c + 6774 a b c 3 4 2 4 3 2 5 2 2 6 2 7 2 + 15366 a b c + 15366 a b c + 6774 a b c + 1092 a b c + 72 a c 8 7 2 6 3 5 4 4 + 18 b c + 206 a b c + 1092 a b c + 2802 a b c + 3796 a b c 5 3 6 2 7 8 9 8 + 2802 a b c + 1092 a b c + 206 a b c + 18 a c + 2 b + 18 a b 2 7 3 6 4 5 5 4 6 3 7 2 + 72 a b + 168 a b + 252 a b + 252 a b + 168 a b + 72 a b 8 9 + 18 a b + 2 a Expanding and collecting terms of the same sign gives: 7 2 6 2 6 4 5 4 5 5 4 34 a b c + 88 a b c + 88 a b c + 14 b c + 14 a c + 14 b c 2 3 4 3 2 4 5 4 2 4 3 4 2 3 + 593 a b c + 593 a b c + 14 a c + 593 a b c + 593 a b c 6 2 3 4 2 4 3 2 6 2 7 + 88 a b c + 593 a b c + 593 a b c + 88 a b c + 34 a b c 2 6 6 2 7 4 5 5 4 + 88 a b c + 88 a b c + 34 a b c + 14 a b + 14 a b >= 9 8 8 2 7 2 7 3 5 2 2 5 c + 5 b c + 5 a c + 8 b c + 8 a c + 34 a b c + 609 a b c 3 5 4 4 4 4 5 3 3 3 3 + 34 a b c + 166 a b c + 166 a b c + 34 a b c + 1662 a b c 5 3 7 2 2 5 2 5 2 2 7 2 8 + 34 a b c + 8 b c + 609 a b c + 609 a b c + 8 a c + 5 b c 3 5 4 4 5 3 8 9 8 2 7 + 34 a b c + 166 a b c + 34 a b c + 5 a c + b + 5 a b + 8 a b 7 2 8 9 + 8 a b + 5 a b + a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 9 8 2 2 7 (28 z + (370 y + 370 x) z + (2562 y + 5236 x y + 2562 x ) z 3 2 2 3 6 + (8271 y + 23549 x y + 23549 x y + 8271 x ) z 4 3 2 2 3 4 5 + (14463 y + 55362 x y + 81966 x y + 55362 x y + 14463 x ) z 5 4 2 3 3 2 4 + (14463 y + 73386 x y + 146503 x y + 146503 x y + 73386 x y 5 4 6 5 2 4 3 3 + 14463 x ) z + (8271 y + 55362 x y + 146503 x y + 198936 x y 4 2 5 6 3 + 146503 x y + 55362 x y + 8271 x ) z 7 6 2 5 3 4 4 3 + (2562 y + 23549 x y + 81966 x y + 146503 x y + 146503 x y 5 2 6 7 2 + 81966 x y + 23549 x y + 2562 x ) z 8 7 2 6 3 5 4 4 5 3 + (370 y + 5236 x y + 23549 x y + 55362 x y + 73386 x y + 55362 x y 6 2 7 8 9 8 2 7 + 23549 x y + 5236 x y + 370 x ) z + 28 y + 370 x y + 2562 x y 3 6 4 5 5 4 6 3 7 2 8 + 8271 x y + 14463 x y + 14463 x y + 8271 x y + 2562 x y + 370 x y 9 9 8 + 28 x )/512 >= (28 z + (370 y + 370 x) z 2 2 7 3 2 2 + (2562 y + 4724 x y + 2562 x ) z + (8271 y + 23933 x y + 23933 x y 3 6 4 3 2 2 3 4 + 8271 x ) z + (14463 y + 55674 x y + 82590 x y + 55674 x y + 14463 x ) 5 5 4 2 3 3 2 4 z + (14463 y + 72218 x y + 146455 x y + 146455 x y + 72218 x y 5 4 6 5 2 4 3 3 + 14463 x ) z + (8271 y + 55674 x y + 146455 x y + 198216 x y 4 2 5 6 3 + 146455 x y + 55674 x y + 8271 x ) z 7 6 2 5 3 4 4 3 + (2562 y + 23933 x y + 82590 x y + 146455 x y + 146455 x y 5 2 6 7 2 + 82590 x y + 23933 x y + 2562 x ) z 8 7 2 6 3 5 4 4 5 3 + (370 y + 4724 x y + 23933 x y + 55674 x y + 72218 x y + 55674 x y 6 2 7 8 9 8 2 7 + 23933 x y + 4724 x y + 370 x ) z + 28 y + 370 x y + 2562 x y 3 6 4 5 5 4 6 3 7 2 8 + 8271 x y + 14463 x y + 14463 x y + 8271 x y + 2562 x y + 370 x y 9 + 28 x )/512 Multiplying both sides by 512 gives: 9 8 8 2 7 7 2 7 28 z + 370 y z + 370 x z + 2562 y z + 5236 x y z + 2562 x z 3 6 2 6 2 6 3 6 4 5 + 8271 y z + 23549 x y z + 23549 x y z + 8271 x z + 14463 y z 3 5 2 2 5 3 5 4 5 5 4 + 55362 x y z + 81966 x y z + 55362 x y z + 14463 x z + 14463 y z 4 4 2 3 4 3 2 4 4 4 + 73386 x y z + 146503 x y z + 146503 x y z + 73386 x y z 5 4 6 3 5 3 2 4 3 3 3 3 + 14463 x z + 8271 y z + 55362 x y z + 146503 x y z + 198936 x y z 4 2 3 5 3 6 3 7 2 6 2 + 146503 x y z + 55362 x y z + 8271 x z + 2562 y z + 23549 x y z 2 5 2 3 4 2 4 3 2 5 2 2 + 81966 x y z + 146503 x y z + 146503 x y z + 81966 x y z 6 2 7 2 8 7 2 6 + 23549 x y z + 2562 x z + 370 y z + 5236 x y z + 23549 x y z 3 5 4 4 5 3 6 2 7 + 55362 x y z + 73386 x y z + 55362 x y z + 23549 x y z + 5236 x y z 8 9 8 2 7 3 6 4 5 + 370 x z + 28 y + 370 x y + 2562 x y + 8271 x y + 14463 x y 5 4 6 3 7 2 8 9 + 14463 x y + 8271 x y + 2562 x y + 370 x y + 28 x >= 9 8 8 2 7 7 2 7 28 z + 370 y z + 370 x z + 2562 y z + 4724 x y z + 2562 x z 3 6 2 6 2 6 3 6 4 5 + 8271 y z + 23933 x y z + 23933 x y z + 8271 x z + 14463 y z 3 5 2 2 5 3 5 4 5 5 4 + 55674 x y z + 82590 x y z + 55674 x y z + 14463 x z + 14463 y z 4 4 2 3 4 3 2 4 4 4 + 72218 x y z + 146455 x y z + 146455 x y z + 72218 x y z 5 4 6 3 5 3 2 4 3 3 3 3 + 14463 x z + 8271 y z + 55674 x y z + 146455 x y z + 198216 x y z 4 2 3 5 3 6 3 7 2 6 2 + 146455 x y z + 55674 x y z + 8271 x z + 2562 y z + 23933 x y z 2 5 2 3 4 2 4 3 2 5 2 2 + 82590 x y z + 146455 x y z + 146455 x y z + 82590 x y z 6 2 7 2 8 7 2 6 + 23933 x y z + 2562 x z + 370 y z + 4724 x y z + 23933 x y z 3 5 4 4 5 3 6 2 7 + 55674 x y z + 72218 x y z + 55674 x y z + 23933 x y z + 4724 x y z 8 9 8 2 7 3 6 4 5 + 370 x z + 28 y + 370 x y + 2562 x y + 8271 x y + 14463 x y 5 4 6 3 7 2 8 9 + 14463 x y + 8271 x y + 2562 x y + 370 x y + 28 x Expanding and collecting terms of the same sign gives: 7 4 4 2 3 4 3 2 4 4 4 512 x y z + 1168 x y z + 48 x y z + 48 x y z + 1168 x y z 2 4 3 3 3 3 4 2 3 3 4 2 4 3 2 + 48 x y z + 720 x y z + 48 x y z + 48 x y z + 48 x y z 7 4 4 7 + 512 x y z + 1168 x y z + 512 x y z >= 2 6 2 6 3 5 2 2 5 3 5 384 x y z + 384 x y z + 312 x y z + 624 x y z + 312 x y z 5 3 5 3 6 2 2 5 2 5 2 2 + 312 x y z + 312 x y z + 384 x y z + 624 x y z + 624 x y z 6 2 2 6 3 5 5 3 6 2 + 384 x y z + 384 x y z + 312 x y z + 312 x y z + 384 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 64 z + 146 y z + 6 x y z + 6 x y z + 146 x z + 6 x y z + 90 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 + 64 y + 146 x y + 64 x >= 5 5 2 4 4 2 4 4 2 4 2 48 y z + 48 x z + 39 y z + 78 x y z + 39 x z + 39 y z + 39 x z 5 4 4 5 5 2 4 4 2 + 48 y z + 78 x y z + 78 x y z + 48 x z + 48 x y + 39 x y + 39 x y 5 + 48 x y Expressing in terms of symmetric polynomials gives: 32 {6, 0, 0} + 73 {3, 3, 0} + 6 {3, 2, 1} + 15 {2, 2, 2} >= 48 {5, 1, 0} + 39 {4, 2, 0} + 39 {4, 1, 1} This follows from the following majorizations: 15 {6, 0, 0} + 15 {2, 2, 2} >= 30 {4, 2, 0} 17 {6, 0, 0} >= 17 {5, 1, 0} left side: [15 {2, 2, 2}, 6 {3, 2, 1}, 73 {3, 3, 0}, 32 {6, 0, 0}] right side: [39 {4, 1, 1}, 39 {4, 2, 0}, 48 {5, 1, 0}] (d15) notsure (c16) /* 6.21 */ trineq(csum(1/(h(a)-2*r))>=3/r); 1 1 1 3 To prove: --------- + --------- + --------- >= - 2 K 2 K 2 K r --- - 2 r --- - 2 r --- - 2 r c b a Expanding and collecting terms of the same sign gives: 2 4 3 3 3 2 2 8 K b c r /(2 a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 2 K c r 2 2 2 2 3 2 + 2 K b r + 2 K a r - 2 K r) + 8 K a c r 4 3 3 3 2 2 2 2 /(2 a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 2 K c r + 2 K b r 2 2 3 2 4 3 3 + 2 K a r - 2 K r) + 8 K a b r /(2 a b c r - 2 K b c r - 2 K a c r 3 2 2 2 2 2 2 3 - 2 K a b r + 2 K c r + 2 K b r + 2 K a r - 2 K r) 3 4 3 3 3 2 2 + 6 K /(2 a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 2 K c r 2 2 2 2 3 3 + 2 K b r + 2 K a r - 2 K r) >= 9 a b c r 4 3 3 3 2 2 2 2 /(2 a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 2 K c r + 2 K b r 2 2 3 2 4 3 3 + 2 K a r - 2 K r) + 7 K c r/(2 a b c r - 2 K b c r - 2 K a c r 3 2 2 2 2 2 2 3 - 2 K a b r + 2 K c r + 2 K b r + 2 K a r - 2 K r) 2 4 3 3 3 2 2 + 7 K b r/(2 a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 2 K c r 2 2 2 2 3 2 + 2 K b r + 2 K a r - 2 K r) + 7 K a r 4 3 3 3 2 2 2 2 /(2 a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 2 K c r + 2 K b r 2 2 3 + 2 K a r - 2 K r) Let r = K/s . We get: 4 2 3 s + ((4 b + 4 a) c + 4 a b) s - ------------------------------------------------------------------- >= 3 2 K s + (- K c - K b - K a) s + ((K b + K a) c + K a b) s - K a b c 3 3 2 - ((7 c + 7 b + 7 a) s + 9 a b c s)/(2 K s + (- 2 K c - 2 K b - 2 K a) s + ((2 K b + 2 K a) c + 2 K a b) s - 2 K a b c) Multiplying both sides by 2 K (s - a) (s - b) (s - c) gives: 4 2 2 2 - 6 s - 8 b c s - 8 a c s - 8 a b s >= 3 3 3 - 7 c s - 7 b s - 7 a s - 9 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 7 c s + 7 b s + 7 a s + 9 a b c s >= 6 s + 8 b c s + 8 a c s + 8 a b s Let s = (c+b+a)/2 . We get: 4 3 2 2 2 (7 c + (28 b + 28 a) c + (42 b + 120 a b + 42 a ) c 3 2 2 3 4 3 2 2 + (28 b + 120 a b + 120 a b + 28 a ) c + 7 b + 28 a b + 42 a b 3 4 4 3 2 2 2 + 28 a b + 7 a )/8 >= (3 c + (28 b + 28 a) c + (50 b + 116 a b + 50 a ) c 3 2 2 3 4 3 2 2 + (28 b + 116 a b + 116 a b + 28 a ) c + 3 b + 28 a b + 50 a b 3 4 + 28 a b + 3 a )/8 Multiplying both sides by 8 gives: 4 3 3 2 2 2 2 2 3 7 c + 28 b c + 28 a c + 42 b c + 120 a b c + 42 a c + 28 b c 2 2 3 4 3 2 2 3 + 120 a b c + 120 a b c + 28 a c + 7 b + 28 a b + 42 a b + 28 a b 4 4 3 3 2 2 2 2 2 + 7 a >= 3 c + 28 b c + 28 a c + 50 b c + 116 a b c + 50 a c 3 2 2 3 4 3 2 2 + 28 b c + 116 a b c + 116 a b c + 28 a c + 3 b + 28 a b + 50 a b 3 4 + 28 a b + 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 4 c + 4 a b c + 4 a b c + 4 a b c + 4 b + 4 a >= 2 2 2 2 2 2 8 b c + 8 a c + 8 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 /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 )/2 Multiplying both sides by 2 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. (d16) true (c17) /* 6.22 */ trineq(csum((h(a)+r)/(h(a)-r))>=6); 2 K 2 K 2 K r + --- r + --- r + --- c b a To prove: ------- + ------- + ------- >= 6 2 K 2 K 2 K --- - r --- - r --- - r c b a Expanding and collecting terms of the same sign gives: 2 3 2 2 2 2 14 K b c r /(a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 4 K c r 2 2 3 2 + 4 K b r + 4 K a r - 8 K ) + 14 K a c r 3 2 2 2 2 2 /(a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 4 K c r + 4 K b r 2 3 2 3 2 2 + 4 K a r - 8 K ) + 14 K a b r /(a b c r - 2 K b c r - 2 K a c r 2 2 2 2 3 - 2 K a b r + 4 K c r + 4 K b r + 4 K a r - 8 K ) 3 3 2 2 2 2 2 + 24 K /(a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 4 K c r + 4 K b r 2 3 3 3 2 2 + 4 K a r - 8 K ) >= 9 a b c r /(a b c r - 2 K b c r - 2 K a c r 2 2 2 2 3 - 2 K a b r + 4 K c r + 4 K b r + 4 K a r - 8 K ) 2 3 2 2 2 2 + 20 K c r/(a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 4 K c r 2 2 3 2 + 4 K b r + 4 K a r - 8 K ) + 20 K b r 3 2 2 2 2 2 /(a b c r - 2 K b c r - 2 K a c r - 2 K a b r + 4 K c r + 4 K b r 2 3 2 3 2 2 + 4 K a r - 8 K ) + 20 K a r/(a b c r - 2 K b c r - 2 K a c r 2 2 2 2 3 - 2 K a b r + 4 K c r + 4 K b r + 4 K a r - 8 K ) Let r = K/s . We get: 3 24 s + ((14 b + 14 a) c + 14 a b) s - ----------------------------------------------------------------- >= 3 2 8 s + (- 4 c - 4 b - 4 a) s + ((2 b + 2 a) c + 2 a b) s - a b c 2 (20 c + 20 b + 20 a) s + 9 a b c - ----------------------------------------------------------------- 3 2 8 s + (- 4 c - 4 b - 4 a) s + ((2 b + 2 a) c + 2 a b) s - a b c Multiplying both sides by (2 s - a) (2 s - b) (2 s - c) gives: 3 - 24 s - 14 b c s - 14 a c s - 14 a b s >= 2 2 2 - 20 c s - 20 b s - 20 a s - 9 a b c Expanding and collecting terms of the same sign gives: 2 2 2 3 20 c s + 20 b s + 20 a s + 9 a b c >= 24 s + 14 b c s + 14 a c s + 14 a b s Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 2 5 c + (15 b + 15 a) c + (15 b + 39 a b + 15 a ) c + 5 b + 15 a b + 15 a b 3 3 2 2 2 3 + 5 a >= 3 c + (16 b + 16 a) c + (16 b + 39 a b + 16 a ) c + 3 b 2 2 3 + 16 a b + 16 a b + 3 a Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 2 c + 2 b + 2 a >= b c + a c + b c + a c + a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 2 3 2 z + (3 y + 3 x) z + (3 y + 3 x ) z + 2 y + 3 x y + 3 x y + 2 x ----------------------------------------------------------------------- >= 4 3 2 2 2 3 2 2 (2 z + (5 y + 5 x) z + (5 y + 12 x y + 5 x ) z + 2 y + 5 x y + 5 x y 3 + 2 x )/8 Multiplying both sides by 8 gives: 3 2 2 2 2 3 2 2 3 4 z + 6 y z + 6 x z + 6 y z + 6 x z + 4 y + 6 x y + 6 x y + 4 x >= 3 2 2 2 2 3 2 2 2 z + 5 y z + 5 x z + 5 y z + 12 x y z + 5 x z + 2 y + 5 x y + 5 x y 3 + 2 x Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 2 z + y z + x z + y z + x z + 2 y + x y + x y + 2 x >= 12 x y z Expressing in terms of symmetric polynomials gives: {3, 0, 0} + {2, 1, 0} >= 2 {1, 1, 1} This follows from the following majorizations: {2, 1, 0} >= {1, 1, 1} {3, 0, 0} >= {1, 1, 1} (d17) true (c18) print("Summary:") $ Summary: (c19) print("Proved",triangtrue,"inequalities out of",triangcount,".") $ Proved 9 inequalities out of 14 . (d20) BATCH DONE (c21)