判定四次方程至少有一个实根

hbghlyj

$x^4 + qx^2 + rx + s$ 没有实根 $\iff\Delta>0\land(q \geq 0 \lor s > \frac{q^2}{4})$
$x^4 + qx^2 + rx + s$ 有实根 $\iff\Delta \leq 0\lor(q < 0 \land s \leq \frac{q^2}{4})$
$x^4+px^3+qx^2+rx+s$ 有实根 $\iff\Delta \leq 0\lor(8q-3 p^2<0\land -3 p^4+16 p^2 q-16 p r-16 q^2+64 s \leq 0)$

hbghlyj

这个问题，全部展开的话：

1. NMinValue[{24 s1^2+22 s1^4+28 s1^6+92 s1^8+68 s1^10+6 s1^12-72 s2-140 s1^2 s2-196 s1^4 s2-748 s1^6 s2-708 s1^8 s2-88 s1^10 s2-138 s2^2+645 s1^2 s2^2+1356 s1^4 s2^2+1846 s1^6 s2^2+198 s1^8 s2^2-35 s1^10 s2^2+436 s2^3-128 s1^2 s2^3-332 s1^4 s2^3+792 s1^6 s2^3+352 s1^8 s2^3+398 s2^4-764 s1^2 s2^4-1312 s1^4 s2^4-616 s1^6 s2^4+90 s1^8 s2^4-832 s2^5-168 s1^2 s2^5-380 s1^4 s2^5-540 s1^6 s2^5-436 s2^6+230 s1^2 s2^6+356 s1^4 s2^6-122 s1^6 s2^6+664 s2^7+448 s1^2 s2^7+396 s1^4 s2^7+236 s2^8+28 s1^2 s2^8+90 s1^4 s2^8-216 s2^9-140 s1^2 s2^9-66 s2^10-35 s1^2 s2^10+20 s2^11+6 s2^12+1080 s1 s3-1664 s1^3 s3+1708 s1^5 s3+2364 s1^7 s3+492 s1^9 s3+20 s1^11 s3+1014 s1 s2 s3-2504 s1^3 s2 s3-10028 s1^5 s2 s3-2376 s1^7 s2 s3+6 s1^9 s2 s3-6296 s1 s2^2 s3+848 s1^3 s2^2 s3-5716 s1^5 s2^2 s3-3000 s1^7 s2^2 s3-140 s1^9 s2^2 s3-104 s1 s2^3 s3+3656 s1^3 s2^3 s3+6152 s1^5 s2^3 s3+56 s1^7 s2^3 s3+7600 s1 s2^4 s3+4160 s1^3 s2^4 s3+4772 s1^5 s2^4 s3+396 s1^7 s2^4 s3+244 s1 s2^5 s3-1464 s1^3 s2^5 s3-188 s1^5 s2^5 s3-4176 s1 s2^6 s3-3440 s1^3 s2^6 s3-540 s1^5 s2^6 s3-392 s1 s2^7 s3+56 s1^3 s2^7 s3+1112 s1 s2^8 s3+352 s1^3 s2^8 s3+6 s1 s2^9 s3-88 s1 s2^10 s3-999 s3^2+918 s1^2 s3^2+9454 s1^4 s3^2+484 s1^6 s3^2-959 s1^8 s3^2-66 s1^10 s3^2-2628 s2 s3^2+12632 s1^2 s2 s3^2+46884 s1^4 s2 s3^2+18480 s1^6 s2 s3^2+1112 s1^8 s2 s3^2+9000 s2^2 s3^2-8200 s1^2 s2^2 s3^2-28412 s1^4 s2^2 s3^2-1448 s1^6 s2^2 s3^2+28 s1^8 s2^2 s3^2+1904 s2^3 s3^2-14760 s1^2 s2^3 s3^2-27800 s1^4 s2^3 s3^2-3440 s1^6 s2^3 s3^2-14546 s2^4 s3^2-1708 s1^2 s2^4 s3^2+6342 s1^4 s2^4 s3^2+356 s1^6 s2^4 s3^2+2712 s2^5 s3^2+15368 s1^2 s2^5 s3^2+4772 s1^4 s2^5 s3^2+8588 s2^6 s3^2-1448 s1^2 s2^6 s3^2-616 s1^4 s2^6 s3^2-3632 s2^7 s3^2-3000 s1^2 s2^7 s3^2-959 s2^8 s3^2+198 s1^2 s2^8 s3^2+492 s2^9 s3^2+68 s2^10 s3^2+16236 s1 s3^3-86824 s1^3 s3^3-36988 s1^5 s3^3-3632 s1^7 s3^3-216 s1^9 s3^3-51432 s1 s2 s3^3+5160 s1^3 s2 s3^3-7640 s1^5 s2 s3^3-392 s1^7 s2 s3^3+24272 s1 s2^2 s3^3+108776 s1^3 s2^2 s3^3+15368 s1^5 s2^2 s3^3+448 s1^7 s2^2 s3^3+54024 s1 s2^3 s3^3-23152 s1^3 s2^3 s3^3-1464 s1^5 s2^3 s3^3-50856 s1 s2^4 s3^3-27800 s1^3 s2^4 s3^3-380 s1^5 s2^4 s3^3-7640 s1 s2^5 s3^3+6152 s1^3 s2^5 s3^3+18480 s1 s2^6 s3^3+792 s1^3 s2^6 s3^3-2376 s1 s2^7 s3^3-708 s1 s2^8 s3^3-19008 s3^4+194136 s1^2 s3^4+76676 s1^4 s3^4+8588 s1^6 s3^4+236 s1^8 s3^4+56988 s2 s3^4-258340 s1^2 s2 s3^4-50856 s1^4 s2 s3^4-4176 s1^6 s2 s3^4-40836 s2^2 s3^4+3454 s1^2 s2^2 s3^4-1708 s1^4 s2^2 s3^4+230 s1^6 s2^2 s3^4-39772 s2^3 s3^4+108776 s1^2 s2^3 s3^4+4160 s1^4 s2^3 s3^4+76676 s2^4 s3^4-28412 s1^2 s2^4 s3^4-1312 s1^4 s2^4 s3^4-36988 s2^5 s3^4-5716 s1^2 s2^5 s3^4+484 s2^6 s3^4+1846 s1^2 s2^6 s3^4+2364 s2^7 s3^4+92 s2^8 s3^4-174132 s1 s3^5-39772 s1^3 s3^5+2712 s1^5 s3^5+664 s1^7 s3^5+383268 s1 s2 s3^5+54024 s1^3 s2 s3^5+244 s1^5 s2 s3^5-258340 s1 s2^2 s3^5-14760 s1^3 s2^2 s3^5-168 s1^5 s2^2 s3^5+5160 s1 s2^3 s3^5+3656 s1^3 s2^3 s3^5+46884 s1 s2^4 s3^5-332 s1^3 s2^4 s3^5-10028 s1 s2^5 s3^5-748 s1 s2^6 s3^5+57294 s3^6-40836 s1^2 s3^6-14546 s1^4 s3^6-436 s1^6 s3^6-174132 s2 s3^6+24272 s1^2 s2 s3^6+7600 s1^4 s2 s3^6+194136 s2^2 s3^6-8200 s1^2 s2^2 s3^6-764 s1^4 s2^2 s3^6-86824 s2^3 s3^6+848 s1^2 s2^3 s3^6+9454 s2^4 s3^6+1356 s1^2 s2^4 s3^6+1708 s2^5 s3^6+28 s2^6 s3^6+56988 s1 s3^7+1904 s1^3 s3^7-832 s1^5 s3^7-51432 s1 s2 s3^7-104 s1^3 s2 s3^7+12632 s1 s2^2 s3^7-128 s1^3 s2^2 s3^7-2504 s1 s2^3 s3^7-196 s1 s2^4 s3^7-19008 s3^8+9000 s1^2 s3^8+398 s1^4 s3^8+16236 s2 s3^8-6296 s1^2 s2 s3^8+918 s2^2 s3^8+645 s1^2 s2^2 s3^8-1664 s2^3 s3^8+22 s2^4 s3^8-2628 s1 s3^9+436 s1^3 s3^9+1014 s1 s2 s3^9-140 s1 s2^2 s3^9-999 s3^10-138 s1^2 s3^10+1080 s2 s3^10+24 s2^2 s3^10-72 s1 s3^11,s2<s1^2/3,1/27 (-2 s1^3+9 s1 s2)-2/27 Sqrt[s1^6-9 s1^4 s2+27 s1^2 s2^2-27 s2^3]<s3,s3<1/27 (-2 s1^3+9 s1 s2)+2/27 Sqrt[s1^6-9 s1^4 s2+27 s1^2 s2^2-27 s2^3],256-96 s1^4+32 s1^6-3 s1^8+1024 s2+576 s1^2 s2-480 s1^4 s2+68 s1^6 s2+672 s2^2+1680 s1^2 s2^2-594 s1^4 s2^2+6 s1^6 s2^2-416 s2^3+1524 s1^2 s2^3-120 s1^4 s2^3-371 s2^4+318 s1^2 s2^4-9 s1^4 s2^4+60 s2^5+24 s1^2 s2^5+62 s2^6+6 s1^2 s2^6-4 s2^7-3 s2^8+1024 s1 s3+1152 s1^3 s3+96 s1^5 s3-4 s1^7 s3-1248 s1 s2 s3+864 s1^3 s2 s3+240 s1^5 s2 s3-1536 s1 s2^2 s3-1284 s1^3 s2^2 s3+24 s1^5 s2^2 s3+2104 s1 s2^3 s3-456 s1^3 s2^3 s3+564 s1 s2^4 s3-120 s1^3 s2^4 s3+240 s1 s2^5 s3+68 s1 s2^6 s3+4912 s3^2+4560 s1^2 s3^2+762 s1^4 s3^2+62 s1^6 s3^2-816 s2 s3^2+5844 s1^2 s2 s3^2+564 s1^4 s2 s3^2-6918 s2^2 s3^2+1008 s1^2 s2^2 s3^2+318 s1^4 s2^2 s3^2+1708 s2^3 s3^2-1284 s1^2 s2^3 s3^2+762 s2^4 s3^2-594 s1^2 s2^4 s3^2+96 s2^5 s3^2+32 s2^6 s3^2-816 s1 s3^3+1708 s1^3 s3^3+60 s1^5 s3^3-552 s1 s2 s3^3+2104 s1^3 s2 s3^3+5844 s1 s2^2 s3^3+1524 s1^3 s2^2 s3^3+864 s1 s2^3 s3^3-480 s1 s2^4 s3^3-10371 s3^4-6918 s1^2 s3^4-371 s1^4 s3^4-816 s2 s3^4-1536 s1^2 s2 s3^4+4560 s2^2 s3^4+1680 s1^2 s2^2 s3^4+1152 s2^3 s3^4-96 s2^4 s3^4-816 s1 s3^5-416 s1^3 s3^5-1248 s1 s2 s3^5+576 s1 s2^2 s3^5+4912 s3^6+672 s1^2 s3^6+1024 s2 s3^6+1024 s1 s3^7+256 s3^8>0},{s1,s2,s3}]

复制代码

所以数值上，最小值为0。
如何证明呢