let a, b be square Nat; :: thesis: ( a,b are_coprime implies not 3 divides a + b )
assume A1: a,b are_coprime ; :: thesis: not 3 divides a + b
consider x being Nat such that
A2: a = x ^2 by PYTHTRIP:def 3;
consider y being Nat such that
A3: b = y ^2 by PYTHTRIP:def 3;
A4: ( x ^2 = x |^ 2 & y ^2 = y |^ 2 ) by NEWTON:81;
1 = 2 -root (1 |^ 2)
.= 2 -root ((x gcd y) |^ 2) by A1, A2, A3, A4, NEWTON03:4
.= x gcd y ;
then x,y are_coprime ;
hence not 3 divides a + b by A2, A3, A4, NEWTON02:193; :: thesis: verum