本日のC.A.D.

$a,\ b,\ c$ が実数のとき，次の $(1),\ (2)$ は等価です．

$\displaystyle a>1\ \land\ b>1\ \land\ c>1\ \land\ 1>\frac{1}{a}+\frac{1}{a}+\frac{1}{c}\ \ \cdots\ \ (1)$

$\forall x\ \forall y\ \forall z\ \left(\ x+y+z=1\to ax^2+by^2+cz^2>1\ \right)\ \ \cdots\ \ (2)$

? tst12([all,all,all,all,all],[a,b,c,x,y],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"1<a,1<b,1<c,a*b+b*c+c*a<a*b*c,a*x^2+b*y^2+c*(1-x-y)^2>1",23);Ans();
[[],[[a,1,5],[b,1,5],[c,1,10],[x,2,4],[y,2,4]]]
 *** reordering by degree+occurrence.
 *** using Lazard's method (MPP17).
[y,1]
[x,2]
[b,5]
[a,6]
[c,5]
time = 86 ms.
11 125(0,12) 1165(0,139) 6989(568,224) 26427(2822,0) 
 *** combined adjacent 26426 cells.
1[true,true,true,true,true]
time = 3,781 ms.

? tst12([ex,ex,ex,all,all],[a,b,c,x,y],and,"a*x^2+b*y^2+c*(1-x-y)^2>1,a<=1");Ans();
 *** using Lazard's method (MPP17).
[y,1]
[x,2]
[c,7]
[b,8]
[a,7]
time = 56 ms.
12 172(0,22) 2194(0,244) 11434(904,376) 0(302,0) 
1[false]
time = 1,227 ms.

? tst12([ex,ex,ex,all,all],[a,b,c,x,y],and,"a*x^2+b*y^2+c*(1-x-y)^2>1,a*b*c<=a*b+b*c+c*a");Ans();
 *** using Lazard's method (MPP17).
[y,1]
[x,2]
[c,7]
[b,8]
[a,7]
time = 81 ms.
15 219(0,26) 1094(0,295) 6340(552,324) 0(654,0) 
1[false]
time = 768 ms.

なお，今回の主張自体は，例えば，$(1)\ \to\ (2)$ では Cauchy–Schwarz の不等式，$(2)\ \to\ (1)$ では $x,\ y,\ z$ として $1,\ 0,\ 0$ や $\frac{1/a}{(1/a)+(1/b)+(1/c)},\ \frac{1/b}{(1/a)+(1/b)+(1/c)},\ \frac{1/c}{(1/a)+(1/b)+(1/c)}$ などを用いれば見易いです．