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