let F be Field; :: thesis: ( F is algebraic-closed iff for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p,q have_no_common_roots ) )

A: now :: thesis: ( F is algebraic-closed implies for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p,q have_no_common_roots ) )

assume Z: F is algebraic-closed ; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p,q have_no_common_roots )

now :: thesis: for p, q being Element of the carrier of (Polynom-Ring F) st not p,q are_coprime holds
p,q have_a_common_root

let p, q be Element of the carrier of (Polynom-Ring F); :: thesis: ( not p,q are_coprime implies b₁,b₂ have_a_common_root )
set g = p gcd q;
assume AS: not p,q are_coprime ; :: thesis: b₁,b₂ have_a_common_root

per cases ( ( p = 0_. F & q = 0_. F ) or p <> 0_. F or q <> 0_. F ) ;

suppose X: ( p = 0_. F & q = 0_. F ) ; :: thesis: b₁,b₂ have_a_common_root

eval ((0_. F),(0. F)) = 0. F by POLYNOM4:17;
then ( 0. F is_a_root_of p & 0. F is_a_root_of q ) by X, POLYNOM5:def 7;
hence p,q have_a_common_root by RATFUNC1:def 4, RATFUNC1:def 3; :: thesis: verum

end;

suppose K: ( p <> 0_. F or q <> 0_. F ) ; :: thesis: b₁,b₂ have_a_common_root

now :: thesis: not p gcd q is constant

assume K0: p gcd q is constant ; :: thesis: contradiction

per cases ( p gcd q = 0_. F or p gcd q <> 0_. F ) ;

suppose K1: p gcd q = 0_. F ; :: thesis: contradiction

consider r1 being Polynomial of F such that
K2: (0_. F) *' r1 = p by K1, RING_4:52, RING_4:1;
consider r2 being Polynomial of F such that
K3: (0_. F) *' r2 = q by K1, RING_4:52, RING_4:1;
thus contradiction by K, K2, K3; :: thesis: verum

end;

suppose K1: p gcd q <> 0_. F ; :: thesis: contradiction

reconsider p1 = p, q1 = q as Polynomial of F ;
reconsider g1 = p gcd q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg (p gcd q) <= 0 by K0, RATFUNC1:def 2;
then reconsider g1 = g1 as non zero constant Element of the carrier of (Polynom-Ring F) by K1, UPROOTS:def 5, RING_4:def 4;
consider a being Element of F such that
K3: g1 = a | F by RING_4:20;

per cases ( p <> 0_. F or q <> 0_. F ) by K;

suppose p <> 0_. F ; :: thesis: contradiction

then not p1 is zero by UPROOTS:def 5;
then 1. F = LC (a | F) by K3, RATFUNC1:def 7
.= a by RING_5:6 ;
then p gcd q = 1_. F by K3, RING_4:14;
hence contradiction by AS, copr1; :: thesis: verum

end;

suppose q <> 0_. F ; :: thesis: contradiction

then not q1 is zero by UPROOTS:def 5;
then 1. F = LC (a | F) by K3, RATFUNC1:def 7
.= a by RING_5:6 ;
then p gcd q = 1_. F by K3, RING_4:14;
hence contradiction by AS, copr1; :: thesis: verum

end;

end;

end;

end;

end;

then consider a being Element of F such that
F: a is_a_root_of p gcd q by Z, POLYNOM5:def 8;
X: eval ((p gcd q),a) = 0. F by F, POLYNOM5:def 7;
consider gp being Polynomial of F such that
G: (p gcd q) *' gp = p by RING_4:52, RING_4:1;
consider gq being Polynomial of F such that
J: (p gcd q) *' gq = q by RING_4:52, RING_4:1;
( eval (p,a) = (0. F) * (eval (gp,a)) & eval (q,a) = (0. F) * (eval (gq,a)) ) by J, G, X, POLYNOM4:24;
then ( a is_a_root_of p & a is_a_root_of q ) by POLYNOM5:def 7;
hence p,q have_a_common_root by RATFUNC1:def 4, RATFUNC1:def 3; :: thesis: verum

end;

end;

end;

hence for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p,q have_no_common_roots ) by copr2; :: thesis: verum

end;

now :: thesis: ( not F is algebraic-closed implies ex p, q being Element of the carrier of (Polynom-Ring F) st
( not p,q are_coprime & p,q have_no_common_roots ) )

assume not F is algebraic-closed ; :: thesis: ex p, q being Element of the carrier of (Polynom-Ring F) st
( not p,q are_coprime & p,q have_no_common_roots )
then reconsider F1 = F as non algebraic-closed Field ;
set p = the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1);
reconsider p1 = the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) as Element of (Polynom-Ring F1) ;
reconsider e = 1. (Polynom-Ring F1) as Element of (Polynom-Ring F1) ;
H: e = 1_. F1 by POLYNOM3:def 10;
B: not the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1), the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) are_coprime

proof

D: p1 divides p1 ;

now :: thesis: 1. (Polynom-Ring F1) is not a_gcd of p1,p1

assume 1. (Polynom-Ring F1) is a_gcd of p1,p1 ; :: thesis: contradiction
then p1 divides e by D, RING_4:def 10;
then the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) divides 1_. F1 by H;
then deg the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) <= deg (1_. F) by RING_5:13;
then deg the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) <= 0 by RATFUNC1:def 2;
hence contradiction by RING_4:def 4; :: thesis: verum

end;

hence not the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1), the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) are_coprime ; :: thesis: verum

end;

now :: thesis: not the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1), the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) have_a_common_root

assume the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1), the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) have_a_common_root ; :: thesis: contradiction
then consider a being Element of F1 such that
A: a is_a_common_root_of the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1), the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) by RATFUNC1:def 4;
( a is_a_root_of the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) & a is_a_root_of the monic non with_roots non constant Element of the carrier of (Polynom-Ring F1) ) by A, RATFUNC1:def 3;
hence contradiction by POLYNOM5:def 8; :: thesis: verum

end;

hence ex p, q being Element of the carrier of (Polynom-Ring F) st
( not p,q are_coprime & p,q have_no_common_roots ) by B; :: thesis: verum

end;

hence ( F is algebraic-closed iff for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p,q have_no_common_roots ) ) by A; :: thesis: verum