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

now

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

suppose A7: 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
A8: j = 0 ;
take j = j; :: thesis: ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n )
A9: j is_expressible_by n by A3, A8, Def3;
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 ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) by A9; :: thesis: verum

end;

suppose A10: 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
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: ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n )
A13: a <> 0 by A11, NAT_D:24;

now

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

suppose A14: 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 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 by Def3;
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 ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) by A16; :: thesis: verum

end;

suppose A17: 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 A18: k = 0 by Def8;
then A19: k is_expressible_by n by A3, Def3;
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 ex b₁ being Element of NAT st
( MUL_MOD i,b₁,n = 1 & b₁ is_expressible_by n ) by A19; :: 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