let F be Field; :: thesis: for p being Ppoly of F
for q being Polynomial of F holds
( (Roots p) /\ (Roots q) = {} iff p gcd q = 1_. F )
let p be Ppoly of F; :: thesis: for q being Polynomial of F holds
( (Roots p) /\ (Roots q) = {} iff p gcd q = 1_. F )
let q be Polynomial of F; :: thesis: ( (Roots p) /\ (Roots q) = {} iff p gcd q = 1_. F )

Z: now :: thesis: ( (Roots p) /\ (Roots q) = {} implies p gcd q = 1_. F )

assume AS: (Roots p) /\ (Roots q) = {} ; :: thesis: p gcd q = 1_. F
( (1_. F) *' p = p & (1_. F) *' q = q ) ;
then A: ( 1_. F divides p & 1_. F divides q ) by RING_4:1;

now :: thesis: for r being Polynomial of F st r divides q & r divides p holds
r divides 1_. F

let r be Polynomial of F; :: thesis: ( r divides q & r divides p implies r divides 1_. F )
assume C: ( r divides q & r divides p ) ; :: thesis: r divides 1_. F
then consider u being Polynomial of F such that
D: p = r *' u by RING_4:1;
( Roots r c= Roots q & Roots r c= Roots p ) by C, ZZ3b;
then E: Roots r c= (Roots q) /\ (Roots p) ;

now :: thesis: r is constant

assume F: not r is constant ; :: thesis: contradiction
then F2: r is non zero Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
set r1 = NormPolynomial r;
set u1 = (LC r) * u;
F3: LC r <> 0. F by F;
F1: (NormPolynomial r) *' ((LC r) * u) = (((LC r) ") * r) *' ((LC r) * u) by F2, RING_4:23
.= (LC r) * ((((LC r) ") * r) *' u) by RING_4:10
.= (LC r) * (((LC r) ") * (u *' r)) by RING_4:10
.= ((LC r) * ((LC r) ")) * (u *' r) by RING_4:11
.= (1. F) * (r *' u) by F3, VECTSP_1:def 10
.= p by D ;
F4: deg r > 0 by F, RATFUNC1:def 2;
F5: deg r = (len r) - 1 by HURWITZ:def 2;
then I: len r <> 0 by F;
then len (NormPolynomial r) = len r by POLYNOM5:57;
then deg (NormPolynomial r) = deg r by F5, HURWITZ:def 2;
then K: ( not NormPolynomial r is constant & NormPolynomial r is monic ) by F, F4, RATFUNC1:def 2;
not (LC r) * u is zero by F1;
then G: NormPolynomial r is Ppoly of F by F1, K, FIELD_8:10;
Roots (NormPolynomial r) = Roots r by I, POLYNOM5:61;
hence contradiction by AS, E, G; :: thesis: verum

end;

then deg r <= 0 by RATFUNC1:def 2;
then r is constant Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10, RING_4:def 4;
then consider a being Element of F such that
F6: r = a | F by RING_4:20;

F7: now :: thesis: not a = 0. F

assume a = 0. F ; :: thesis: contradiction
then r = 0_. F by F6, RING_4:13;
hence contradiction by E, AS; :: thesis: verum

end;

(a | F) *' ((a ") | F) = (a * (a ")) | F by RING_4:18
.= (1. F) | F by F7, VECTSP_1:def 10
.= 1_. F by RING_4:14 ;
hence r divides 1_. F by F6, RING_4:1; :: thesis: verum

end;

hence p gcd q = 1_. F by A, RING_4:53; :: thesis: verum

end;

now :: thesis: ( (Roots p) /\ (Roots q) <> {} implies p gcd q <> 1_. F )

assume AS: (Roots p) /\ (Roots q) <> {} ; :: thesis: p gcd q <> 1_. F
set a = the Element of (Roots p) /\ (Roots q);
A1: ( the Element of (Roots p) /\ (Roots q) in Roots p & the Element of (Roots p) /\ (Roots q) in Roots q ) by AS, XBOOLE_0:def 4;
then reconsider a = the Element of (Roots p) /\ (Roots q) as Element of F ;
a is_a_root_of p by A1, POLYNOM5:def 10;
then A2: eval (p,a) = 0. F by POLYNOM5:def 7;
a is_a_root_of q by A1, POLYNOM5:def 10;
then eval (q,a) = 0. F by POLYNOM5:def 7;
then A3: ( rpoly (1,a) divides p & rpoly (1,a) divides q ) by A2, RING_5:11;
( deg (rpoly (1,a)) = 1 & deg (1_. F) <= 0 ) by HURWITZ:27, RATFUNC1:def 2;
hence p gcd q <> 1_. F by A3, RING_5:13, RING_4:52; :: thesis: verum

end;

hence ( (Roots p) /\ (Roots q) = {} iff p gcd q = 1_. F ) by Z; :: thesis: verum