let F be Field; :: thesis: for a being non zero Element of F
for b, c being Element of F st Roots <%c,b,a%> <> {} holds
(b ^2) - ((4 '*' a) * c) is square
let a be non zero Element of F; :: thesis: for b, c being Element of F st Roots <%c,b,a%> <> {} holds
(b ^2) - ((4 '*' a) * c) is square
let b, c be Element of F; :: thesis: ( Roots <%c,b,a%> <> {} implies (b ^2) - ((4 '*' a) * c) is square )
set p = <%c,b,a%>;
set r = the Element of Roots <%c,b,a%>;
assume AS: Roots <%c,b,a%> <> {} ; :: thesis: (b ^2) - ((4 '*' a) * c) is square
then the Element of Roots <%c,b,a%> in Roots <%c,b,a%> ;
then reconsider r = the Element of Roots <%c,b,a%> as Element of F ;
r is_a_root_of <%c,b,a%> by AS, POLYNOM5:def 10;
then 0. F = (c + (b * r)) + (a * (r ^2)) by evalq
.= ((a * (r ^2)) + (b * r)) + c by RLVECT_1:def 3
.= ((a * (r ^2)) + (r * b)) + c by GROUP_1:def 12 ;
then 0. F = (4 '*' a) * (((a * (r ^2)) + (r * b)) + c)
.= ((4 '*' a) * ((a * (r ^2)) + (r * b))) + ((4 '*' a) * c) by VECTSP_1:def 2
.= (((4 '*' a) * (a * (r ^2))) + ((4 '*' a) * (r * b))) + ((4 '*' a) * c) by VECTSP_1:def 2
.= (((4 '*' a) * (a * (r ^2))) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by GROUP_1:def 3
.= ((((4 '*' a) * a) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by GROUP_1:def 3
.= (((4 '*' (a * a)) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by REALALG2:5
.= ((((2 * 2) '*' (a ^2)) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by O_RING_1:def 1
.= ((((2 ^2) '*' (a ^2)) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by SQUARE_1:def 1
.= ((((2 '*' a) ^2) * (r ^2)) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by ch1
.= ((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c) by ch0 ;
then - ((4 '*' a) * c) = (((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + ((4 '*' a) * c)) - ((4 '*' a) * c)
.= ((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + (((4 '*' a) * c) - ((4 '*' a) * c)) by RLVECT_1:def 3
.= ((((2 '*' a) * r) ^2) + (((4 '*' a) * r) * b)) + (0. F) by RLVECT_1:15 ;
then (b ^2) + (- ((4 '*' a) * c)) = ((((2 '*' a) * r) ^2) + (((2 * 2) '*' (a * r)) * b)) + (b ^2) by REALALG2:5
.= ((((2 '*' a) * r) ^2) + ((2 '*' (2 '*' (a * r))) * b)) + (b ^2) by RING_3:65
.= ((((2 '*' a) * r) ^2) + ((2 '*' ((2 '*' a) * r)) * b)) + (b ^2) by REALALG2:5
.= (((2 '*' a) * r) + b) ^2 by REALALG2:7 ;
hence (b ^2) - ((4 '*' a) * c) is square ; :: thesis: verum