Re: [isabelle] nonnegative quadratic polynomial



Dear Wenda,

now I see where I was stuck. Thank you very much for that, it's really
helpful.

Cheers.

Omar

On 19 July 2016 at 17:14, Wenda Li <wl302 at cam.ac.uk> wrote:

> 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 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
>>
>
> --
> Wenda Li
> PhD Candidate
> Computer Laboratory
> University of Cambridge
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.