let n be non zero 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,|.h.|))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,|.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,|.h.|))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,|.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,|.h.|))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,|.i.|))) + i) mod (2 to_power n)
n <= MajP (n,|.i.|) by Def1;
then consider y being Nat such that
A2: MajP (n,|.i.|) = n + y by NAT_1:10;
reconsider L = 2 to_power (MajP (n,|.i.|)) as Integer ;
reconsider M = 2 to_power (MajP (n,|.h.|)) as Integer ;
n <= MajP (n,|.h.|) by Def1;
then consider x being Nat such that
A3: MajP (n,|.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,|.h.|))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,|.i.|))) + i) mod (2 to_power n) by A1, A6; :: thesis: verum