let p be INT -valued monic Polynomial of F_Real; :: thesis: for e being rational Element of F_Real st e is_a_root_of p holds
e is integer
let e be rational Element of F_Real; :: thesis: ( e is_a_root_of p implies e is integer )
assume A1: e is_a_root_of p ; :: thesis: e is integer
set k = numerator e;
set n = denominator e;
A2: e = (numerator e) / (denominator e) by RAT_1:15;
A3: numerator e, denominator e are_coprime by WSIERP_1:22;
p is monic ;
then ( denominator e = 1 or denominator e = - 1 ) by A1, A2, A3, Th50, INT_2:13;
hence e is integer by A2; :: thesis: verum