let n1, m1, n2, m2 be natural number ; :: thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies ( n1 = n2 & m1 = m2 ) )
A1: 2 |^ n1 <> 0 by Th106;
assume A2: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; :: thesis: ( n1 = n2 & m1 = m2 )
then A3: n2 <= n1 by Lm4;
n1 <= n2 by A2, Lm4;
hence n1 = n2 by A3, XXREAL_0:1; :: thesis: m1 = m2
then (2 * m1) + 1 = (2 * m2) + 1 by A2, A1, XCMPLX_1:5;
hence m1 = m2 ; :: thesis: verum