let n1, n2, m1, m2 be Nat; ( (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)
; n1 <= n2
assume A2:
n1 > n2
; 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 Th87;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
2 |^ n1 = (2 |^ n2) * (2 |^ (k + 1))
by A3, A4, Th8;
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 Th8
.=
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; verum