let n be non empty Nat; :: thesis: for k, l, m being Nat st m < n & k mod (2 to_power n) = l mod (2 to_power n) holds
(k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
let k, l, m be Nat; :: thesis: ( m < n & k mod (2 to_power n) = l mod (2 to_power n) implies (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2 )
assume A1: ( m < n & k mod (2 to_power n) = l mod (2 to_power n) ) ; :: thesis: (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
2 to_power n = 2 |^ n by POWER:46;
then not 2 to_power n is empty by PREPOWER:12;
then consider s being Integer such that
A2: k = l + (s * (2 to_power n)) by A1, Lm2;
consider j being Nat such that
A3: n = m + j by A1, NAT_1:10;
reconsider j = j as Nat ;
set M = 2 to_power m;
set J = 2 to_power j;
reconsider L = l as Integer ;
A4: 2 to_power m > 0 by POWER:39;
m + (- m) < n + (- m) by A1, XREAL_1:10;
then 0 + 1 < j + 1 by A3, XREAL_1:10;
then 1 <= j by NAT_1:13;
then 2 to_power 1 divides 2 to_power j by NAT_2:13;
then 2 divides 2 to_power j by POWER:30;
then (2 to_power j) mod 2 = 0 by PEPIN:6;
then A5: (s * (2 to_power j)) mod 2 = ((s mod 2) * 0 ) mod 2 by INT_3:15
.= 0 by NAT_D:26 ;
k div (2 to_power m) = (l + (s * ((2 to_power j) * (2 to_power m)))) div (2 to_power m) by A2, A3, POWER:32
.= (l + ((s * (2 to_power j)) * (2 to_power m))) div (2 to_power m)
.= (l div (2 to_power m)) + (s * (2 to_power j)) by A4, INT_3:8 ;
then (k div (2 to_power m)) mod 2 = (((L div (2 to_power m)) mod 2) + 0 ) mod 2 by A5, INT_3:14
.= (L div (2 to_power m)) mod 2 by INT_3:13 ;
hence (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2 ; :: thesis: verum