let x1, x2, y1, y2, p1, p2 be Nat; :: thesis: ( x1 + (y1 / (2 |^ p1)) = x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 implies x1 = x2 )
assume A1: ( x1 + (y1 / (2 |^ p1)) = x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 ) ; :: thesis: x1 = x2
( 0 <= y1 / (2 |^ p1) & y1 / (2 |^ p1) < 1 & 0 <= y2 / (2 |^ p2) & y2 / (2 |^ p2) < 1 ) by A1, XREAL_1:189;
then ( x1 + 0 <= x1 + (y1 / (2 |^ p1)) & x1 + (y1 / (2 |^ p1)) < x1 + 1 & x2 + 0 <= x2 + (y2 / (2 |^ p2)) & x2 + (y2 / (2 |^ p2)) < x2 + 1 ) by XREAL_1:6;
then ( x1 < x2 + 1 & x2 < x1 + 1 ) by A1, XXREAL_0:2;
then ( x1 <= x2 & x2 <= x1 ) by NAT_1:13;
hence x1 = x2 by XXREAL_0:1; :: thesis: verum