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