let n, x, y be Nat; :: thesis: ( n > 1 & x >= 1 & 1 = (((x * y) * n) + x) + y implies ( x = 1 & y = 0 ) )
assume that
A1: n > 1 and
A2: x >= 1 and
A3: 1 = (((x * y) * n) + x) + y ; :: thesis: ( x = 1 & y = 0 )
now :: thesis: ( x = 1 & y = 0 )
per cases ( x > 1 or x = 1 ) by A2, XXREAL_0:1;
suppose A4: x > 1 ; :: thesis: ( x = 1 & y = 0 )
now :: thesis: ( x = 1 & y = 0 )
per cases ( y > 0 or y = 0 ) ;
suppose A5: y > 0 ; :: thesis: ( x = 1 & y = 0 )
then x * y > 1 * y by A4, XREAL_1:68;
then (x * y) * n > 1 * (x * y) by A1, XREAL_1:68;
then ((x * y) * n) + x > 0 + x by XREAL_1:6;
then A6: ((x * y) * n) + x > 1 by A4, XXREAL_0:2;
y + 1 > 0 + 1 by A5, XREAL_1:6;
hence ( x = 1 & y = 0 ) by A3, A6, XREAL_1:6; :: thesis: verum
end;
suppose y = 0 ; :: thesis: ( x = 1 & y = 0 )
hence ( x = 1 & y = 0 ) by A3; :: thesis: verum
end;
end;
end;
hence ( x = 1 & y = 0 ) ; :: thesis: verum
end;
suppose A7: x = 1 ; :: thesis: ( x = 1 & y = 0 )
now :: thesis: ( x = 1 & y = 0 )
per cases ( y > 0 or y = 0 ) ;
suppose A8: y > 0 ; :: thesis: ( x = 1 & y = 0 )
then (x * y) * n > 0 by A1, A7, XREAL_1:68;
then A9: ((x * y) * n) + x > 0 + 1 by A7, XREAL_1:6;
y + 1 > 0 + 1 by A8, XREAL_1:6;
hence ( x = 1 & y = 0 ) by A3, A9, XREAL_1:6; :: thesis: verum
end;
suppose y = 0 ; :: thesis: ( x = 1 & y = 0 )
hence ( x = 1 & y = 0 ) by A7; :: thesis: verum
end;
end;
end;
hence ( x = 1 & y = 0 ) ; :: thesis: verum
end;
end;
end;
hence ( x = 1 & y = 0 ) ; :: thesis: verum