Recenty in sci.math.symbolic there was a question if
This can be proved by an elementary argument. Below w show purely mechanical way based on cylindrical algebraic decomposition (CAD). fricas (1) -> rC := RealClosure(Fraction(Integer))
Type: Typefricas pR := POLY(rC)
Type: Typefricas -- Replace inequalies by differences of sides lp := [b^2 - (a - c)^2,
Type: List(Polynomial(Integer))fricas -- Do CAD cd := cylindricalDecomposition(lp::List(pR) )$CylindricalAlgebraicDecompositionPackage(rC)
Type: List(Cell(RealClosure(Fraction(Integer))))fricas -- If implication is false, Type: List(Cell(RealClosure(Fraction(Integer))))fricas sp3 := [samplePoint(ce) for ce in cd3]::List(List(Fraction(Integer)))
Type: List(List(Fraction(Integer)))fricas vll := [map(p +-> eval(p, Type: List(List(Polynomial(Fraction(Integer))))fricas vlq := vll::List(List(Fraction(Integer)))
Type: List(List(Fraction(Integer)))fricas good := true
Type: Booleanfricas -- Loop to check validity of formula at each sample point for vl in vlq repeat if vl(1) > 0 and vl(2) > 0 and vl(3) < 0 and vl(4) < 0 then good := false Type: Voidfricas print good Type: VoidLet us explain this a bit more. CAD for list of polynomials |