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

now :: thesis: ex a being Nat st (a * i) mod j = k

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

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

now :: thesis: ex a being Element of NAT ex a being Nat st (a * i) mod j = k

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

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

then reconsider a = a, b = b as Element of NAT by A7, INT_1:3;
take a = a; :: thesis: ex a being Nat st (a * i) mod j = k
((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 ;
hence ex a being Nat st (a * i) mod j = k by A3, A5, NAT_D:24; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

suppose A10: a < 0 ; :: thesis: ex a being Nat st (a * i) mod j = k

consider a1 being Integer such that
A11: a1 = 0 - a ;
reconsider a1 = a1 as Element of NAT by A10, A11, INT_1:3;
consider a2 being Nat such that
A12: a2 = (a1 div j) + 1 ;
consider a9 being Integer such that
A13: a9 = a + (a2 * j) ;
A14: a9 = ((- a1) + ((a1 div j) * j)) + j by A11, A12, A13;
consider t being Nat such that
A15: a1 = (j * (a1 div j)) + t and
A16: t < j by A6, NAT_D:def 1;
(- t) + t < (- t) + j by A16, XREAL_1:6;
then reconsider a9 = a9 as Element of NAT by A14, A15, INT_1:3;

now :: thesis: ex a9 being Element of NAT st (a9 * i) mod j = k

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

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

then reconsider b = b as Element of NAT by INT_1:3;
take a9 = a9; :: thesis: (a9 * i) mod j = k
A17: (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 ;
((a * i) + (b * j)) + ((a2 * j) * i) = (a9 * i) + (b * j) by A13;
hence (a9 * i) mod j = k by A5, A17, NAT_D:21; :: thesis: verum

end;

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

take a9 = a9; :: thesis: (a9 * i) mod j = k
consider b9 being Integer such that
A19: b9 = 0 - b ;
reconsider b9 = b9 as Element of NAT by A18, A19, INT_1:3;
(k + ((a2 * j) * i)) + (b9 * j) = k + (((a2 * i) + b9) * j) ;
hence (a9 * i) mod j = k mod j by A5, A13, A19, NAT_D:21
.= k by A3, NAT_D:24 ;
:: thesis: verum

end;

end;

end;

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

end;

end;

end;

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