theorem LMM: :: E_TRANS2:41

( number_e is algebraic implies 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 ) )