let n, x, y, z, t be positive Nat; :: thesis: ( x <= y & y <= z implies ( ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t iff ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) ) )
assume that
A1: x <= y and
A2: y <= z ; :: thesis: ( ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t iff ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) )
thus ( not ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t or ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) :: thesis: ( ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) implies ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t )
proof
assume A3: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
reconsider yx = y - x as Element of NAT by A1, INT_1:5;
reconsider zx = z - x as Element of NAT by A1, A2, XXREAL_0:2, INT_1:5;
n <> 1 by A3;
then A4: n >= 2 by NAT_1:23;
then A5: n >= 1 by XXREAL_0:2;
then A6: n |^ x <= n |^ y by A1, PREPOWER:93;
n |^ y <= n |^ z by A2, A5, PREPOWER:93;
then A7: (n |^ x) + (n |^ y) <= (n |^ y) + (n |^ z) by A6, XREAL_1:7;
per cases ( n = 2 or n > 2 ) by A4, XXREAL_0:1;
suppose A8: n = 2 ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
A9: now :: thesis: not t - x <= 1
assume t - x <= 1 ; :: thesis: contradiction
then A10: (t - x) + x <= 1 + x by XREAL_1:6;
n |^ (1 + x) = (n |^ 1) * (n |^ x) by NEWTON:8;
then (((n |^ x) + (n |^ y)) + (n |^ z)) - (n |^ x) <= (n * (n |^ x)) - (n |^ x) by A3, A5, A10, PREPOWER:93, XREAL_1:9;
then (n |^ x) + (n |^ y) <= (n - 1) * (n |^ x) by A7, XXREAL_0:2;
then ((n |^ x) + (n |^ y)) - (n |^ x) <= ((n - 1) * (n |^ x)) - (n |^ x) by XREAL_1:9;
then n |^ y <= 0 by A8;
hence contradiction ; :: thesis: verum
end;
then reconsider tx = t - x as non zero Element of NAT by INT_1:3;
A11: ( 2 to_power yx = (2 to_power y) / (2 to_power x) & 2 to_power zx = (2 to_power z) / (2 to_power x) & 2 to_power tx = (2 to_power t) / (2 to_power x) ) by POWER:29;
A12: (((n |^ x) / (n |^ x)) + ((n |^ y) / (n |^ x))) + ((n |^ z) / (n |^ x)) = (n |^ t) / (n |^ x) by A3;
then A13: (1 + (2 |^ yx)) + (2 |^ zx) = 2 |^ tx by A8, A11, XCMPLX_1:60;
A14: 2 to_power ((zx - 1) + 1) = (2 to_power (zx - 1)) * (2 to_power 1) by POWER:27;
A15: 2 to_power ((tx - 1) + 1) = (2 to_power (tx - 1)) * (2 to_power 1) by POWER:27;
A16: now :: thesis: not y > x
assume A17: y > x ; :: thesis: contradiction
then reconsider yx = yx as non zero Element of NAT ;
reconsider zx = zx as non zero Element of NAT by A2, A17;
( 2 |^ yx is even & 2 |^ zx is even & 2 |^ tx is even ) ;
hence contradiction by A8, A11, A12; :: thesis: verum
end;
then A18: x = y by A1, XXREAL_0:1;
then A19: (1 + 1) + (2 |^ zx) = 2 |^ tx by A13, NEWTON:4;
then 2 + (2 |^ ((zx - 1) + 1)) = 2 |^ ((tx - 1) + 1) ;
then A20: 1 + (2 to_power (zx - 1)) = 2 to_power (tx - 1) by A14, A15;
A21: now :: thesis: not zx <> 1
assume zx <> 1 ; :: thesis: contradiction
per cases then ( zx < 1 or zx > 1 ) by XXREAL_0:1;
suppose zx > 1 ; :: thesis: contradiction
then reconsider zx1 = zx - 1 as non zero Element of NAT by INT_1:3;
reconsider tx1 = tx - 1 as non zero Element of NAT by A9, INT_1:3;
A22: (2 / 2) + ((2 |^ zx) / 2) = (2 |^ tx) / 2 by A19;
( (2 to_power zx) / (2 to_power 1) = 2 to_power zx1 & (2 to_power tx) / (2 to_power 1) = 2 to_power tx1 ) by POWER:29;
hence contradiction by A22; :: thesis: verum
end;
end;
end;
then 1 + 1 = 2 to_power (tx - 1) by A20, POWER:24;
then 2 to_power 1 = 2 to_power (tx - 1) ;
then tx - 1 = 1 by Th48;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A1, A8, A16, A21, XXREAL_0:1; :: thesis: verum
end;
suppose A23: n > 2 ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
reconsider yx = y - x as Element of NAT by A1, INT_1:5;
reconsider zx = z - x as Element of NAT by A1, A2, XXREAL_0:2, INT_1:5;
set tx = t - x;
A24: ( n to_power yx = (n to_power y) / (n to_power x) & n to_power zx = (n to_power z) / (n to_power x) & n to_power (t - x) = (n to_power t) / (n to_power x) ) by POWER:29;
A25: (((n |^ x) / (n |^ x)) + ((n |^ y) / (n |^ x))) + ((n |^ z) / (n |^ x)) = (n |^ t) / (n |^ x) by A3;
then A26: (1 + (n |^ yx)) + (n |^ zx) = n to_power (t - x) by A24, XCMPLX_1:60;
1 + (n |^ yx) > 1 + 0 by XREAL_1:6;
then A27: (1 + (n |^ yx)) + (n |^ zx) > 1 + 0 by XREAL_1:8;
A28: n > 1 by A23, XXREAL_0:2;
now :: thesis: not x >= t
assume x >= t ; :: thesis: contradiction
then t - x <= t - t by XREAL_1:10;
end;
then reconsider tx = t - x as non zero Element of NAT by INT_1:5;
A29: (n |^ yx) mod n = ((n mod n) |^ yx) mod n by GR_CY_3:30;
A30: (n |^ zx) mod n = ((n mod n) |^ zx) mod n by GR_CY_3:30;
A31: (n |^ tx) mod n = ((n mod n) |^ tx) mod n by GR_CY_3:30;
per cases ( x < y or x >= y ) ;
suppose A32: x < y ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then reconsider yx = yx as non zero Element of NAT ;
reconsider zx = zx as non zero Element of NAT by A2, A32;
(((n |^ x) / (n |^ x)) + ((n |^ y) / (n |^ x))) + ((n |^ z) / (n |^ x)) = (n |^ t) / (n |^ x) by A3;
then A33: (1 + (n |^ yx)) + (n |^ zx) = n to_power tx by A24, XCMPLX_1:60;
((1 + (n |^ yx)) + (n |^ zx)) mod n = (((1 mod n) + ((n |^ yx) mod n)) + ((n |^ zx) mod n)) mod n by NUMBER05:8
.= 1 by A28, A29, A30, NAT_D:14 ;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A31, A33; :: thesis: verum
end;
suppose x >= y ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then A34: x = y by A1, XXREAL_0:1;
then A35: (1 + 1) + (n |^ zx) = n to_power tx by A26, NEWTON:4;
A36: 2 mod n = 2 by A23, NAT_D:24;
per cases ( zx <= 0 or zx > 0 ) ;
suppose zx <= 0 ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then A37: zx = 0 ;
n >= 2 + 1 by A23, NAT_1:13;
per cases then ( n > 3 or n = 3 ) by XXREAL_0:1;
suppose n > 3 ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then 3 = (2 + 1) mod n by NAT_D:24
.= (2 + (n |^ zx)) mod n by A37, NEWTON:4 ;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A31, A35; :: thesis: verum
end;
suppose A38: n = 3 ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
3 * (3 |^ x) = 3 |^ (x + 1) by NEWTON:6;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A3, A34, A37, A38, PEPIN:30; :: thesis: verum
end;
end;
end;
suppose zx > 0 ; :: thesis: ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) )
then A39: zx >= 0 + 1 by NAT_1:13;
(2 + (n |^ zx)) mod n = (2 + ((0 |^ zx) mod n)) mod n by A30, A36, NAT_D:66
.= (2 + (0 mod n)) mod n by A39, NEWTON:11
.= 2 by A23, NAT_D:24 ;
hence ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) by A31, A35; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
assume ( ( n = 2 & y = x & z = x + 1 & t = x + 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 = 3 & y = x & z = x & t = x + 1 ) ) ;
suppose A40: ( n = 2 & y = x & z = x + 1 & t = x + 2 ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
( 2 |^ (x + 1) = (2 |^ x) * (2 |^ 1) & 2 |^ (x + 2) = (2 |^ x) * (2 |^ 2) ) by NEWTON:8;
hence ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t by A40, Lm2; :: thesis: verum
end;
suppose A41: ( n = 3 & y = x & z = x & t = x + 1 ) ; :: thesis: ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t
3 |^ (x + 1) = (3 |^ x) * 3 by NEWTON:6;
hence ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t by A41; :: thesis: verum
end;
end;