# Inequality cannot be solved using Reduce (no transcendental functions) [closed]

I have these assumptions:

aF = vF0 > 0 && vR0 > 0 &&
bFx > 0 && rho > 0 && aRx > 0 && bRx > 0 &&
bFx > bRx && 0 < vF0/bFx && vF0/bFx < rho &&
rho < (aRx*rho + bRx*rho + vR0)/bRx


I cannot solve the following inequality with Reduce (output form visible in the last line):

SetSystemOptions["SimplificationOptions" -> "AssumptionsMaxNonlinearVariables" -> 100];
Assuming[
aF,
Reduce[$Assumptions && (aRx^2 bFx rho^2 + aRx bFx bRx rho^2 - bRx vF0^2 + 2 aRx bFx rho vR0 + 2 bFx bRx rho vR0 + bFx vR0^2)/(2 bFx bRx) <= (aRx vF0^2 - bFx vF0^2 + 2 bFx vF0 vR0)/(2 bFx^2)] ]  Reduce::nsmet: This system cannot be solved with the methods available to Reduce. Can inequalities like this be solved in another way? • Please go here to see how to copy readable code from Mathematica: How to copy code from Mathematica so it looks good on this site. Jul 19, 2022 at 15:59 • Thanks for the link, but I use the free Wolfram Engine in a text terminal. I updated the question to explain why only a text form. Jul 19, 2022 at 16:01 • MMA version 13.1 I get "False" as result from Reduce. Jul 19, 2022 at 16:10 • @scriptfoo Does the Wolfram Engine in text mode only return the unreadable FullForm you show? I find that hard to believe. Can't you get the InputForm? Anyway, I tried to convert your equations to InputForm to make them more readable, but I also get False as the output. Note that you did not show us the contents of your $Assumptions, so we may not be able to properly reproduce your behavior. Jul 19, 2022 at 16:14
• @Daniel Yes, the inequality should always be false. I use Wolfram Engine 13.0.1. I'll try to install the newest version in a moment. Jul 19, 2022 at 16:17

Reducing assumptions and inequation yields False

aF = (vF0 > 0 && vR0 > 0 && bFx > 0 && rho > 0 && aRx > 0 && bRx > 0 &&
bFx > bRx) && Less[0, Times[Power[bFx, -1], vF0]] &&
Less[Times[Power[bFx, -1], vF0], rho] &&
Less[rho,
Times[Power[bRx, -1],
Plus[Times[aRx, rho], Times[bRx, rho], vR0]]] // Reduce

ineq = Times[Divide[1, 2], Power[bFx, -1], Power[bRx, -1],
Plus[Times[Power[aRx, 2], bFx, Power[rho, 2]],
Times[aRx, bFx, bRx, Power[rho, 2]],
Times[-1, bRx, Power[vF0, 2]], Times[2, aRx, bFx, rho, vR0],
Times[2, bFx, bRx, rho, vR0], Times[bFx, Power[vR0, 2]]]] <=
Times[Divide[1, 2], Power[bFx, -2],
Plus[Times[aRx, Power[vF0, 2]], Times[-1, bFx, Power[vF0, 2]],
Times[2, bFx, vF0, vR0]]] // Simplify

red = Reduce[ineq && aF]

(*   False   *)