let a, b, c, n be Integer; :: thesis: ( 3 < n implies ex k being Integer st
( not n divides k + a & not n divides k + b & not n divides k + c ) )
assume A1: 3 < n ; :: thesis: ex k being Integer st
( not n divides k + a & not n divides k + b & not n divides k + c )
set r1 = (- a) mod n;
set r2 = (- b) mod n;
set r3 = (- c) mod n;
reconsider X = n as Nat by A1, TARSKI:1;
3 + 1 <= n by A1, NAT_1:13;
then card (Segm 4) c= card (Segm X) by NAT_1:40;
then consider r being object such that
A2: r in X and
A3: ( (- a) mod n <> r & (- b) mod n <> r & (- c) mod n <> r ) by GLIBPRE0:17;
reconsider r = r as Nat by A2;
take r ; :: thesis: ( not n divides r + a & not n divides r + b & not n divides r + c )
Segm X = X ;
then r < n by A2, NAT_1:44;
hence ( not n divides r + a & not n divides r + b & not n divides r + c ) by A3, Lm38; :: thesis: verum