-
Notifications
You must be signed in to change notification settings - Fork 3
Proof
Naoki Shibata edited this page Aug 19, 2020
·
2 revisions
P: w * sqrt(x) + y > z
Below is a proof of the following proposition.
P <-> s*(w*w)*x > s*(z - y)*(z - y) if s*(z-y) >= 0
P <-> w >= 0 if s*(z-y) < 0
where s = w < 0 ? -1 : 1.
--
P <-> w * sqrt(x) > z - y
P <-> 0 > z - y if w == 0
P <-> sqrt(x) > (z - y) / w if w > 0
P <-> sqrt(x) < (z - y) / w if w < 0
Let s = w < 0 ? -1 : 1
P <-> 0 > z - y if w == 0
P <-> s*sqrt(x) > s*(z - y) / w if w != 0
P <-> 0 > z - y if w == 0
P <-> s*x > s*((z - y) / w)^2 if w != 0 && (z - y) / w >= 0
P <-> sqrt(x) > (z-y) / w if w != 0 && (z - y) / w < 0 && w >= 0
P <-> sqrt(x) < (z-y) / w if w != 0 && (z - y) / w < 0 && w < 0
P <-> 0 > z - y if w == 0
P <-> s*x > s*((z - y) / w)^2 if w != 0 && (z - y) / w >= 0
P <-> true if w != 0 && (z - y) / w < 0 && w >= 0
P <-> false if w != 0 && (z - y) / w < 0 && w < 0
P <-> 0 > z - y if w == 0
P <-> s*x > s*((z - y) / w)^2 if w != 0 && (z - y) / w >= 0
P <-> w >= 0 if w != 0 && (z - y) / w < 0
P <-> 0 > z - y if w == 0
P <-> s*(w*w)*x > s*(z - y)*(z - y) if w != 0 && (z - y) / w >= 0
P <-> w >= 0 if w != 0 && (z - y) / w < 0
Here, (z - y) / w >= 0 <-> s*(z-y) >= 0 holds if w != 0
P <-> 0 > z - y if w == 0
P <-> s*(w*w)*x > s*(z - y)*(z - y) if w != 0 && s*(z-y) >= 0
P <-> w >= 0 if w != 0 && (z - y) / w < 0
w == 0 -> s == 1 && s*(w*w)*x <= s*(z - y)*(z - y) && (s*(z - y) >= 0 <-> z >= y)
P <-> s*(w*w)*x > s*(z - y)*(z - y) if s*(z-y) >= 0
P <-> 0 > z - y if w == 0 && s*(z-y) < 0
P <-> w >= 0 if w != 0 && s*(z-y) < 0
s*(z - y) < 0 <-> (w < 0 && z > y) || (w > 0 && z < y)
P <-> s*(w*w)*x > s*(z - y)*(z - y) if s*(z-y) >= 0
P <-> w >= 0 if s*(z-y) < 0