let n, i, j, k be Element of NAT ; :: thesis: ( (2 to_power n) + 1 is prime & i is_expressible_by n & j is_expressible_by n & k is_expressible_by n implies MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n )
assume that
A1: (2 to_power n) + 1 is prime and
A2: i is_expressible_by n and
A3: j is_expressible_by n and
A4: k is_expressible_by n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n
set J = ChangeVal_1 j,n;
A5: ChangeVal_1 j,n > 0 by A3, Th18;
set I = ChangeVal_1 i,n;
ChangeVal_1 i,n <= 2 to_power n by A2, Th18;
then A6: ChangeVal_1 i,n < (2 to_power n) + 1 by NAT_1:13;
ChangeVal_1 j,n <= 2 to_power n by A3, Th18;
then A7: ChangeVal_1 j,n < (2 to_power n) + 1 by NAT_1:13;
set K = ChangeVal_1 k,n;
A8: ChangeVal_1 k,n > 0 by A4, Th18;
ChangeVal_1 k,n <= 2 to_power n by A4, Th18;
then A9: ChangeVal_1 k,n < (2 to_power n) + 1 by NAT_1:13;
A10: ChangeVal_1 i,n > 0 by A2, Th18;

now

set CV = ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1);
((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) < (2 to_power n) + 1 by NAT_D:1;
then A11: ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) <= 2 to_power n by NAT_1:13;
A12: ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) <> 0 by A1, A6, A10, A7, A5, Th5;

now

per cases ( ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) = 2 to_power n or ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) < 2 to_power n ) by A11, XXREAL_0:1;

suppose A13: ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) = 2 to_power n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n

then A14: MUL_MOD (MUL_MOD i,j,n),k,n = ChangeVal_2 (((ChangeVal_1 0 ,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by Def8
.= ChangeVal_2 (((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by A13, Def7
.= ChangeVal_2 ((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by EULER_2:10 ;
set CV2 = ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1);
((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) < (2 to_power n) + 1 by NAT_D:1;
then A15: ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) <= 2 to_power n by NAT_1:13;
A16: ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) <> 0 by A1, A7, A5, A9, A8, Th5;

now

per cases ( ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) = 2 to_power n or ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) < 2 to_power n ) by A15, XXREAL_0:1;

suppose A17: ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) = 2 to_power n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n

then MUL_MOD i,(MUL_MOD j,k,n),n = ChangeVal_2 (((ChangeVal_1 i,n) * (ChangeVal_1 0 ,n)) mod ((2 to_power n) + 1)),n by Def8
.= ChangeVal_2 (((ChangeVal_1 i,n) * (((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1))) mod ((2 to_power n) + 1)),n by A17, Def7
.= ChangeVal_2 (((ChangeVal_1 i,n) * ((ChangeVal_1 j,n) * (ChangeVal_1 k,n))) mod ((2 to_power n) + 1)),n by EULER_2:10
.= ChangeVal_2 ((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n ;
hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n by A14; :: thesis: verum

end;

suppose ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) < 2 to_power n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n

then MUL_MOD j,k,n = ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) by Def8;
then MUL_MOD i,(MUL_MOD j,k,n),n = ChangeVal_2 (((ChangeVal_1 i,n) * (((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1))) mod ((2 to_power n) + 1)),n by A16, Def7
.= ChangeVal_2 (((ChangeVal_1 i,n) * ((ChangeVal_1 j,n) * (ChangeVal_1 k,n))) mod ((2 to_power n) + 1)),n by EULER_2:10
.= ChangeVal_2 ((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n ;
hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n by A14; :: thesis: verum

end;

end;

end;

hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n ; :: thesis: verum

end;

suppose ((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1) < 2 to_power n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n

then A18: MUL_MOD (MUL_MOD i,j,n),k,n = ChangeVal_2 (((ChangeVal_1 (((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1)),n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by Def8
.= ChangeVal_2 (((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by A12, Def7
.= ChangeVal_2 ((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by EULER_2:10 ;
set CV2 = ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1);
((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) < (2 to_power n) + 1 by NAT_D:1;
then A19: ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) <= 2 to_power n by NAT_1:13;
A20: ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) <> 0 by A1, A7, A5, A9, A8, Th5;

now

per cases ( ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) = 2 to_power n or ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) < 2 to_power n ) by A19, XXREAL_0:1;

suppose A21: ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) = 2 to_power n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n

then MUL_MOD i,(MUL_MOD j,k,n),n = ChangeVal_2 (((ChangeVal_1 i,n) * (ChangeVal_1 0 ,n)) mod ((2 to_power n) + 1)),n by Def8
.= ChangeVal_2 (((ChangeVal_1 i,n) * (((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1))) mod ((2 to_power n) + 1)),n by A21, Def7
.= ChangeVal_2 (((ChangeVal_1 i,n) * ((ChangeVal_1 j,n) * (ChangeVal_1 k,n))) mod ((2 to_power n) + 1)),n by EULER_2:10
.= ChangeVal_2 ((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n ;
hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n by A18; :: thesis: verum

end;

suppose ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) < 2 to_power n ; :: thesis: MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n

then MUL_MOD j,k,n = ((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1) by Def8;
then MUL_MOD i,(MUL_MOD j,k,n),n = ChangeVal_2 (((ChangeVal_1 i,n) * (((ChangeVal_1 j,n) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1))) mod ((2 to_power n) + 1)),n by A20, Def7
.= ChangeVal_2 (((ChangeVal_1 i,n) * ((ChangeVal_1 j,n) * (ChangeVal_1 k,n))) mod ((2 to_power n) + 1)),n by EULER_2:10
.= ChangeVal_2 ((((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n ;
hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n by A18; :: thesis: verum

end;

end;

end;

hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n ; :: thesis: verum

end;

end;

end;

hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n ; :: thesis: verum

end;

hence MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n ; :: thesis: verum