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)
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
A2: 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 A2, POWER:32;
then A3: 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:10
.= (0 * (2 to_power x)) mod (2 to_power n) by NAT_D:25
.= 0 by NAT_D:26 ;
reconsider L = 2 to_power (MajP n,(abs i)) as Integer ;
n <= MajP n,(abs i) by Def1;
then consider y being Nat such that
A4: MajP n,(abs i) = n + y by NAT_1:10;
reconsider y = y as Nat ;
L = (2 to_power n) * (2 to_power y) by A4, POWER:32;
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:10
.= (0 * (2 to_power y)) mod (2 to_power n) by NAT_D:25
.= 0 by NAT_D:26 ;
A6: (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 INT_3:14
.= (h mod (2 to_power n)) mod (2 to_power n) by A3 ;
(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 INT_3:14
.= (i mod (2 to_power n)) mod (2 to_power n) by A5 ;
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