let m, n be non zero Nat; :: thesis: ( n > ((2 |^ m) - 1) * ((((2 |^ m) - 1) |^ m) - 1) implies ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l) )
assume A1: n > ((2 |^ m) - 1) * ((((2 |^ m) - 1) |^ m) - 1) ; :: thesis: ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)
reconsider a = (2 |^ m) - 1 as non zero Nat ;
0 + 1 <= m by NAT_1:13;

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

suppose O1: m = 1 ; :: thesis: ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)

set k = n;
set l = 1;
(((2 |^ m) - 1) * n) + (((((2 |^ m) - 1) |^ m) - 1) * 1) = n by O1;
hence ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l) ; :: thesis: verum

end;

suppose m > 1 ; :: thesis: ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)

then 2 to_power m > 2 to_power 1 by POWER:39;
then (2 to_power m) - 1 > 2 - 1 by XREAL_1:6;
then A0: (2 |^ m) - 1 > 1 ;
((2 |^ m) - 1) to_power 0 < ((2 |^ m) - 1) to_power m by A0, POWER:39;
then reconsider b = (((2 |^ m) - 1) |^ m) - 1 as non zero Nat by NEWTON:4;
a,b are_coprime by CoprimeProof;
then consider x, y being non zero Nat such that
A2: n = (a * x) + (b * y) by A1, SierpCorr2;
thus ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l) by A2; :: thesis: verum

end;

end;