let i, j, k be Nat; :: thesis: ( j is prime & i < j & k < j & i <> 0 implies ex a being Nat st
( (a * i) mod j = k & a < j ) )
assume that
A1: j is prime and
A2: i < j and
A3: ( k < j & i <> 0 ) ; :: thesis: ex a being Nat st
( (a * i) mod j = k & a < j )
consider a being Nat such that
A4: (a * i) mod j = k by A1, A2, A3, Lm2;
consider a9 being Nat such that
A5: a9 = a mod j ;
take a9 ; :: thesis: ( (a9 * i) mod j = k & a9 < j )
thus ( (a9 * i) mod j = k & a9 < j ) by A2, A4, A5, EULER_2:8, NAT_D:1; :: thesis: verum