Omar Jasim
2016-07-19 14:15:18 UTC
Dear all,
Please I need to prove that for any nonnegative quadratic polynomial
equation the discriminant will be nonpositive. I found a proposition in a
text book bellow :
https://books.google.co.uk/books?id=TPE0fXGnYtMC&pg=PA81&lpg=PA81&dq=if+f(x)+%3E0+then+b%5E2-4ac%3C0&source=bl&ots=eUAdjNvJpT&sig=KwJxcX_5RqIsCL4wJ3nrfvfZe9g&hl=en&sa=X&ved=0ahUKEwjlxpjm2ZjNAhWMLsAKHX2vAs8Q6AEILzAE#v=onepage&q&f=false
but for this one, the equality hold iff x=-b/2*a and I don't want to put
this as an assumption as I need this lemma in another work. the lemma I'm
trying is:
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows " discrim a b c ≤0"
I proved that for strictly positive equation as bellow:
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. (a*(x)^2 + b*x + c) >0 "
shows " discrim a b c ≤0"
using assms by (metis discriminant_pos_ex less_le not_less)
but for nonnegative equation (the first lemma) I couldn't and way. please
could any one help me in this because I spend alot of time trying to prove
it but unfortunately I failed.
Omar
Please I need to prove that for any nonnegative quadratic polynomial
equation the discriminant will be nonpositive. I found a proposition in a
text book bellow :
https://books.google.co.uk/books?id=TPE0fXGnYtMC&pg=PA81&lpg=PA81&dq=if+f(x)+%3E0+then+b%5E2-4ac%3C0&source=bl&ots=eUAdjNvJpT&sig=KwJxcX_5RqIsCL4wJ3nrfvfZe9g&hl=en&sa=X&ved=0ahUKEwjlxpjm2ZjNAhWMLsAKHX2vAs8Q6AEILzAE#v=onepage&q&f=false
but for this one, the equality hold iff x=-b/2*a and I don't want to put
this as an assumption as I need this lemma in another work. the lemma I'm
trying is:
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows " discrim a b c ≤0"
I proved that for strictly positive equation as bellow:
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. (a*(x)^2 + b*x + c) >0 "
shows " discrim a b c ≤0"
using assms by (metis discriminant_pos_ex less_le not_less)
but for nonnegative equation (the first lemma) I couldn't and way. please
could any one help me in this because I spend alot of time trying to prove
it but unfortunately I failed.
Omar