let a be non zero square Integer; :: thesis: for b being Integer st a * b is square holds
b is square
let b be Integer; :: thesis: ( a * b is square implies b is square )
assume A1: a * b is square ; :: thesis: b is square
consider x being Nat such that
A2: a = x ^2 by PYTHTRIP:def 3;
consider y being Nat such that
A3: a * b = y ^2 by A1, PYTHTRIP:def 3;
x ^2 divides y ^2 by A2, A3;
then |.x.| divides |.y.| by PYTHTRIP:6;
then consider k being Integer such that
A4: y = k * x ;
A5: ( k * k = k ^2 & x * x = x ^2 & y * y = y ^2 ) by SQUARE_1:def 1;
a * b = a * (k ^2) by A2, A3, A4, A5;
then b = k ^2 by XCMPLX_1:5
.= |.k.| ^2 by COMPLEX1:75 ;
hence b is square ; :: thesis: verum