let i, j, k be Element of NAT ; :: thesis: ( j is prime & i < j & k < j & i <> 0 implies ex a being Element of NAT st
( (a * i) mod j = k & a < j ) )
assume A1: ( j is prime & i < j & k < j & i <> 0 ) ; :: thesis: ex a being Element of NAT st
( (a * i) mod j = k & a < j )
then consider a being Element of NAT such that
A2: (a * i) mod j = k by Lm2;
consider a' being Element of NAT such that
A3: a' = a mod j ;
take a' ; :: thesis: ( (a' * i) mod j = k & a' < j )
thus ( (a' * i) mod j = k & a' < j ) by A1, A2, A3, EULER_2:10, NAT_D:1; :: thesis: verum