let F be Field; :: thesis: for p, q being Polynomial of F holds
( p gcd q divides p & p gcd q divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q ) )
let p, q be Polynomial of F; :: thesis: ( p gcd q divides p & p gcd q divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q ) )
reconsider a = p, b = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
set g = a gcd b;
A0: p gcd q = a gcd b by dd;
a gcd b divides a by defGCD;
then consider c being Element of (Polynom-Ring F) such that
A1: (a gcd b) * c = a ;
reconsider r = c as Polynomial of F by POLYNOM3:def 10;
(p gcd q) *' r = p by A0, A1, POLYNOM3:def 10;
hence p gcd q divides p by T2; :: thesis: ( p gcd q divides q & ( for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q ) )
a gcd b divides b by defGCD;
then consider c being Element of (Polynom-Ring F) such that
A1: (a gcd b) * c = b ;
reconsider r = c as Polynomial of F by POLYNOM3:def 10;
(p gcd q) *' r = q by A0, A1, POLYNOM3:def 10;
hence p gcd q divides q by T2; :: thesis: for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q
now :: thesis: for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q
let r be Polynomial of F; :: thesis: ( r divides p & r divides q implies r divides p gcd q )
assume A1: ( r divides p & r divides q ) ; :: thesis: r divides p gcd q
reconsider c = r as Element of (Polynom-Ring F) by POLYNOM3:def 10;
consider s being Polynomial of F such that
A2: r *' s = p by A1, T2;
consider t being Polynomial of F such that
A3: r *' t = q by A1, T2;
reconsider x = s, y = t as Element of (Polynom-Ring F) by POLYNOM3:def 10;
( c * x = a & c * y = b ) by A2, A3, POLYNOM3:def 10;
then ( c divides a & c divides b ) ;
then c divides a gcd b by defGCD;
hence r divides p gcd q by dd; :: thesis: verum
end;
hence for r being Polynomial of F st r divides p & r divides q holds
r divides p gcd q ; :: thesis: verum