set PRat = Polynom-Ring F_Rat;
assume number_e is algebraic ; :: thesis: ex g being INT -valued Polynomial of F_Rat st
( @ g is irreducible & Ext_eval (g,(In (number_e,F_Real))) = 0 & deg g >= 2 & g . 0 <> 0. F_Rat )
then consider x being Element of F_Complex such that
A2: ( x = number_e & x is_integral_over F_Rat ) by ALGNUM_1:def 4;
reconsider e1 = number_e as Element of F_Real by XREAL_0:def 1;
consider f0 being Element of (Polynom-Ring F_Rat) such that
A3: ( f0 <> 0_. F_Rat & {f0} -Ideal = Ann_Poly (x,F_Rat) & f0 = NormPolynomial f0 ) by ALGNUM_1:3, A2, ALGNUM_1:33;
f0 in Ann_Poly (x,F_Rat) by A3, IDEAL_1:66;
then f0 in { p where p is Polynomial of F_Rat : Ext_eval (p,x) = 0. F_Complex } by ALGNUM_1:def 8;
then consider f being Polynomial of F_Rat such that
A4: ( f0 = f & Ext_eval (f,x) = 0. F_Complex ) ;
f0 <> 0. (Polynom-Ring F_Rat) by A3, POLYNOM3:def 10;
then reconsider f0 = f0 as non zero Element of (Polynom-Ring F_Rat) by STRUCT_0:def 12;
{f0} -Ideal is maximal by A2, E_TRANS1:11, ALGNUM_1:3, A3;
then A7: f0 is irreducible by RING_2:25;
reconsider f0 = f0 as non zero Element of the carrier of (Polynom-Ring F_Rat) by A3, UPROOTS:def 5;
reconsider m = Product (denomi-seq f0) as non zero Nat by E_TRANS1:9;
A8: m * f0 = ((In (m,F_Rat)) | F_Rat) *' (~ f0) by Lm8a;
reconsider mf0 = m * f0 as Element of the carrier of (Polynom-Ring F_Rat) ;
A14: rng mf0 c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng mf0 or y in INT )
assume y in rng mf0 ; :: thesis: y in INT
then consider x1 being object such that
A10: ( x1 in dom mf0 & y = mf0 . x1 ) by FUNCT_1:def 3;
reconsider i = x1 as Element of NAT by A10;
reconsider f0i = f0 . i as Rational ;
A11: mf0 . i = (In (m,F_Rat)) * (f0 . i) by A8, RINGDER1:27;
consider z being Integer such that
A12: z * (denominator (f0 . i)) = m by E_TRANS1:10;
m * f0i = z * ((denominator f0i) * f0i) by A12
.= z * (numerator f0i) by RAT_1:def 4 ;
hence y in INT by A11, A10, INT_1:def 2; :: thesis: verum

end;

reconsider g = ((In (m,F_Rat)) | F_Rat) *' (~ f0) as INT -valued Polynomial of F_Rat by A14, RELAT_1:def 19, A8;
A16: Ext_eval (g,x) = (Ext_eval (((In (m,F_Rat)) | F_Rat),x)) * (0. F_Complex) by A4, ALGNUM_1:3, ALGNUM_1:20
.= 0 by MATRIX_5:2 ;
take g ; :: thesis: ( @ g is irreducible & Ext_eval (g,(In (number_e,F_Real))) = 0 & deg g >= 2 & g . 0 <> 0. F_Rat )
@ g = m * f0 by Lm8a;
then A18: @ g is irreducible by A7, E_TRANS1:12;
reconsider FR = F_Real as Subring of F_Complex by LIOUVIL2:3;
g is Polynomial of F_Real by FIELD_4:8;
then reconsider g1 = g as Element of the carrier of (Polynom-Ring F_Real) by POLYNOM3:def 10;
g is Polynomial of F_Complex by FIELD_4:8;
then reconsider gc = g as Element of the carrier of (Polynom-Ring F_Complex) by POLYNOM3:def 10;
reconsider g0 = g as Element of the carrier of (Polynom-Ring F_Rat) by POLYNOM3:def 10;
A19: Ext_eval (g0,x) = 0 by A16;
A20: Ext_eval (g0,e1) = eval (g1,e1) by FIELD_4:26
.= eval (gc,x) by A2, FIELD_4:27
.= 0 by A19, FIELD_4:26 ;
then deg g >= 2 by A18, E_TRANS1:13;
hence ( @ g is irreducible & Ext_eval (g,(In (number_e,F_Real))) = 0 & deg g >= 2 & g . 0 <> 0. F_Rat ) by A18, A20, E_TRANS1:14; :: thesis: verum