set R = Z/ 6;
set z = 2 '*' (1. (Z/ 6));
set d = 3 '*' (1. (Z/ 6));
take p = rpoly (1,(2 '*' (1. (Z/ 6)))); :: thesis: not for q being Polynomial of (Z/ 6) holds Roots (p *' q) c= (Roots p) \/ (Roots q)
take q = rpoly (1,(3 '*' (1. (Z/ 6)))); :: thesis: not Roots (p *' q) c= (Roots p) \/ (Roots q)
C: Char (Z/ 6) = 6 by RING_3:77;
eval ((p *' q),(0. (Z/ 6))) = (eval (p,(0. (Z/ 6)))) * (eval (q,(0. (Z/ 6)))) by POLYNOM4:24
.= ((0. (Z/ 6)) - (2 '*' (1. (Z/ 6)))) * (eval (q,(0. (Z/ 6)))) by HURWITZ:29
.= ((0. (Z/ 6)) - (2 '*' (1. (Z/ 6)))) * ((0. (Z/ 6)) - (3 '*' (1. (Z/ 6)))) by HURWITZ:29
.= (- (2 '*' (1. (Z/ 6)))) * ((0. (Z/ 6)) - (3 '*' (1. (Z/ 6)))) by RLVECT_1:14
.= (- (2 '*' (1. (Z/ 6)))) * (- (3 '*' (1. (Z/ 6)))) by RLVECT_1:14
.= (2 '*' (1. (Z/ 6))) * (3 '*' (1. (Z/ 6))) by VECTSP_1:10
.= (2 * 3) '*' (1. (Z/ 6)) by RING_3:67
.= 0. (Z/ 6) by C, RING_3:def 5 ;
then 0. (Z/ 6) is_a_root_of p *' q by POLYNOM5:def 7;
then B: 0. (Z/ 6) in Roots (p *' q) by POLYNOM5:def 10;
now :: thesis: not 0. (Z/ 6) in (Roots p) \/ (Roots q)
assume AS: 0. (Z/ 6) in (Roots p) \/ (Roots q) ; :: thesis: contradiction
per cases ( 0. (Z/ 6) in Roots p or 0. (Z/ 6) in Roots q ) by AS, XBOOLE_0:def 3;
suppose 0. (Z/ 6) in Roots p ; :: thesis: contradiction
then 0. (Z/ 6) is_a_root_of p by POLYNOM5:def 10;
then B: 0. (Z/ 6) = eval (p,(0. (Z/ 6))) by POLYNOM5:def 7
.= (0. (Z/ 6)) - (2 '*' (1. (Z/ 6))) by HURWITZ:29
.= - (2 '*' (1. (Z/ 6))) by RLVECT_1:14 ;
2 '*' (1. (Z/ 6)) = - (- (2 '*' (1. (Z/ 6))))
.= 0. (Z/ 6) by B ;
hence contradiction by C, RING_3:def 5; :: thesis: verum
end;
suppose 0. (Z/ 6) in Roots q ; :: thesis: contradiction
then 0. (Z/ 6) is_a_root_of q by POLYNOM5:def 10;
then B: 0. (Z/ 6) = eval (q,(0. (Z/ 6))) by POLYNOM5:def 7
.= (0. (Z/ 6)) - (3 '*' (1. (Z/ 6))) by HURWITZ:29
.= - (3 '*' (1. (Z/ 6))) by RLVECT_1:14 ;
3 '*' (1. (Z/ 6)) = - (- (3 '*' (1. (Z/ 6))))
.= 0. (Z/ 6) by B ;
hence contradiction by C, RING_3:def 5; :: thesis: verum
end;
end;
end;
hence not Roots (p *' q) c= (Roots p) \/ (Roots q) by B; :: thesis: verum