let j, i, 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 )
assume that
A1: j is prime and
A2: i < j and
A3: k < j and
A4: i <> 0 ; :: thesis: ex a being Element of NAT st (a * i) mod j = k
A5: j > 0 by A1, INT_2:def 5;
i,j are_relative_prime by A1, A2, A4, Lm1;
then consider a, b being Integer such that
A6: (a * i) + (b * j) = k by EULER_1:11;

now

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

suppose A7: a >= 0 ; :: thesis: ex a being Element of NAT st (a * i) mod j = k

now

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

suppose b >= 0 ; :: thesis: ex a, a being Element of NAT st (a * i) mod j = k

then reconsider a = a, b = b as Element of NAT by A7, INT_1:16;
A8: ((a * i) + (b * j)) mod j = ((a * i) + ((b * j) mod j)) mod j by NAT_D:23
.= ((a * i) + 0 ) mod j by NAT_D:13
.= (a * i) mod j ;
take a = a; :: thesis: ex a being Element of NAT st (a * i) mod j = k
thus ex a being Element of NAT st (a * i) mod j = k by A3, A6, A8, NAT_D:24; :: thesis: verum

end;

suppose A9: b < 0 ; :: thesis: ex a, a being Element of NAT st (a * i) mod j = k

reconsider a = a as Element of NAT by A7, INT_1:16;
consider b' being Integer such that
A10: b' = 0 - b ;
b - b < 0 - b by A9;
then reconsider b' = b' as Element of NAT by A10, INT_1:16;
take a = a; :: thesis: ex a being Element of NAT st (a * i) mod j = k
((a * i) + (b * j)) + (b' * j) = a * i by A10;
then (a * i) mod j = k mod j by A6, NAT_D:21
.= k by A3, NAT_D:24 ;
hence ex a being Element of NAT st (a * i) mod j = k ; :: thesis: verum

end;

end;

end;

hence ex a being Element of NAT st (a * i) mod j = k ; :: thesis: verum

end;

suppose A11: a < 0 ; :: thesis: ex a being Element of NAT st (a * i) mod j = k

consider a1 being Integer such that
A12: a1 = 0 - a ;
a - a < 0 - a by A11;
then reconsider a1 = a1 as Element of NAT by A12, INT_1:16;
consider a2 being Element of NAT such that
A13: a2 = (a1 div j) + 1 ;
consider a' being Integer such that
A14: a' = a + (a2 * j) ;
A15: a' = ((- a1) + ((a1 div j) * j)) + j by A12, A13, A14;
consider t being Nat such that
A16: ( a1 = (j * (a1 div j)) + t & t < j ) by A5, NAT_D:def 1;
(- t) + t < (- t) + j by A16, XREAL_1:8;
then reconsider a' = a' as Element of NAT by A15, A16, INT_1:16;

now

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

suppose b >= 0 ; :: thesis: ex a' being Element of NAT st (a' * i) mod j = k

then reconsider b = b as Element of NAT by INT_1:16;
take a' = a'; :: thesis: (a' * i) mod j = k
A17: ((a * i) + (b * j)) + ((a2 * j) * i) = (a' * i) + (b * j) by A14;
(k + ((a2 * j) * i)) mod j = (k + ((a2 * i) * j)) mod j
.= k mod j by NAT_D:21
.= k by A3, NAT_D:24 ;
hence (a' * i) mod j = k by A6, A17, NAT_D:21; :: thesis: verum

end;

suppose A18: b < 0 ; :: thesis: ex a' being Element of NAT st (a' * i) mod j = k

consider b' being Integer such that
A19: b' = 0 - b ;
b - b < 0 - b by A18;
then reconsider b' = b' as Element of NAT by A19, INT_1:16;
take a' = a'; :: thesis: (a' * i) mod j = k
(k + ((a2 * j) * i)) + (b' * j) = k + (((a2 * i) + b') * j) ;
hence (a' * i) mod j = k mod j by A6, A14, A19, NAT_D:21
.= k by A3, NAT_D:24 ;
:: thesis: verum

end;

end;

end;

hence ex a being Element of NAT st (a * i) mod j = k ; :: thesis: verum

end;

end;

end;

hence ex a being Element of NAT st (a * i) mod j = k ; :: thesis: verum