let a, b be non square Element of NAT ; :: thesis: ( a,b are_coprime implies not a * b is square )
assume A1: a,b are_coprime ; :: thesis: not a * b is square
assume a * b is square ; :: thesis: contradiction
then consider k being Nat such that
A2: a * b = k ^2 by PYTHTRIP:def 3;
ex k being Nat st k |^ 2 = a by A1, A2, NEWTON02:30;
hence contradiction ; :: thesis: verum