per cases ( n >= m or m > n ) ;
suppose n >= m ; :: thesis: not (a |^ n) + (a |^ m) is square
then consider x being Nat such that
A1: n = m + x by NAT_1:10;
reconsider l = a |^ x as non zero square Integer ;
(a |^ (m + x)) + (a |^ m) = ((a |^ m) * (a |^ x)) + (a |^ m) by NEWTON:8
.= (l + 1) * (a |^ m) ;
hence not (a |^ n) + (a |^ m) is square by A1; :: thesis: verum
end;
suppose m > n ; :: thesis: not (a |^ n) + (a |^ m) is square
then consider x being Nat such that
A1: m = n + x by NAT_1:10;
reconsider l = a |^ x as non zero square Integer ;
(a |^ (n + x)) + (a |^ n) = ((a |^ n) * (a |^ x)) + (a |^ n) by NEWTON:8
.= (l + 1) * (a |^ n) ;
hence not (a |^ n) + (a |^ m) is square by A1; :: thesis: verum
end;
end;