let a, b be Nat; :: thesis: ( a,b are_coprime implies not 3 divides ((a + b) * (a - b)) + (a * b) )
assume a,b are_coprime ; :: thesis: not 3 divides ((a + b) * (a - b)) + (a * b)
then ( not 3 divides a or not 3 divides b ) by PYTHTRIP:def 1;
hence not 3 divides ((a + b) * (a - b)) + (a * b) by Th51; :: thesis: verum