let p, q be Prime; :: thesis: for k being Nat holds

( not k divides p * q or k = 1 or k = p or k = q or k = p * q )

let k be Nat; :: thesis: ( not k divides p * q or k = 1 or k = p or k = q or k = p * q )

assume A1: k divides p * q ; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

( not k divides p * q or k = 1 or k = p or k = q or k = p * q )

let k be Nat; :: thesis: ( not k divides p * q or k = 1 or k = p or k = q or k = p * q )

assume A1: k divides p * q ; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

per cases
( k,p are_coprime or k gcd p = p )
by PEPIN:2;

end;

suppose
k,p are_coprime
; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

then
k divides q
by A1, PEPIN:3;

hence ( k = 1 or k = p or k = q or k = p * q ) by INT_2:def 4; :: thesis: verum

end;hence ( k = 1 or k = p or k = q or k = p * q ) by INT_2:def 4; :: thesis: verum

suppose
k gcd p = p
; :: thesis: ( k = 1 or k = p or k = q or k = p * q )

then
p divides k
by NAT_D:def 5;

then consider l being Nat such that

A2: k = p * l by NAT_D:def 3;

consider m being Nat such that

A3: k * m = p * q by A1, NAT_D:def 3;

p * (l * m) = p * q by A2, A3;

then l * m = q by XCMPLX_1:5;

then l divides q by NAT_D:def 3;

then ( l = 1 or l = q ) by INT_2:def 4;

hence ( k = 1 or k = p or k = q or k = p * q ) by A2; :: thesis: verum

end;then consider l being Nat such that

A2: k = p * l by NAT_D:def 3;

consider m being Nat such that

A3: k * m = p * q by A1, NAT_D:def 3;

p * (l * m) = p * q by A2, A3;

then l * m = q by XCMPLX_1:5;

then l divides q by NAT_D:def 3;

then ( l = 1 or l = q ) by INT_2:def 4;

hence ( k = 1 or k = p or k = q or k = p * q ) by A2; :: thesis: verum