:: deftheorem Def10 defines INV_MOD IDEA_1:def 10 :
for n being non zero Nat
for i being Nat st i is_expressible_by n & (2 to_power n) + 1 is prime holds
for b₃ being Nat holds
( b₃ = INV_MOD (i,n) iff ( MUL_MOD (i,b₃,n) = 1 & b₃ is_expressible_by n ) );