let a be rational number ; :: thesis: for b being real irrational number st a <> 0 holds
a * b is irrational
let b be real irrational number ; :: thesis: ( a <> 0 implies a * b is irrational )
assume A1: a <> 0 ; :: thesis: a * b is irrational
assume not a * b is irrational ; :: thesis: contradiction
then consider m, n being Integer such that
A2: ( n <> 0 & a * b = m / n ) by RAT_1:3;
consider m1, n1 being Integer such that
A3: ( n1 <> 0 & a = m1 / n1 ) by RAT_1:3;
(a * b) / a = (m * n1) / (n * m1) by A2, A3, XCMPLX_1:85;
hence contradiction by A1, XCMPLX_1:90; :: thesis: verum