let n be non zero Nat; 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; ( 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 that
A1:
m < n
and
A2:
k mod (2 to_power n) = l mod (2 to_power n)
; (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
consider j being Nat such that
A3:
n = m + j
by A1, NAT_1:10;
2 to_power n = 2 |^ n
by POWER:41;
then
not 2 to_power n is zero
by PREPOWER:5;
then consider s being Integer such that
A4:
k = l + (s * (2 to_power n))
by A2, Lm2;
reconsider j = j as Nat ;
set M = 2 to_power m;
set J = 2 to_power j;
m + (- m) < n + (- m)
by A1, XREAL_1:8;
then
0 + 1 < j + 1
by A3, XREAL_1:8;
then
1 <= j
by NAT_1:13;
then
2 to_power 1 divides 2 to_power j
by NAT_2:11;
then
2 divides 2 to_power j
by POWER:25;
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 NAT_D:67
.=
0
by NAT_D:26
;
reconsider L = l as Integer ;
A6:
2 to_power m > 0
by POWER:34;
k div (2 to_power m) =
(l + (s * ((2 to_power j) * (2 to_power m)))) div (2 to_power m)
by A4, A3, POWER:27
.=
(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 A6, NAT_D:61
;
then (k div (2 to_power m)) mod 2 =
(((L div (2 to_power m)) mod 2) + 0) mod 2
by A5, NAT_D:66
.=
(L div (2 to_power m)) mod 2
by NAT_D:65
;
hence
(k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
; verum