let c be Element of F_Complex; :: thesis: ( c is algebraic iff ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f )
hereby :: thesis: ( ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f implies c is algebraic )
assume c is algebraic ; :: thesis: ex f1 being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f1
then c is_integral_over F_Rat ;
then consider f being Polynomial of F_Rat such that
A1: LC f = 1. F_Rat and
A2: Ext_eval (f,c) = 0. F_Complex ;
reconsider f1 = f as RAT -valued Polynomial of F_Complex by ALGNUM_1:3, Th8;
f1 is monic by A1, Th9, Lm2, ALGNUM_1:3;
then reconsider f1 = f1 as RAT -valued monic Polynomial of F_Complex ;
take f1 = f1; :: thesis: c is_a_root_of f1
thus c is_a_root_of f1 :: thesis: verum
proof
thus eval (f1,c) = In ((eval (f1,c)),F_Complex)
.= Ext_eval (f1,(In (c,F_Complex))) by Lm3, ALGNUM_1:12
.= 0. F_Complex by A2, Th15, ALGNUM_1:3 ; :: according to POLYNOM5:def 7 :: thesis: verum
end;
end;
given f1 being RAT -valued monic Polynomial of F_Complex such that A3: c is_a_root_of f1 ; :: thesis: c is algebraic
reconsider f = f1 as Polynomial of F_Rat by Th21;
take f ; :: according to ALGNUM_1:def 2,ALGNUM_1:def 5 :: thesis: ( Leading-Coefficient f = 1. F_Rat & Ext_eval (f,c) = 0. F_Complex )
LC f1 = 1. F_Complex by RATFUNC1:def 7;
hence LC f = 1. F_Rat by Th9, Lm2, ALGNUM_1:3; :: thesis: Ext_eval (f,c) = 0. F_Complex
thus Ext_eval (f,c) = Ext_eval (f1,(In (c,F_Complex))) by Th15, ALGNUM_1:3
.= In ((eval (f1,c)),F_Complex) by Lm3, ALGNUM_1:12
.= 0. F_Complex by A3 ; :: thesis: verum