let n be Nat; :: thesis: for p1, p2 being Prime holds
( not n divides p1 * p2 or n = 1 or n = p1 or n = p2 or n = p1 * p2 )
let p1, p2 be Prime; :: thesis: ( not n divides p1 * p2 or n = 1 or n = p1 or n = p2 or n = p1 * p2 )
assume n divides p1 * p2 ; :: thesis: ( n = 1 or n = p1 or n = p2 or n = p1 * p2 )
then consider a, b being Nat such that
A1: ( a divides p1 & b divides p2 & n = a * b ) by Lem1;
( ( a = 1 or a = p1 ) & ( b = 1 or b = p2 ) ) by A1, INT_2:def 4;
hence ( n = 1 or n = p1 or n = p2 or n = p1 * p2 ) by A1; :: thesis: verum