assume a / b is integer ; :: thesis: contradiction
then (a / b) * b is integer ;
hence contradiction by XCMPLX_1:87; :: thesis: verum