let n be non zero Nat; :: thesis: for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds
n -BinarySequence l = n -BinarySequence m
let l, m be Nat; :: thesis: ( l mod (2 to_power n) = m mod (2 to_power n) implies n -BinarySequence l = n -BinarySequence m )
assume A1: l mod (2 to_power n) = m mod (2 to_power n) ; :: thesis: n -BinarySequence l = n -BinarySequence m
|.m.| = m by ABSVALUE:def 1;
then A2: 2sComplement (n,m) = n -BinarySequence m by Def2;
|.l.| = l by ABSVALUE:def 1;
then 2sComplement (n,l) = n -BinarySequence l by Def2;
hence n -BinarySequence l = n -BinarySequence m by A1, A2, Lm5; :: thesis: verum