let x, y, z, t be positive Nat; :: thesis: ( x <= y & x <= z & z <= t implies ( ( x + y = z * t & z + t = x * y ) iff ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) ) )
assume that
A1: x <= y and
A2: x <= z and
A3: z <= t ; :: thesis: ( ( x + y = z * t & z + t = x * y ) iff ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) )
thus ( x + y = z * t & z + t = x * y & not ( x = 1 & y = 5 & z = 2 & t = 3 ) implies ( x = 2 & y = 2 & z = 2 & t = 2 ) ) :: thesis: ( ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) implies ( x + y = z * t & z + t = x * y ) )

proof

assume that
A4: x + y = z * t and
A5: z + t = x * y ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

per cases ( x <= 2 or x > 2 ) ;

suppose x <= 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

then not not x = 0 & ... & not x = 2 ;

per cases then ( x = 1 or x = 2 ) ;

suppose A6: x = 1 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

then z <> 1 by A4, A5;
then ( z < 0 + 1 or z > 1 ) by XXREAL_0:1;
then z >= 1 + 1 by NAT_1:13;

per cases then ( z = 2 or z > 2 ) by XXREAL_0:1;

suppose z = 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

hence ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) by A4, A5, A6; :: thesis: verum

end;

suppose A7: z > 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

then reconsider z1 = z - 2 as Element of NAT by INT_1:5;
A8: t > 2 by A3, A7, XXREAL_0:2;
reconsider t1 = t - 2 as Element of NAT by A3, A7, XXREAL_0:2, INT_1:5;
A9: (z + t) + 3 = (z1 + t1) + 7 ;
( 2 + 1 <= z & 2 + 1 <= t ) by A7, A8, NAT_1:13;
then A10: ( 3 - 2 <= z1 & 3 - 2 <= t1 ) by XREAL_1:9;
then A11: 1 + 1 <= z1 + t1 by XREAL_1:7;
1 * 1 <= z1 * t1 by A10, XREAL_1:66;
then 1 + 2 <= (z1 * t1) + (t1 + z1) by A11, XREAL_1:7;
then 3 + (t1 + z1) <= (((z1 * t1) + t1) + z1) + (t1 + z1) by XREAL_1:6;
then ((z1 + t1) + 3) + 4 <= (((z1 * t1) + (2 * t1)) + (2 * z1)) + 4 by XREAL_1:6;
hence ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) by A4, A5, A6, A9, XREAL_1:8; :: thesis: verum

end;

end;

end;

suppose A12: x = 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

per cases then ( z = 2 or z > 2 ) by A2, XXREAL_0:1;

suppose z = 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

hence ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) by A4, A5, A12; :: thesis: verum

end;

suppose A13: z > 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

then reconsider z1 = z - 2 as Element of NAT by INT_1:5;
A14: t > 2 by A3, A13, XXREAL_0:2;
reconsider t1 = t - 2 as Element of NAT by A3, A13, XXREAL_0:2, INT_1:5;
( 2 + 1 <= z & 2 + 1 <= t ) by A13, A14, NAT_1:13;
then A15: ( 3 - 2 <= z1 & 3 - 2 <= t1 ) by XREAL_1:9;
then A16: 1 + 1 <= z1 + t1 by XREAL_1:7;
1 * 1 <= z1 * t1 by A15, XREAL_1:66;
then 1 + 2 <= (z1 * t1) + (t1 + z1) by A16, XREAL_1:7;
then 3 + (t1 + z1) <= (((z1 * t1) + t1) + z1) + (t1 + z1) by XREAL_1:6;
then ((z1 + t1) + 3) + 4 <= (((z1 * t1) + (2 * t1)) + (2 * z1)) + 4 by XREAL_1:6;
then ((z + t) + 3) - 2 <= (((1 / 2) * (z + t)) + 2) - 2 by A4, A5, A12, XREAL_1:9;
then 2 * ((z + t) + 1) <= 2 * ((1 / 2) * (z + t)) by XREAL_1:64;
then (z + t) + ((z + t) + 2) <= (z + t) + 0 ;
hence ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) by XREAL_1:6; :: thesis: verum

end;

end;

end;

end;

end;

suppose A17: x > 2 ; :: thesis: ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) )

then A18: z > 2 by A2, XXREAL_0:2;
reconsider z1 = z - 2 as Element of NAT by A2, A17, XXREAL_0:2, INT_1:5;
reconsider t1 = t - 2 as Element of NAT by A3, A18, XXREAL_0:2, INT_1:5;
A19: z - 2 > 2 - 2 by A18, XREAL_1:8;
t > 2 by A3, A18, XXREAL_0:2;
then t - 2 > 2 - 2 by XREAL_1:8;
then 0 + 1 <= t1 by NAT_1:13;
then A20: 1 * 1 <= z1 * t1 by A19, NAT_1:13;
z1 <= t1 by A3, XREAL_1:9;
then A21: z1 + t1 <= t1 + t1 by XREAL_1:6;
A22: 2 + 1 <= x by A17, NAT_1:13;
then consider b being Nat such that
A23: y = 3 + b by A1, XXREAL_0:2, NAT_1:10;
consider a being Nat such that
A24: x = 3 + a by A22, NAT_1:10;

now :: thesis: not (x + y) + 3 > x * y

assume (x + y) + 3 > x * y ; :: thesis: contradiction
then 9 + (a + b) > 9 + (((3 * a) + (3 * b)) + (a * b)) by A23, A24;
then a + b > a + (((2 * a) + (3 * b)) + (a * b)) by XREAL_1:6;
then 0 + b > b + (((2 * a) + (2 * b)) + (a * b)) by XREAL_1:6;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then A25: ((x + y) + 3) + 3 <= (x * y) + 3 by XREAL_1:6;
0 + 1 <= z1 by A19, NAT_1:13;
then 2 * 1 <= 2 * z1 by XREAL_1:64;
then 1 + 2 <= (z1 * t1) + (2 * z1) by A20, XREAL_1:7;
then 3 + 4 <= ((z1 * t1) + (2 * z1)) + 4 by XREAL_1:7;
then (z1 + t1) + 7 <= (2 * t1) + (((z1 * t1) + (2 * z1)) + 4) by A21, XREAL_1:7;
then (x + y) + 6 <= (x + y) + 0 by A4, A5, A25, XXREAL_0:2;
hence ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) by XREAL_1:6; :: thesis: verum

end;

end;

end;

thus ( ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) implies ( x + y = z * t & z + t = x * y ) ) ; :: thesis: verum