(26) |

(28) |

*
*

*
*

*
*

*
*

(30) |

By hypothesis

(31) |

Hence both and are mutiple of . It follows that

(32) |

*
*

*
*

N := NonNegativeInteger (1) NonNegativeInteger Type: Domain Z := Integer (2) Integer Type: Domain U := UnivariatePolynomial(x,Z) (3) UnivariatePolynomial(x,Integer) Type: Domain m: Z := 5 (4) 5 Type: Integer f: U := x^4 - 1 4 (5) x - 1 Type: UnivariatePolynomial(x,Integer) g: U := x - 2 (6) x - 2 Type: UnivariatePolynomial(x,Integer) h: U := x^3 + 2 *x^2 -x -2 3 2 (7) x + 2x - x - 2 Type: UnivariatePolynomial(x,Integer) e := f - g*h 2 (8) 5x - 5 Type: UnivariatePolynomial(x,Integer) K5 := PrimeField(5) (9) PrimeField Type: Domain U5 := UnivariatePolynomial(x,K5) (10) UnivariatePolynomial(x,PrimeField 5) Type: Domain f5: U5 := f :: U5 4 (11) x + 4 Type: UnivariatePolynomial(x,PrimeField 5) g5: U5 := g :: U5 (12) x + 3 Type: UnivariatePolynomial(x,PrimeField 5) h5: U5 := h ::U5 3 2 (13) x + 2x + 4x + 3 Type: UnivariatePolynomial(x,PrimeField 5) res := extendedEuclidean(g5,h5) 2 (14) [coef1= 2x + 3x + 4,coef2= 3,generator= 1] s5: U5 := res.coef1 2 (15) 2x + 3x + 4 Type: UnivariatePolynomial(x,PrimeField 5) t5: U5 := res.coef2 (16) 3 Type: UnivariatePolynomial(x,PrimeField 5) g_^ := g + t5 :: U * e 2 (17) 15x + x - 17 Type: UnivariatePolynomial(x,Integer) h_^ := h + s5 :: U * e 4 3 2 (18) 10x + 16x + 12x - 16x - 22 Type: UnivariatePolynomial(x,Integer) factor(f - g_^ * h_^ ) 4 3 2 (19) - 25(x - 1)(x + 1)(6x + 10x + 7x - 10x - 15) Type: Factored UnivariatePolynomial(x,Integer)

(33) |

*
*

*
*

(34) |

*
*

*
*

(35) |

Hence we have

(36) |

Since the quotient and the remainder of w.r.t. are unique we have

(37) |

- ,
- ,
- is monic,
- ,
- ,
- .

- ,
- ,
- ,
- monic and of the same degree as ,
- of the same degree as .

(38) |

By assumption we have

(39) |

by Proposition 2 imply

(40) |

This leads to

(41) |

Now the relation defining

(42) |

together with and imply

(43) |

Similarly we have

(44) |

Now observe that by definition of we have

(45) |

Then since

(46) |

we obtain

(47) |

These last relations together with

(48) |

imply

(49) |

This concludes this proof. We refer to Theorem 15.11 in [GG99] for the other claims of the theorem.

(50) |

N := NonNegativeInteger (1) NonNegativeInteger Type: Domain Z := Integer (2) Integer Type: Domain U := UnivariatePolynomial(x,Z) (3) UnivariatePolynomial(x,Integer) Type: Domain m: Z := 5 (4) 5 Type: Integer f: U := x^4 - 1 4 (5) x - 1 Type: UnivariatePolynomial(x,Integer) g: U := x - 2 (6) x - 2 Type: UnivariatePolynomial(x,Integer) h: U := x^3 + 2 *x^2 -x -2 3 2 (7) x + 2x - x - 2 Type: UnivariatePolynomial(x,Integer) e := f - g*h 2 (8) 5x - 5 Type: UnivariatePolynomial(x,Integer) K5 := PrimeField(5) (9) PrimeField 5 Type: Domain U5 := UnivariatePolynomial(x,K5) (10) UnivariatePolynomial(x,PrimeField 5) Type: Domain f5: U5 := f :: U5 4 (11) x + 4 Type: UnivariatePolynomial(x,PrimeField 5) g5: U5 := g :: U5 (12) x + 3 Type: UnivariatePolynomial(x,PrimeField 5) h5: U5 := h ::U5 3 2 (13) x + 2x + 4x + 3 Type: UnivariatePolynomial(x,PrimeField 5) res := extendedEuclidean(g5,h5) 2 (14) [coef1= 2x + 3x + 4,coef2= 3,generator= 1] Type: Record(coef1: UnivariatePolynomial(x,PrimeField 5), coef2: UnivariatePolynomial(x,PrimeField 5), generator: UnivariatePolynomial(x,PrimeField 5)) s5: U5 := res.coef1 2 (15) 2x + 3x + 4 Type: UnivariatePolynomial(x,PrimeField 5) s: U := s5 :: U 2 (16) 2x + 3x + 4 Type: UnivariatePolynomial(x,Integer) t5: U5 := res.coef2 (17) 3 Type: UnivariatePolynomial(x,PrimeField 5) t: U := t5 :: U (18) 3 Type: UnivariatePolynomial(x,Integer) R25 := IntegerMod(25) (19) IntegerMod 25 Type: Domain U25 := UnivariatePolynomial(x,R25) (20) UnivariatePolynomial(x,IntegerMod 25) Type: Domain e25 := f::U25 - g::U25 * h::U25 2 (21) 5x + 20 Type: UnivariatePolynomial(x,IntegerMod 25) e : U := e25 :: U 2 (22) 5x + 20 Type: UnivariatePolynomial(x,Integer) res := monicDivide(s*e, h) 2 (23) [quotient= 10x - 5,remainder= 80x + 75x + 70] Type: Record(quotient: UnivariatePolynomial(x,Integer), remainder: UnivariatePolynomial(x,Integer)) q25: U25 := res.quotient :: U25 (24) 10x + 20 Type: UnivariatePolynomial(x,IntegerMod 25) r25: U25 := res.remainder :: U25 2 (25) 5x + 20 Type: UnivariatePolynomial(x,IntegerMod 25) g_* := (g::U25 + t::U25 * e25 + q25 * (g::U25)) :: U (26) x + 18 Type: UnivariatePolynomial(x,Integer) h_* := (h::U25 + r25) :: U 3 2 (27) x + 7x + 24x + 18 Type: UnivariatePolynomial(x,Integer) (f - g_* * h_*) :: U25 (28) 0 Type: UnivariatePolynomial(x,IntegerMod 25)

- the leading coefficients of and are not zero divisors modulo
- the polynomials and have the same leading coefficients, the same degree and coincide modulo
- the polynomials and have the same leading coefficients, the same degree and coincide modulo

(51) |

(52) |

Let be maximal such that both divides and . Thus there exist polynomials such that

(53) |

and also does not divide or . We may assume that does not divide . Now we have

(54) |

This means that divides . In other words there exist such that

(55) |

Since is not a zero divisor in we have

(56) |

which implies

(57) |

Recall also that we have

(58) |

and

(59) |

Therefore we obtain the following calculation modulo

(60) |

This shows that divides modulo . However from together with the facts that and have same leading coefficient and degree shows that

(61) |

Since the leading coefficient of is not a zero divisor modulo we must have

(62) |

A contradiction. Therefore the theorem is proved.

*
*

*
*

2008-01-07