let i, j, k, n be 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, Th17;
set I = ChangeVal_1 (i,n);
ChangeVal_1 (i,n) <= 2 to_power n by A2, Th17;
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, Th17;
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, Th17;
ChangeVal_1 (k,n) <= 2 to_power n by A4, Th17;
then A9: ChangeVal_1 (k,n) < (2 to_power n) + 1 by NAT_1:13;
A10: ChangeVal_1 (i,n) > 0 by A2, Th17;

now :: thesis: MUL_MOD ((MUL_MOD (i,j,n)),k,n) = MUL_MOD (i,(MUL_MOD (j,k,n)),n)

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 :: thesis: MUL_MOD ((MUL_MOD (i,j,n)),k,n) = MUL_MOD (i,(MUL_MOD (j,k,n)),n)

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:8 ;
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 :: thesis: MUL_MOD ((MUL_MOD (i,j,n)),k,n) = MUL_MOD (i,(MUL_MOD (j,k,n)),n)

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:8
.= 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:8
.= 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:8 ;
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 :: thesis: MUL_MOD ((MUL_MOD (i,j,n)),k,n) = MUL_MOD (i,(MUL_MOD (j,k,n)),n)

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:8
.= 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:8
.= 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