A2: 2 to_power n > 0 by POWER:39;
reconsider n2 = ((2 to_power n) + 1) - 1 as Element of NAT ;
A3: (2 to_power n) + 1 > 0 + 1 by A2, XREAL_1:8;
reconsider nn = (2 to_power n) + 1 as Element of NAT ;
A4: 2 to_power n <> 1 by POWER:40;
((2 to_power n) + 1) - 1 >= (1 + 1) - 1 by A3, NAT_1:13;
then (((2 to_power n) + 1) - 1) - 1 >= ((1 + 1) - 1) - 1 by XREAL_1:11;
then reconsider n3 = (((2 to_power n) + 1) - 1) - 1 as Element of NAT by INT_1:16;
n2 * n2 = (nn * n3) + 1 ;
then A5: (n2 * n2) mod nn = 1 mod nn by NAT_D:21
.= 1 by A3, NAT_D:24 ;

now

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

suppose A6: i = 0 ; :: thesis: ex j, b₂ being Element of NAT st
( MUL_MOD i,b₂,n = 1 & b₂ is_expressible_by n )

consider j being Element of NAT such that
A7: j = 0 ;
take j = j; :: thesis: ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n )
A8: MUL_MOD i,j,n = ChangeVal_2 (((2 to_power n) * (ChangeVal_1 0 ,n)) mod nn),n by A6, A7, Def7
.= ChangeVal_2 ((n2 * n2) mod nn),n by Def7
.= 1 by A4, A5, Def8 ;
j is_expressible_by n by A2, A7, Def3;
hence ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) by A8; :: thesis: verum

end;

suppose A9: i <> 0 ; :: thesis: ex k, b₂ being Element of NAT st
( MUL_MOD i,b₂,n = 1 & b₂ is_expressible_by n )

i < 2 to_power n by A1, Def3;
then i < (2 to_power n) + 1 by NAT_1:13;
then consider a being Element of NAT such that
A10: ( (a * i) mod ((2 to_power n) + 1) = 1 & a < (2 to_power n) + 1 ) by A1, A3, A9, Th1;
A11: a <> 0 by A10, NAT_D:24;
take k = ChangeVal_2 a,n; :: thesis: ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n )

now

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

suppose A12: a <> 2 to_power n ; :: thesis: ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n )

then A13: k = a by Def8;
then k <= 2 to_power n by A10, NAT_1:13;
then k < 2 to_power n by A12, A13, XXREAL_0:1;
then A14: k is_expressible_by n by Def3;
MUL_MOD i,k,n = ChangeVal_2 ((i * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by A9, Def7
.= ChangeVal_2 ((i * a) mod ((2 to_power n) + 1)),n by A11, A13, Def7
.= 1 by A4, A10, Def8 ;
hence ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) by A14; :: thesis: verum

end;

suppose A15: a = 2 to_power n ; :: thesis: ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n )

then A16: k = 0 by Def8;
then A17: k is_expressible_by n by A2, Def3;
MUL_MOD i,k,n = ChangeVal_2 ((i * (ChangeVal_1 k,n)) mod ((2 to_power n) + 1)),n by A9, Def7
.= ChangeVal_2 ((i * a) mod ((2 to_power n) + 1)),n by A15, A16, Def7
.= 1 by A4, A10, Def8 ;
hence ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) by A17; :: thesis: verum

end;

end;

end;

hence ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) ; :: thesis: verum

end;

end;

end;

hence ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) ; :: thesis: verum