let n be non empty Nat; :: thesis: for h, i being Integer st h mod (2 to_power n) = i mod (2 to_power n) holds
((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n)
let h, i be Integer; :: thesis: ( h mod (2 to_power n) = i mod (2 to_power n) implies ((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n) )
assume A1: h mod (2 to_power n) = i mod (2 to_power n) ; :: thesis: ((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n)
n <= MajP (n,(abs i)) by Def1;
then consider y being Nat such that
A2: MajP (n,(abs i)) = n + y by NAT_1:10;
reconsider L = 2 to_power (MajP (n,(abs i))) as Integer ;
reconsider M = 2 to_power (MajP (n,(abs h))) as Integer ;
n <= MajP (n,(abs h)) by Def1;
then consider x being Nat such that
A3: MajP (n,(abs h)) = n + x by NAT_1:10;
reconsider x = x as Nat ;
M = (2 to_power n) * (2 to_power x) by A3, POWER:27;
then A4: M mod (2 to_power n) = (((2 to_power n) mod (2 to_power n)) * (2 to_power x)) mod (2 to_power n) by EULER_2:8
.= (0 * (2 to_power x)) mod (2 to_power n) by NAT_D:25
.= 0 by NAT_D:26 ;
reconsider y = y as Nat ;
L = (2 to_power n) * (2 to_power y) by A2, POWER:27;
then A5: L mod (2 to_power n) = (((2 to_power n) mod (2 to_power n)) * (2 to_power y)) mod (2 to_power n) by EULER_2:8
.= (0 * (2 to_power y)) mod (2 to_power n) by NAT_D:25
.= 0 by NAT_D:26 ;
A6: (L + i) mod (2 to_power n) = ((L mod (2 to_power n)) + (i mod (2 to_power n))) mod (2 to_power n) by NAT_D:66
.= (i mod (2 to_power n)) mod (2 to_power n) by A5 ;
(M + h) mod (2 to_power n) = ((M mod (2 to_power n)) + (h mod (2 to_power n))) mod (2 to_power n) by NAT_D:66
.= (h mod (2 to_power n)) mod (2 to_power n) by A4 ;
hence ((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n) by A1, A6; :: thesis: verum