let a be Rational; :: thesis: for b being irrational Real st a <> 0 holds
a * b is irrational
let b be irrational Real; :: thesis: ( a <> 0 implies a * b is irrational )
assume A1: a <> 0 ; :: thesis: a * b is irrational
assume a * b is rational ; :: thesis: contradiction
then consider m, n being Integer such that
n <> 0 and
A2: a * b = m / n by RAT_1:2;
consider m1, n1 being Integer such that
n1 <> 0 and
A3: a = m1 / n1 by RAT_1:2;
(a * b) / a = (m * n1) / (n * m1) by A2, A3, XCMPLX_1:84;
hence contradiction by A1, XCMPLX_1:89; :: thesis: verum