:: deftheorem Def2 defines order PEPIN:def 2 :
for i, p being Nat st p > 1 & i,p are_coprime holds
for b₃ being Element of NAT holds
( b₃ = order (i,p) iff ( b₃ > 0 & (i |^ b₃) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < b₃ & b₃ <= k ) ) ) );