consider m being Integer such that
A1: p = m / (denominator p) by Def3;
denominator p <> 0 by Def3;
hence (denominator p) * p is Integer by A1, XCMPLX_1:88; :: thesis: verum