let n1, n2, m2, m1 be Nat; :: thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies n1 <= n2 )

assume A1: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; :: thesis: n1 <= n2

assume A2: n1 > n2 ; :: thesis: contradiction

then consider n being Nat such that

A3: n1 = n2 + n by NAT_1:10;

n <> 0 by A2, A3;

then consider k being Nat such that

A4: n = k + 1 by NAT_1:6;

A5: 2 |^ n2 <> 0 by Th3;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

2 |^ n1 = (2 |^ n2) * (2 |^ (k + 1)) by A3, A4, NEWTON:8;

then (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 |^ (k + 1)) * ((2 * m1) + 1)) ;

then (2 |^ (k + 1)) * ((2 * m1) + 1) = (2 * m2) + 1 by A1, A5, XCMPLX_1:5;

then (2 * m2) + 1 = ((2 |^ k) * (2 |^ 1)) * ((2 * m1) + 1) by NEWTON:8

.= (2 * (2 |^ k)) * ((2 * m1) + 1)

.= 2 * ((2 |^ k) * ((2 * m1) + 1)) ;

then A6: 2 divides (2 * m2) + 1 by NAT_D:def 3;

2 divides 2 * m2 by NAT_D:def 3;

hence contradiction by A6, NAT_D:7, NAT_D:10; :: thesis: verum

assume A1: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; :: thesis: n1 <= n2

assume A2: n1 > n2 ; :: thesis: contradiction

then consider n being Nat such that

A3: n1 = n2 + n by NAT_1:10;

n <> 0 by A2, A3;

then consider k being Nat such that

A4: n = k + 1 by NAT_1:6;

A5: 2 |^ n2 <> 0 by Th3;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

2 |^ n1 = (2 |^ n2) * (2 |^ (k + 1)) by A3, A4, NEWTON:8;

then (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 |^ (k + 1)) * ((2 * m1) + 1)) ;

then (2 |^ (k + 1)) * ((2 * m1) + 1) = (2 * m2) + 1 by A1, A5, XCMPLX_1:5;

then (2 * m2) + 1 = ((2 |^ k) * (2 |^ 1)) * ((2 * m1) + 1) by NEWTON:8

.= (2 * (2 |^ k)) * ((2 * m1) + 1)

.= 2 * ((2 |^ k) * ((2 * m1) + 1)) ;

then A6: 2 divides (2 * m2) + 1 by NAT_D:def 3;

2 divides 2 * m2 by NAT_D:def 3;

hence contradiction by A6, NAT_D:7, NAT_D:10; :: thesis: verum