let l, p, n1, n2 be Nat; :: thesis: ( 0 <> l & p > l & p > n1 & p > n2 & (l * n1) mod p = (l * n2) mod p & p is prime implies n1 = n2 )

assume that

A1: ( l <> 0 & p > l ) and

A2: p > n1 and

A3: p > n2 ; :: thesis: ( not (l * n1) mod p = (l * n2) mod p or not p is prime or n1 = n2 )

assume A4: (l * n1) mod p = (l * n2) mod p ; :: thesis: ( not p is prime or n1 = n2 )

assume A5: p is prime ; :: thesis: n1 = n2

then ((l * n1) - (l * n2)) mod p = 0 by A4, INT_4:22;

then A6: p divides l * (n1 - n2) by A5, INT_1:62;

assume that

A1: ( l <> 0 & p > l ) and

A2: p > n1 and

A3: p > n2 ; :: thesis: ( not (l * n1) mod p = (l * n2) mod p or not p is prime or n1 = n2 )

assume A4: (l * n1) mod p = (l * n2) mod p ; :: thesis: ( not p is prime or n1 = n2 )

assume A5: p is prime ; :: thesis: n1 = n2

then ((l * n1) - (l * n2)) mod p = 0 by A4, INT_4:22;

then A6: p divides l * (n1 - n2) by A5, INT_1:62;

per cases
( p divides l or p divides n1 - n2 )
by A5, A6, INT_5:7;

end;

suppose A7:
p divides n1 - n2
; :: thesis: n1 = n2

end;

per cases
( n1 - n2 > 0 or n1 - n2 = 0 or n1 - n2 < 0 )
;

end;

suppose A8:
n1 - n2 > 0
; :: thesis: n1 = n2

then
( p divides n1 -' n2 & n1 -' n2 > 0 )
by A7, XREAL_0:def 2;

then p <= n1 -' n2 by NAT_D:7;

then p + n2 <= (n1 -' n2) + n2 by XREAL_1:6;

then p + n2 <= (n1 - n2) + n2 by A8, XREAL_0:def 2;

then p + n2 < p by A2, XXREAL_0:2;

then (p + n2) - p < p - p by XREAL_1:9;

then n2 < 0 ;

hence n1 = n2 ; :: thesis: verum

end;then p <= n1 -' n2 by NAT_D:7;

then p + n2 <= (n1 -' n2) + n2 by XREAL_1:6;

then p + n2 <= (n1 - n2) + n2 by A8, XREAL_0:def 2;

then p + n2 < p by A2, XXREAL_0:2;

then (p + n2) - p < p - p by XREAL_1:9;

then n2 < 0 ;

hence n1 = n2 ; :: thesis: verum

suppose
n1 - n2 < 0
; :: thesis: n1 = n2

then A9:
- (n1 - n2) > 0
;

then A10: n2 - n1 > 0 ;

then A11: n2 -' n1 > 0 by XREAL_0:def 2;

p divides - (n1 - n2) by A7, INT_2:10;

then p divides n2 -' n1 by A10, XREAL_0:def 2;

then p <= n2 -' n1 by A11, NAT_D:7;

then p + n1 <= (n2 -' n1) + n1 by XREAL_1:6;

then p + n1 <= (n2 - n1) + n1 by A9, XREAL_0:def 2;

then p + n1 < p by A3, XXREAL_0:2;

then (p + n1) - p < p - p by XREAL_1:9;

then n1 < 0 ;

hence n1 = n2 ; :: thesis: verum

end;then A10: n2 - n1 > 0 ;

then A11: n2 -' n1 > 0 by XREAL_0:def 2;

p divides - (n1 - n2) by A7, INT_2:10;

then p divides n2 -' n1 by A10, XREAL_0:def 2;

then p <= n2 -' n1 by A11, NAT_D:7;

then p + n1 <= (n2 -' n1) + n1 by XREAL_1:6;

then p + n1 <= (n2 - n1) + n1 by A9, XREAL_0:def 2;

then p + n1 < p by A3, XXREAL_0:2;

then (p + n1) - p < p - p by XREAL_1:9;

then n1 < 0 ;

hence n1 = n2 ; :: thesis: verum