let n, x, y, z, t be positive Nat; :: thesis: ( ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t iff ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) )
A1: ((n |^ x) + (n |^ y)) + (n |^ z) = ((n |^ z) + (n |^ y)) + (n |^ x) ;
A2: ((n |^ x) + (n |^ y)) + (n |^ z) = ((n |^ x) + (n |^ z)) + (n |^ y) ;
A3: ((n |^ x) + (n |^ y)) + (n |^ z) = ((n |^ y) + (n |^ z)) + (n |^ x) ;
A4: ((n |^ x) + (n |^ y)) + (n |^ z) = ((n |^ z) + (n |^ x)) + (n |^ y) ;
thus ( not ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t or ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) :: thesis: ( ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) implies ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t )
proof
assume A5: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
per cases ( ( x <= y & y <= z ) or ( x <= z & z <= y ) or ( y <= x & x <= z ) or ( y <= z & z <= x ) or ( z <= x & x <= y ) or ( z <= y & y <= x ) ) ;
suppose ( x <= y & y <= z ) ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A5, Th49; :: thesis: verum
end;
suppose ( x <= z & z <= y ) ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A2, A5, Th49; :: thesis: verum
end;
suppose ( y <= x & x <= z ) ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then ( ( n = 2 & y = x & z = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = y & t = y + 1 ) ) by A5, Th49;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ; :: thesis: verum
end;
suppose ( y <= z & z <= x ) ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then ( ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & z = y & x = y & t = y + 1 ) ) by A3, A5, Th49;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ; :: thesis: verum
end;
suppose ( z <= x & x <= y ) ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then ( ( n = 2 & x = z & y = z + 1 & t = z + 2 ) or ( n = 3 & x = z & y = z & t = z + 1 ) ) by A4, A5, Th49;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ; :: thesis: verum
end;
suppose ( z <= y & y <= x ) ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then ( ( n = 2 & y = z & x = z + 1 & t = z + 2 ) or ( n = 3 & y = z & z = x & t = z + 1 ) ) by A1, A5, Th49;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ; :: thesis: verum
end;
end;
end;
A6: x + 0 <= x + 1 by XREAL_1:6;
A7: y + 0 <= y + 1 by XREAL_1:6;
assume ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
per cases then ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ;
suppose ( n = 2 & y = x & z = x + 1 & t = x + 2 ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
hence ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t by A6, Th49; :: thesis: verum
end;
suppose ( n = 2 & y = x + 1 & z = x & t = x + 2 ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
hence ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t by A2, A6, Th49; :: thesis: verum
end;
suppose ( n = 2 & z = y & x = y + 1 & t = y + 2 ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
hence ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t by A1, A7, Th49; :: thesis: verum
end;
suppose ( n = 3 & y = x & z = x & t = x + 1 ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
hence ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t by Th49; :: thesis: verum
end;
end;