*To*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Subject*: Re: [isabelle] nonnegative quadratic polynomial*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Tue, 19 Jul 2016 17:14:16 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAAi=gevZ3jPsJSteprcnmdasPL57jYyky1pw+0gp1v3Zj42y5Q@mail.gmail.com>*References*: <CAAi=gevZ3jPsJSteprcnmdasPL57jYyky1pw+0gp1v3Zj42y5Q@mail.gmail.com>*User-agent*: Roundcube Webmail/1.0.2

Dear Omar, Here you are, 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" proof - have "âx. a*x^2 + b*x + c<0 " when "discrim a b c > 0" "a>0" proof - let ?P="Îx. a*x^2 + b*x +c" have "?P (- b / (2*a)) = (4*a*c-b^2)/(4*a)" using âa>0â apply (auto simp add:field_simps) by algebra also have "... <0" using that unfolding discrim_def by (simp add: divide_neg_pos) finally show ?thesis by blast qed then show ?thesis using assms using not_less by blast qed Best, Wenda On 2016-07-19 15:10, Omar Jasim wrote:

Dear all, Please I need to prove that for any nonnegative quadratic polynomialequation the discriminant will be nonpositive. I found a proposition inatext 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=falsebut for this one, the equality hold iff x=-b/2*a and I don't want toputthis as an assumption as I need this lemma in another work. the lemmaI'mtrying 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.pleasecould any one help me in this because I spend alot of time trying toproveit but unfortunately I failed. Omar

-- Wenda Li PhD Candidate Computer Laboratory University of Cambridge

**Follow-Ups**:**Re: [isabelle] nonnegative quadratic polynomial***From:*Omar Jasim

**References**:**[isabelle] nonnegative quadratic polynomial***From:*Omar Jasim

- Previous by Date: [isabelle] nonnegative quadratic polynomial
- Next by Date: Re: [isabelle] nonnegative quadratic polynomial
- Previous by Thread: [isabelle] nonnegative quadratic polynomial
- Next by Thread: Re: [isabelle] nonnegative quadratic polynomial
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list