A3: 2 to_power n > 0 by POWER:34;
then A4: (2 to_power n) + 1 > 0 + 1 by XREAL_1:6;
then ((2 to_power n) + 1) - 1 >= (1 + 1) - 1 by NAT_1:13;
then (((2 to_power n) + 1) - 1) - 1 >= ((1 + 1) - 1) - 1 by XREAL_1:9;
then reconsider n3 = (((2 to_power n) + 1) - 1) - 1 as Element of NAT by INT_1:3;
reconsider nn = (2 to_power n) + 1 as Nat ;
reconsider n2 = ((2 to_power n) + 1) - 1 as Nat ;
A5: 2 to_power n <> 1 by POWER:35;
n2 * n2 = (nn * n3) + 1 ;
then A6: (n2 * n2) mod nn = 1 mod nn by NAT_D:21
.= 1 by A4, NAT_D:24 ;

per cases ( i = 0 or i <> 0 ) ;

suppose A7: i = 0 ; :: thesis: ex b₁ being Nat st
( MUL_MOD (i,b₁,n) = 1 & b₁ is_expressible_by n )

consider j being Nat such that
A8: j = 0 ;
take j ; :: thesis: ( MUL_MOD (i,j,n) = 1 & j is_expressible_by n )
A9: j is_expressible_by n by A3, A8;
MUL_MOD (i,j,n) = ChangeVal_2 ((((2 to_power n) * (ChangeVal_1 (0,n))) mod nn),n) by A7, A8, Def7
.= ChangeVal_2 (((n2 * n2) mod nn),n) by Def7
.= 1 by A5, A6, Def8 ;
hence ( MUL_MOD (i,j,n) = 1 & j is_expressible_by n ) by A9; :: thesis: verum

end;

suppose A10: i <> 0 ; :: thesis: ex b₁ being Nat st
( MUL_MOD (i,b₁,n) = 1 & b₁ is_expressible_by n )

i < 2 to_power n by A1;
then i < (2 to_power n) + 1 by NAT_1:13;
then consider a being Nat such that
A11: (a * i) mod ((2 to_power n) + 1) = 1 and
A12: a < (2 to_power n) + 1 by A2, A4, A10, Th1;
take k = ChangeVal_2 (a,n); :: thesis: ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )
A13: a <> 0 by A11, NAT_D:24;

now :: thesis: ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )

per cases ( a <> 2 to_power n or a = 2 to_power n ) ;

suppose A14: a <> 2 to_power n ; :: thesis: ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )

then A15: k = a by Def8;
then k <= 2 to_power n by A12, NAT_1:13;
then k < 2 to_power n by A14, A15, XXREAL_0:1;
then A16: k is_expressible_by n ;
MUL_MOD (i,k,n) = ChangeVal_2 (((i * (ChangeVal_1 (k,n))) mod ((2 to_power n) + 1)),n) by A10, Def7
.= ChangeVal_2 (((i * a) mod ((2 to_power n) + 1)),n) by A13, A15, Def7
.= 1 by A5, A11, Def8 ;
hence ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n ) by A16; :: thesis: verum

end;

suppose A17: a = 2 to_power n ; :: thesis: ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )

then A18: k = 0 by Def8;
then A19: k is_expressible_by n by A3;
MUL_MOD (i,k,n) = ChangeVal_2 (((i * (ChangeVal_1 (k,n))) mod ((2 to_power n) + 1)),n) by A10, Def7
.= ChangeVal_2 (((i * a) mod ((2 to_power n) + 1)),n) by A17, A18, Def7
.= 1 by A5, A11, Def8 ;
hence ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n ) by A19; :: thesis: verum

end;

end;

end;

hence ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n ) ; :: thesis: verum

end;

end;