set IR = INT.Ring ;
set i1 = In (1,INT.Ring);
set i2 = In (2,INT.Ring);
set i3 = In (3,INT.Ring);
set i5 = In (5,INT.Ring);
given p being Polynomial of INT.Ring such that A1:
( eval (p,(In (1,INT.Ring))) = 2 & eval (p,(In (3,INT.Ring))) = 5 )
; contradiction
set IR = INT.Ring ;
set t = (In (2,INT.Ring)) * (1_. INT.Ring);
set g = p - ((In (2,INT.Ring)) * (1_. INT.Ring));
reconsider G = p - ((In (2,INT.Ring)) * (1_. INT.Ring)) as Polynomial of F_Rat by RING_3:47, LIOUVIL2:7;
reconsider I1 = In (1,INT.Ring), I2 = In (2,INT.Ring), I3 = In (3,INT.Ring) as Element of F_Rat by RING_3:47, LIOUVIL2:6;
A2: eval (((In (2,INT.Ring)) * (1_. INT.Ring)),(In (1,INT.Ring))) =
(In (2,INT.Ring)) * (eval ((1_. INT.Ring),(In (1,INT.Ring))))
by RING_5:7
.=
(In (2,INT.Ring)) * (1. INT.Ring)
by POLYNOM4:18
.=
In (2,INT.Ring)
;
A3: eval (((In (2,INT.Ring)) * (1_. INT.Ring)),(In (3,INT.Ring))) =
(In (2,INT.Ring)) * (eval ((1_. INT.Ring),(In (3,INT.Ring))))
by RING_5:7
.=
(In (2,INT.Ring)) * (1. INT.Ring)
by POLYNOM4:18
.=
In (2,INT.Ring)
;
eval (G,I1) =
eval ((p - ((In (2,INT.Ring)) * (1_. INT.Ring))),(In (1,INT.Ring)))
by RING_3:47, Th40
.=
(In (2,INT.Ring)) - (In (2,INT.Ring))
by A2, A1, POLYNOM4:21
.=
0. INT.Ring
.=
0. F_Rat
by RING_3:47, C0SP1:def 3
;
then A4:
G = (G div (rpoly (1,I1))) *' (rpoly (1,I1))
by Th41, POLYNOM5:def 7;
(In (1,INT.Ring)) * (In (1,INT.Ring)) = 1. INT.Ring
;
then reconsider h = G div (rpoly (1,I1)) as Polynomial of INT.Ring by RING_3:47, A4, Th42, ALGSTR_0:def 27;
reconsider hi3 = eval (h,(In (3,INT.Ring))) as Integer ;
eval ((rpoly (1,I1)),I3) =
I3 - I1
by HURWITZ:29
.=
In (2,INT.Ring)
;
then eval (G,I3) =
(eval ((G div (rpoly (1,I1))),I3)) * I2
by A4, POLYNOM4:24
.=
(eval (h,(In (3,INT.Ring)))) * (In (2,INT.Ring))
by RING_3:47, Th40
;
then A5:
eval ((p - ((In (2,INT.Ring)) * (1_. INT.Ring))),(In (3,INT.Ring))) = (eval (h,(In (3,INT.Ring)))) * (In (2,INT.Ring))
by RING_3:47, Th40;
eval ((p - ((In (2,INT.Ring)) * (1_. INT.Ring))),(In (3,INT.Ring))) =
(eval (p,(In (3,INT.Ring)))) - (eval (((In (2,INT.Ring)) * (1_. INT.Ring)),(In (3,INT.Ring))))
by POLYNOM4:21
.=
In (3,INT.Ring)
by A1, A3
;
then
( 2 divides 3 & 2 divides 3 + (- 1) )
by A5;
then
2 divides - 1
by INT_2:1;
hence
contradiction
by INT_2:13; verum